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 $\mu$-calculus
formulas over micro-macro stack graphs.
@inproceedings{PV03,
author = "N. Piterman and M. Vardi",
title = "Micro-Macro Stack Systems:
A New Frontier of Elementary Decidability for Sequential Systems",
booktitle = "17th IEEE Symposium on Logic in Computer Science",
year = 2003,
}
PDF