Differences

This shows you the differences between two versions of the page.

--- sav07_lecture_20 [2007/06/05 07:11]
kremena.diatchka
+++ sav07_lecture_20 [2007/06/05 11:02]
kremena.diatchka
@@ Line 169: / Line 169: @@
 ==== Analysis of regular properties of finite-state programs with stack (push down systems- PDS) ====
-Assume we have a program with a finite number of program states. Recall that we can write a push down automata (PDA), $P$, which will accept a language that corresponds to all sequences of operations in the program. Then we can use the PDA to check whether the properties of the program (stated as regular expressions) hold. We do this by constructing a finite state automaton (FSA), $A$, which accepts the language corresponding to the regular expression for the property (recall the [[equivalence of finite state machine and regular expression languages]] ).
+Assume we have a program with a finite number of program states. Recall that we can write a push down automata (PDA), $P$, which will accept a language, $L(P)$, that corresponds to all sequences of operations in the program ([[SAV07 Lecture 19]]). Then we can use the PDA to check whether the properties of the program (stated as regular expressions) hold. We do this by constructing a finite state automaton (FSA), $A$, which accepts the language, $L(A)$, corresponding to the regular expression for the property (recall the [[equivalence of finite state machine and regular expression languages]]). Then we verify whether the property holds by checking if the following is true:
-In other words, if $A$ is an automaton which recognized the  program property, then we have to check that the language recognized by $P$ is a subset of the language :
 $L(P) \subseteq L(A)$
+PDAs and context-free grammars (CFG) are equivalent. Therefore, as an example, we construct the CFG corresponding to the example program above:
+$\Sigma$ = {start, stop, open, read, close}
+$\Gamma$ is the set of symbols on the stack
+$Q$ is the set of program states
+  readContent ::= epsilon | read readContent
+  p2          ::= start readContent stop close
+  p1          ::= open readContent
+  main        ::= p1 p2
+Now to check whether property 2 holds, we have to verify whether $L(CFG) \subseteq L(A)$.
+=== Checking whether one language is a subset of another ===
+Recall that:
+$X \subseteq Y$ iff $X \cap \overline{Y} = \emptyset $
+Therefore showing that $L(P) \subseteq L(A)$ is true is equivalent to showing:
+$L(P) \cap \overline{L(A)} = \emptyset$
+$L(P) \cap L(\overline{A}) = \emptyset$
+Let $Q_{1}$ be the set of states of $P$, and $Q_{2}$ be the set of states of A. Then $L(P) \cap L(\overline{A})$ is the language accepted by a new PDA, $P_{1}$, whose set of states is $Q_{1} \times Q_{2}$. Let $CFG_{1}$ be the CFG equivalent to $P_{1}$. Therefore the problem is now to check whether $L(P_{1}) = \emptyset$ or equivalently whether $L(CFG_{1}) = \emptyset$
+One way to do this is to systematically check the productions of $CFG_{1}$ bottom up (starting from a terminal and following the non-terminals which are used to derive it). If the non-terminal representing the start symbol is reachable in at least one of the derivations, then $L(CFG_{1})$ is non-empty, therefore $L(P) \nsubseteq L(A)$ and the property that $A$ represents does not hold.
+A formal analysis if this "reachability" problem in pushdown automata is discussed in the paper [[http://www.liafa.jussieu.fr/~abou/BEM97.ps.gz|Reachability Analysis of Pushdown Automata: Application to Model Checking]]. A summary of the sections of the paper we covered in class are in the next section.
+=== Convergence of automata for reachable configurations ===
+One of the main results of this paper is an algorithm which, given a set of states S, computes the set of all predecessors of S, denoted by $pre^{*}(S)$. The states in $pre^{*}(S)$ are regular, i.e. they can be represented using a finite state automaton.
+In the paper, a pushdown system is defined as a triplet $\mathcal{P} = (P, \Gamma, \Delta)$ where
+$P$ is a finite set of control locations
+$\Gamma$ is a finite stack alphabet
+$\Delta \subseteq (P \times \Gamma) \times (P \times \Gamma^{*})$ is a set of transition rules
+If $((q, \gamma),(q',w)) \in \Delta$ then we write $(q, \gamma) \hookrightarrow (q', w)$
+Note: an input alphabet is not defined, since here we are only interested in the behavior of the PDS, not the specific language it accepts.
+== Multi-automata ==
+Let $\mathcal{P} = (P, \Gamma, \Delta)$ be a PDS with $P=\{p^{1},...,p^{m}\}$. A multi-automaton (MA for short) for $\mathcal{P}$ is a tuple $\mathcal{A} = (\Gamma, Q, \delta, I, F)$ where
+$Q$ is a finite set of states
+$\delta \subseteq Q \times \Gamma \times Q$ is a set of transitions
+$I \subseteq Q$ is a set of initial states
+$F \subseteq Q$ is a set of final states
+The transition relation $\longrightarrow \subseteq Q \times \Gamma^{*} \times Q$ is defined as the smallest relation which satisfies the following properties
+  * if $(q, \gamma, q')$ then $q \stackrel{\gamma}{\longrightarrow} q'$
+  * $q \stackrel{\varepsilon}{\longrightarrow} q'$ for every $q \in Q$
+  * if $q \stackrel{\w}{\longrightarrow} q''$ and $q'' \stackrel{\gamma}{\longrightarrow} q'$ then $q \stackrel{w\gamma}{\longrightarrow} q'$
+$\mathcal{A}$ accepts or recognizes a configuration $\langle p^{i},w \rangle$ if $s^{i} \stackrel{w}{\longrightarrow} q$ for some $q \in F$. The set of configurations recognized by $\mathcal{A}$ is denoted $Conf($\mathcal{A}$)$. As stated before, a set of configurations is regular if it recognized by some MA.
-  * Product construction based on push down automata and context-free grammar equivalence
-  * Convergence of automata for reachable configurations
 ==== References ====