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.
Type de document :
Communication dans un congrès
27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), Dec 2007, Dehli, India. 4855, pp.179-191, 2007, LNCS. 〈10.1007/978-3-540-77050-3_15〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00424526
Contributeur : Nathalie Bertrand <>
Soumis le : vendredi 16 octobre 2009 - 11:15:34
Dernière modification le : jeudi 11 janvier 2018 - 06:20:13

Lien texte intégral

Identifiants

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. 4855, pp.179-191, 2007, LNCS. 〈10.1007/978-3-540-77050-3_15〉. 〈inria-00424526〉

Partager

Métriques

Consultations de la notice

116