Sciweavers

Share
LICS
2003
IEEE

Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems

10 years 5 days ago
Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems
We define the class of micro-macro stack graphs, a new class of graphs modeling infinite-state sequential systems with a decidable model-checking problem. Micro-macro stack graphs are the configuration graphs of stack automata whose states are partitioned into micro and macro states. Nodes of the graph are configurations of the stack automaton where the state is a macro state. Edges of the graph correspond to the sequence of micro steps that the automaton makes between macro states. We prove that this class strictly contains the class of prefix-recognizable graphs. We give a direct automata-theoretic algorithm for model checking ¢ -calculus formulas over micro-macro stack graphs.
Nir Piterman, Moshe Y. Vardi
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where LICS
Authors Nir Piterman, Moshe Y. Vardi
Comments (0)
books