Description

Do inPythonusingpyEDApackage . You may find installation instructions at https://pyeda.readthedocs.io/en/latest/install.html understand how CTL formulas are interpreted on a graph. 0. Let G be a graph over 32 nodes (namely, node 0, , node 31). Forall 0 i,j 31, there is an edge from node i to node j iff (i + 3)%32 = j%32 or (i + 8)%32 = j%32. (% is the modular operator in C; e.g., 35% 32=3.) A node i is even if i is an even number. A node i is prime if i is a prime number. In particular, we define [even] as the set 0 , 2 , 4 ,6….30 and [prime] as the set { 3, 5, 7, 11, 13, 17, 19, 23, 29, 31} . We use R to denote the set of all edges in G. 1. (20%, graded on correctness and efficiency) (write-up) Let p be a CTL formula while [p] is the set of nodes in G that satisfy p. Pleasedesignafix-pointiterationalgorithmthat computes [EF p](the set of nodes in G that satisfy EF p from R and [p]). Pleasedesignafix-pointiterationalgorithmthat computes [EGp](the set of nodes in G that satisfy EGp from R and [p]). You may first study the algorithms for [AGp] and [AF p]. 2. (50%, graded on correctness and clarity. If you use explicit graph search such asDFS, you receive0.) (coding inPython)Every finite set can be coded as a BDD. Please write a Python program to compute [EG(even EFprime)] (the set of nodes that satisfy the formula EG( even EF prime).), and verify your answer by checking node 5 satisfies EG(even EF prime) and node 6 doesnt satisfy EG(even EF prime). (Important: your code shall first encode R, [even], [prime] in BDDs using pyEDA and then using methods provided with the package, implement the iteration algorithms provided in 3 symbolically inBDD using methods in the package. ManystudentsfindmethodsBDD. compose()andBDD. smoothing() are quite useful in the package.) • • 2 ⊆ 3. (30%, graded on originality, depth, and quality of writing.) (write-up) To make use of the idea of BDDs, a major difficulty is which graph is chosen to model a given set of data. When the graph is too large, the symbolic exploartion algorithm would not even run efficiently. However, if the graph is too small, the modeling might not be even realistic. We now think about an example problem. Consider a finite set L of DNA strands, where each strand is simply a string on alphabet {A, T, C, G} (that is, a strand is a sequence of nucleotides, each of which is chosen from four nitrogen-containing nucleobases.). One may use a deterministic finite automaton (DFA)1 M (which itself is a graph) to model the set L; i.e L L(M ). That is, each strand w in L, there is a walk in M (from the initial state to an accepting state) such that the symbols sequentially collected on the transitions on the walk form exactly the w. Clearly, many many different M can be used to model L(e.g., M canbe ridiculously simplewithonly one state andaccepting every word onthe alphabet.). Consequently,oneneed come up with ametric Q(M,L), which is a real number,to characterize the “precision” on using the given M to model L. When this is done, one can argue, for two given DFAs M1 and M2 which both model the given L, which model is more precise. Now, you need write a mini-paper (of 1 or 2 or more pages) in figuring out ways to define Q(M, L) and to design algorithms to compute Q(M, L).23