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

04/26/2023
by   Michael Blondin, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset