Skip to Main content Skip to Navigation
Journal articles

Diagnosing timed automata using timed markings

Abstract : We consider the problems of efficiently diagnosing (and predicting) what did (and will) happen after a given sequence of observations of the execution of a partially observable one-clock timed automaton. This is made difficult by the facts that timed automata are infinite-state systems, and that they can in general not be determinized. We introduce timed markings as a formalism to keep track of the evolution of the set of reachable configurations over time. We show how timed markings can be used to efficiently represent the closure under silent transitions of such automata. We report on our implementation of this approach compared to the approach of Tripakis (Fault diagnosis for timed automata, in: Damm, Olderog (eds) Formal techniques in real-time and fault-tolerant systems, Springer, Berlin, 2002) and provide some insight to a generalization of our approach to n-clock timed automata.
Complete list of metadata
Contributor : Patricia Bouyer <>
Submitted on : Wednesday, September 15, 2021 - 8:21:27 AM
Last modification on : Thursday, September 16, 2021 - 3:42:25 AM


Files produced by the author(s)



Patricia Bouyer, Léo Henry, Samy Jaziri, Thierry Jéron, Nicolas Markey. Diagnosing timed automata using timed markings. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2021, 23 (2), pp.229-253. ⟨10.1007/s10009-021-00606-2⟩. ⟨hal-03321763⟩



Record views