FORMATS-FTRTFT 2004 START ConferenceManager    

Model-Checking for Weighted Timed Automata

Thomas Brihaye, Véronique Bruyère, Jean-François Raskin

Presented at Formal Modelling and Analysis of Timed Systems - Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT 2004), Grenoble, France, September 22-24, 2004


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.

START Conference Manager (V2.47.2)