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
Contributor : Nathalie Bertrand Connect in order to contact the contributor
Submitted on : Friday, October 16, 2009 - 11:15:34 AM
Last modification on : Tuesday, March 30, 2021 - 12:12:08 PM

Links full text




Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Marcus Grösser. 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⟩



Record views