Logic in Computer Science (LICS 2003)

Paper: Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems (at LICS 2003)

Authors: Nir Piterman Moshe Y. Vardi

Abstract

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.

BibTeX

  @InProceedings{PitermanVardi-MicroMacroStackSyst,
    author = 	 {Nir Piterman and Moshe Y. Vardi},
    title = 	 {Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2003},
    year =	 2003,
    editor =	 {Phokion G. Kolaitis},
    month =	 {June}, 
    pages =      {381--391},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }