Skip to Main content Skip to Navigation
New interface
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

https://hal-centralesupelec.archives-ouvertes.fr/hal-03321763
Contributor : Patricia Bouyer Connect in order to contact the contributor
Submitted on : Wednesday, September 15, 2021 - 8:21:27 AM
Last modification on : Saturday, August 6, 2022 - 3:33:11 AM
Long-term archiving on: : Thursday, December 16, 2021 - 6:10:55 PM

File

rv18.pdf
Files produced by the author(s)

Identifiers

Citation

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, 2021, 23 (2), pp.229-253. ⟨10.1007/s10009-021-00606-2⟩. ⟨hal-03321763⟩

Share

Metrics

Record views

127

Files downloads

206