Skip to Main content Skip to Navigation
Conference papers

Probabilistic and Topological Semantics for Timed Automata.

Abstract : Like most models used in model-checking, timed automata are an idealized mathematical model used for representing systems with strong timing requirements. In such mathematical models, properties can be violated, due to unlikely (sequences of) events. We propose two new semantics for the satisfaction of LTL formulas, one based on probabilities, and the other one based on topology, to rule out these sequences. We prove that the two semantics are equivalent and lead to a PSPACE-Complete model-checking problem for LTL over finite executions.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00424526
Contributor : Nathalie Bertrand <>
Submitted on : Friday, October 16, 2009 - 11:15:34 AM
Last modification on : Tuesday, March 30, 2021 - 12:12:08 PM

Links full text

Identifiers

Collections

Citation

Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Marcus Größer. Probabilistic and Topological Semantics for Timed Automata.. 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), Dec 2007, Dehli, India. pp.179-191, ⟨10.1007/978-3-540-77050-3_15⟩. ⟨inria-00424526⟩

Share

Metrics

Record views

280