TY - GEN

T1 - Memory Event Clocks

AU - Ortiz, James

AU - Legay, Axel

AU - Schobbens, Pierre-Yves

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-15297-9_16

DO - 10.1007/978-3-642-15297-9_16

M3 - Conference contribution

VL - 6246

T3 - Formal Modeling and Analysis of Timed Systems, Lecture Notes in Computer Science

SP - 198

BT - Formal Modeling and Analysis of Timed Systems

PB - Springer

ER -