Patricia Bouyer ; Kim G. Larsen ; Nicolas Markey - Model Checking One-clock Priced Timed Automata

lmcs:828 - Logical Methods in Computer Science, June 20, 2008, Volume 4, Issue 2 - https://doi.org/10.2168/LMCS-4(2:9)2008
Model Checking One-clock Priced Timed Automata

Authors: Patricia Bouyer ; Kim G. Larsen ; Nicolas Markey

    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}).


    Volume: Volume 4, Issue 2
    Published on: June 20, 2008
    Accepted on: June 25, 2015
    Submitted on: September 20, 2007
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,Computer Science - Computer Science and Game Theory,F.1.1,F.3.1

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-319-10575-8_29
    • 10.1007/978-3-319-10575-8_29
    • 10.1007/978-3-319-10575-8_29
    • 10.1007/978-3-319-10575-8_29
    Model Checking Real-Time Systems
    Patricia Bouyer ; Uli Fahrenberg ; Kim Guldstrand Larsen ; Nicolas Markey ; Joël Ouaknine ; James Worrell ;

    19 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 395 times.
    This article's PDF has been downloaded 201 times.