Verifying linear temporal specifications of constant-rate multi-mode systems

Constant-rate multi-mode systems (MMS) are hybrid systems with finitely many modes and real-valued variables that evolve over continuous time according to mode-specific constant rates. We introduce a variant of linear temporal logic (LTL) for MMS, and we investigate the complexity of the modelchecking problem for syntactic fragments of LTL. We obtain a complexity landscape where each fragment is either P-complete, NP-complete or undecidable. These results generalize and unify several results on MMS and continuous counter systems.

proof indirectly shows that the model checking problem is undecidable for formulas of the form (Z 1 ∨• • •∨Z n ) U x target where each Z i is a possibly unbounded zone. We strengthen this result by using bounded zones only.