Differences

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

--- sav07_lecture_20 [2007/06/05 08:21]
kremena.diatchka
+++ sav07_lecture_20 [2007/06/05 11:19]
kremena.diatchka
@@ Line 163: / Line 163: @@
   modifies: FileState
   ensures:  FileState = open
@@ Line 204: / Line 206: @@
 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.
+Section 2.2 of the paper explains how, given a regular set of configurations $C$ of a PDS $\mathcal{P}$ recognized by an MA $\mathcal{A}$, we can construct another MA $\mathcal{A}_{pre*}$ recognizing $pre^{*}(C)$ (refer to paper for details).
+So the idea in the end is to make $C$ include those undesirable (error) states, and then check whether $pre^{*}(C)$ includes the starting state configurations (in other words, whether any of the error states are reachable from the start state).
 ==== References ====