Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighteenth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {381--390},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski