Verifying linear temporal specifications of constant-rate multi-mode systems
Logic in Computer Science
2023-04-28 v1 Computational Complexity
Formal Languages and Automata Theory
Abstract
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 model-checking 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.
Cite
@article{arxiv.2304.13816,
title = {Verifying linear temporal specifications of constant-rate multi-mode systems},
author = {Michael Blondin and Philip Offtermatt and Alex Sansfaçon-Buchanan},
journal= {arXiv preprint arXiv:2304.13816},
year = {2023}
}
Comments
appeared at LICS 2023