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 -