Model Checking One-clock Priced Timed Automata

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities....

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2008-06, Vol.4, Issue 2 (2:9)
Main Authors: Bouyer, Patricia, Larsen, Kim G., Markey, Nicolas
Format: Article
Language:English
Subjects:
Computer Science
computer science - computational complexity
computer science - computer science and game theory
computer science - logic in computer science
f.1.1
f.3.1
Logic in Computer Science
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model-checking WMTL, LTL with cost-constrained modalities, is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).
ISSN:1860-5974
1860-5974
DOI:10.2168/LMCS-4(2:9)2008