May, 2023

具有析取显式策略的交替时间μ演算

TL;DR本文将ATLES与fixpoint算子、策略分离扩展为具有非确定性控制的AMCDES,其可以灵活地表述时间性质,主要结果是ExpTime上限可满足检测(为ExpTime完全问题),并且Model Checking的上限是QP和NP∪coNP或NP,取决于具体策略的解释。