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.

翻译：常速率多模式系统(MMS)是一类混合系统，具有有限个模式，实值变量根据模式特定的常速率在连续时间上演化。我们针对MMS引入一种线性时序逻辑(LTL)的变体，并研究了LTL语法片段上的模型检测问题的复杂性。我们获得了一个复杂性图谱，其中每个片段要么是P完全、NP完全，要么是不可判定的。这些结果推广并统一了关于MMS和连续计数器系统的若干结论。