一句话：为常速率多模式系统引入 LTL 变体，并刻画其模型检测片段的复杂度版图：P-完全、NP-完全或不可判定。
常速率多模式系统（MMS）是一类混合系统，具有有限多个模式与实值变量，变量按模式相关常速率随时间连续演化。论文为 MMS 引入一种线性时序逻辑（LTL）变体，并研究其语法片段上模型检测问题的复杂度。作者获得复杂度版图：每个片段要么是 P-完全、要么 NP-完全、要么不可判定。这些结果推广并统一了若干关于 MMS 与连续计数器系统的已有结果。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{BlondinOS23,
title = {Verifying linear temporal specifications of constant-rate multi-mode systems},
author = {Michael Blondin and Philip Offtermatt and Alex Sansfaçon-Buchanan},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175721}
}