Model Checking One-clock Priced Timed Automata

TL;DR

This paper investigates the complexity of model checking one-clock priced timed automata against cost-constrained temporal logics, establishing PSPACE-completeness for WCTL and decidability conditions for WMTL.

Contribution

It proves that model checking one-clock priced timed automata with WCTL is PSPACE-complete and identifies conditions for decidability of WMTL.

Findings

Model checking WCTL is PSPACE-complete for one-clock priced timed automata.

Model checking WMTL is decidable only with a single clock and a single stopwatch cost variable.

Undecidability arises when models have three or more clocks.

Abstract

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