A Decidable Fixpoint Logic for Time-Outs

We show decidability of the satisfiability problem for an extension of the modal mu-calculus with event-recording clocks. Based on techniques for deciding the untimed mu-calculus, we present a complete set of reduction rules for constructing tableaux for formulas of this event-recording logic. To keep track of the actual value of the clocks, the premises and conclusions of our tableau rules are augmented with timing contexts, which are sets of timing constraints satisfied by the actual value of the clocks. The decidability problem is shown to be EXPTIME complete. In addition, we address the problem of model synthesis, that is, given a formula phi, we construct an event-recording automaton that satisfies phi.

Proceedings of the 13th International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science, Springer-Verlag, 2002. © Springer-Verlag.

gzipped postscript or postscript (updated, and improved text)

BibTeX Entry

@InProceedings{MS2002,
  author = 	 {Maria Sorea},
  title = 	 {A Decidable Fixpoint Logic for Time-Outs},
  booktitle = 	 {13th International Conference on Concurrency Theory (CONCUR)},
  year =	  2002,
  pages =        {255--271},
  series =	 {Lecture Notes in Computer Science},
  address =	 {Brno, Czech Republic},
  month =	 {August},
  publisher =	 {Springer Verlag}
}