Jump to : Download | Note | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Adobe portable document format (pdf)
Copyright noticeThis 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.
To appear
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.
Nathalie Bertrand
nathalie.bertrand@irisa.fr
@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},
Series = {Lecture Notes in Computer Science},
Publisher = {Springer},
Address = {New Delhi, India},
Month = {December},
Year = {2007}
}
Get EndNote Reference (.ref)