LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
reachable_pushdown_configurations_are_regular [2011/05/24 14:22]
vkuncak
reachable_pushdown_configurations_are_regular [2011/05/24 14:29] (current)
vkuncak
Line 1: Line 1:
 ====== Backward reachable pushdown configurations are regular ====== ====== Backward reachable pushdown configurations are regular ======
  
-Example:+Examples:
   * program with procedures that ensures proper use of a global lock   * program with procedures that ensures proper use of a global lock
 +  * Java stack inspection from security policies; accessing a local file system for logging purposes
  
 We next show that in a push down system, the pre-image of a regular set of configurations is again a regular set of configurations. ​ Moreover, the new finite state machine for configurations can use the same set of states as the original one.  This gives an algorithm for verifying regular properties of push down automata by representing them using finite state machines. ​ Based on the introductory part of [[http://​www.liafa.jussieu.fr/​~abou/​BEM97.ps.gz|Reachability Analysis of Pushdown Automata: Application to Model Checking]]. We next show that in a push down system, the pre-image of a regular set of configurations is again a regular set of configurations. ​ Moreover, the new finite state machine for configurations can use the same set of states as the original one.  This gives an algorithm for verifying regular properties of push down automata by representing them using finite state machines. ​ Based on the introductory part of [[http://​www.liafa.jussieu.fr/​~abou/​BEM97.ps.gz|Reachability Analysis of Pushdown Automata: Application to Model Checking]].
Line 41: Line 42:
 To reach the set of all states that can result in a state in $T$ in zero or one steps, we compute $T \cup \mbox{pre}(T)$ by keeping the previous edges along with the new ones in the multi-automaton. ​ By repeating this process we obtain the exact representation of the set of states that can reach states in the original regular set of configurations. ​ This process converges because we only add new edges, never add new states to the automaton, so the maximal number of edges is bounded. To reach the set of all states that can result in a state in $T$ in zero or one steps, we compute $T \cup \mbox{pre}(T)$ by keeping the previous edges along with the new ones in the multi-automaton. ​ By repeating this process we obtain the exact representation of the set of states that can reach states in the original regular set of configurations. ​ This process converges because we only add new edges, never add new states to the automaton, so the maximal number of edges is bounded.
  
-**Example application:​** 
-  * Java stack inspection from security policies; accessing a local file system for logging purposes