On characteristic formulae for event-recording automata (Q2842241)

Event-Recording Automata (ERA) are a special class of timed automata in which clock resets cannot occur arbitrarily but are linked to the reading of corresponding input symbols. This restriction retains some decidability and closure results of problems that are otherwise undecidable for general timed automata, for instance complementation.NEWLINENEWLINEThe paper at hand studies the problem of finding characteristic formulas for ERA with respect to bisimilarity: given an ERA \(\mathcal{A}\), we want to have a formula \(\varphi_\sim^{\mathcal{A}}\) such that the models of this formula are exactly those ERA that are bisimilar to \(\mathcal{A}\). First, the authors show that a Event-Recording Logic (ERL), a previously proposed logic (\textit{M. Sorea} [Lect. Notes Comput. Sci. 2421, 255--271 (2002; Zbl 1012.03042)]), is too weak to capture bisimilarity for ERA in this sense. ERL is a modal fixpoint logic with modalities for transitions induced by a combination of a time delay and an input action. Here, the authors propose a refinement of ERL in which there are separate modalities for delays and inputs. They show that this logic is strong enough to yield characteristic formulas for ERA with respect to bisimilarity.NEWLINENEWLINEIt is worth noting that these results are only proved -- and most probably only hold -- for a very strong notion of timed bisimilarity in which a delay on one side needs to be matched by exactly the same delay on the other side. The stronger such a notion, the fewer bisimilar ETA there are of course and, hence, the easier it is to capture them in a characteristic formula. Another, more useful notion relaxes the demands on the delays in timed bisimulation: a delay on one side needs to be matched by \textit{some} delay on the other, not necessarily the same. This is sometimes called \textit{abstract} timed bisimilarity in order to distinguish it from the one used in the paper at hand for instance. The usefulness of abstract timed bisimilarity is easily exemplified: consider a timed automaton \(\mathcal{A}\) and then \(\mathcal{A}_2\) resulting from it by multiplying every constant in its guards and invariants by the factor two. In general, \(\mathcal{A}\) and \(\mathcal{A}_2\) are abstract timed bisimilar but are not timed bisimilar. On the other hand, time in timed automata is a unitless concept, so \(\mathcal{A}\) and \(\mathcal{A}_2\) are models of exactly the same system. Hence, they should probably be considered bisimilar, i.e.\ abstract timed bisimilarity seems to be a much more sensible notion of behavioural equivalence.NEWLINENEWLINEAt last, the construction of characteristic formulas is used in conjunction with the fact that model checking for ERA and WT\(_\mu\) is in EXPTIME, in order to derive that checking timed bisimilarity is also in EXPTIME (Corollary 5.6). There is a whole in the argument: the characteristic formulas constructed from ERA are not in the syntax of WT\(_\mu\) but use simultaneous fixpoint definitions. This extended syntax can be translated back into the ordinary syntax of WT\(_\mu\) but this involves an exponential blow-up in general. There is also some reason to believe that it cannot be done better [\textit{F. Bruse} et al., Logic J. IGPL 23, No. 2, 194--216 (2015; \url{doi:10.1093/jigpal/jzu030}]. Thus, it needs to be checked whether model checking formulas in the extended syntax of WT\(_\mu\) with simultaneous fixpoints can still be done in exponential time.