Costs are expensive! (English) Zbl 1142.68045
Raskin, Jean-François (ed.) et al., Formal modeling and analysis of timed systems. 5th international conference, FORMATS 2007, Salzburg, Austria, October 3–5, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75453-4/pbk). Lecture Notes in Computer Science 4763, 53-68 (2007).
Summary: We study the model-checking problem for WMTL, a cost-extension of the linear-time timed temporal logic MTL, that is interpreted over weighted timed automata. We draw a complete picture of the decidability for that problem: it is decidable only for the class of one-clock weighted timed automata with a restricted stopwatch cost, and any slight extension of this model leads to undecidability. We finally give some consequences on the undecidability of linear hybrid automata.
For the entire collection see [Zbl 1138.68007].
For the entire collection see [Zbl 1138.68007].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 03D05 | Automata and formal grammars in connection with logical questions |
| 03D35 | Undecidability and degrees of sets of sentences |
| 68Q45 | Formal languages and automata |
