Logic in Computer Science (LICS 1999)

Paper: Modular Temporal Logic (at LICS 1999)

Authors: Augustin Baziramwabo Pierre McKenzie Denis Thérien

Abstract

Thérien and Wilke characterized the Until hierarchy of linear temporal logic in terms of aperiodic monoids. Here, a temporal operator able to count modulo q is introduced. Temporal logic augmented with such operators is found decidable as it is shown to express precisely the solvable regular languages. Natural hierarchies are shown to arise when modular and conventional operators are interleaved. Modular operators are then cast as special cases of more general "group" temporal operators which, added to temporal logic, allow capturing any regular language L in much the same way that the syntactic monoid of L is constructed from groups and aperiodic monoids in the sense of Krohn-Rhodes.

BibTeX

  @InProceedings{BaziramwaboMcKenzie-ModularTemporalLogi,
    author = 	 {Augustin Baziramwabo and Pierre McKenzie and Denis Thérien},
    title = 	 {Modular Temporal Logic},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {344--351},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }