A Decidable Fixpoint Logic for TimeOuts Maria Sorea
We show decidability of the satisfiability problem for an extension of
the modal mucalculus with eventrecording clocks. Based on
techniques for deciding the untimed mucalculus, we present a complete
set of reduction rules for constructing tableaux for formulas of this
eventrecording 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. In addition, we address
the problem of model synthesis, that is, given a formula phi, we
construct an eventrecording automaton that satisfies phi. The
decidability problem is shown to be EXPSPACEcomplete.

concur02@fi.muni.cz 