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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., & Größer, M. (2007). Probabilistic and topological semantics for timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4855 LNCS, pp. 179–191). Springer Verlag. https://doi.org/10.1007/978-3-540-77050-3_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
