Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
reachable_pushdown_configurations_are_regular [2010/05/28 09:56] vkuncak |
reachable_pushdown_configurations_are_regular [2011/05/24 14:22] vkuncak |
||
|---|---|---|---|
| Line 40: | Line 40: | ||
| 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 | ||