Model checking metric temporal logic over automata with one counter

Abstract

We study the decidability status of the model checking problem for Metric Temporal Logic over models with one counter variable whose value can increase and decrease. This includes 1-counter machines with zero tests, 1-dimensional vector addition systems with states, and weighted automata with weights in the integers. We show that model checking of non-deterministic models is undecidable, even if we restrict the intervals used in the logic to be of the form (- ∞,0] and [0, ∞). On the positive side, we show that model checking of deterministic models is decidable. © 2013 Springer-Verlag Berlin Heidelberg.