The Complexity of Linear Temporal Verification for Continuous Counter Systems

Constant-rate multi-mode systems (MMSs) are hybrid systems with finitely many modes and real-valued variables that evolve over continuous time according to mode-specific constant rates. Equivalently, they correspond to continuous vector addition systems (VASs), where counters may become negative. We introduce a variant of linear temporal logic (LTL) for MMS, and we investigate the complexity of the model-checking problem for syntactic fragments of LTL. We obtain a complexity trichotomy: Each fragment is either P-complete, NP-complete, or undecidable. Since our logic can constrain the counters to remain non-negative, it further applies to continuous VAS. Thus, our results yield a framework for MMS and continuous VAS that generalizes and unify several existing results.