Model-Checking for Weighted Timed Automata

10 years 5 months ago
Model-Checking for Weighted Timed Automata
We study the model-checking problem for weighted timed automata and the weighted CTL logic by the bisimulation approach. Weighted timed automata are timed automata extended with costs on both edges and locations. When the costs act as stopwatches, we get stopwatch automata with the restriction that the stopwatches cannot be reset nor tested. The weighted CTL logic is an extension of TCTL that allow to reset and test the cost variables. Our main results are (i) the undecidability of the proposed model-checking problem for discrete and dense time, (ii) its PSpace-Completeness in the discrete case for a slight restriction of the logic, (iii) the precise frontier between finite and infinite bisimulations in the dense case for the subclass of stopwatch automata.
Thomas Brihaye, Véronique Bruyère, J
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Authors Thomas Brihaye, Véronique Bruyère, Jean-François Raskin
Comments (0)