Memory Event Clocks

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

2 Téléchargements (Pure)

Résumé

We introduce logics and automata based on memory event clocks. A memory clock is not really reset: instead, a new clock is created, while the old one is still accessible by indexing. We can thus constrain not only the time since the last reset (which was the main limitation in event clocks), but also since previous resets. When we introduce these clocks in the linear temporal logic of the reals, we create Recursive Memory Event Clocks Temporal Logic (RMECTL). It turns out to have the same expressiveness as the Temporal Logic with Counting (TLC) of Hirshfeld and Rabinovich. We then examine automata with recursive memory event clocks (RMECA). Recursive event clocks are reset by simpler RMECA, hence the name "recursive". In contrast, we show that for RMECA, memory clocks do not add expressiveness, but only concision. The original RECA define thus a fully decidable, robust and expressive level of real-time expressiveness.
langue originaleAnglais
titreFormal Modeling and Analysis of Timed Systems
EditeurSpringer
Pages198
Volume6246
Les DOIs
étatPublié - 2010

Série de publications

NomFormal Modeling and Analysis of Timed Systems, Lecture Notes in Computer Science

    Empreinte digitale

Contient cette citation

Ortiz, J., Legay, A., & Schobbens, P-Y. (2010). Memory Event Clocks. Dans Formal Modeling and Analysis of Timed Systems (Vol 6246, p. 198). (Formal Modeling and Analysis of Timed Systems, Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-642-15297-9_16