Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
reachable_pushdown_configurations_are_regular [2010/05/28 02:06] vkuncak |
reachable_pushdown_configurations_are_regular [2010/05/28 09:56] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Backward reachable pushdown configurations are regular ====== | ====== Backward reachable pushdown configurations are regular ====== | ||
| + | |||
| + | Example: | ||
| + | * program with procedures that ensures proper use of a global lock | ||
| 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]]. | ||