BBBBG-fsttcs07

C. Baier, N. Bertrand, P. Bouyer, Th. Brihaye, M. Groesser. Probabilistic and Topological Semantics for Timed Automata. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), V. Arvind, Sanjiva Prasad (eds.), Lecture Notes in Computer Science, Volume 4855, Pages 1529-3785, New Delhi, India, December 2007.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

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

Contact

Nathalie Bertrand http://www.irisa.fr/prive/nbertran/

BibTex Reference

@InProceedings{BBBBG-fsttcs07,
   Author = {Baier, C. and Bertrand, N. and Bouyer, P. and Brihaye, Th. and Groesser, M.},
   Title = {Probabilistic and Topological Semantics for Timed Automata},
   BookTitle = {{P}roceedings of the 27th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'07)},
   editor = {Arvind, V. and Prasad, Sanjiva},
   Volume = {    4855},
   Pages = {1529--3785},
   Series = {Lecture Notes in Computer Science},
   Publisher = {Springer},
   Address = {New Delhi, India},
   Month = {December},
   Year = {2007}
}

EndNote Reference [help]

Get EndNote Reference (.ref)