Paper: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time (at LICS 1988)

Authors: David E. Muller Ahmed Saoudi Paul E. Schupp

Abstract

The authors give a very simple uniform explanation of the persistence of exponential decidability. They follow M. Vardi and P. Wolper's theory (1986) that given a formula γ of a temporal or dynamic logic, it is important to construct an equivalent automation M_γ. They characterize the weak monadic theory of the tree; it turns out that weak alternating automata greatly simplify design procedures

BibTeX

  @InProceedings{MullerSaoudiSchupp-Weakalternatingauto,
    author = 	 {David E. Muller and Ahmed Saoudi and Paul E. Schupp},
    title = 	 {Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time },
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {422--427},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }