基于完备抽象解释的模型检验CTL公式研究

Abstraction plays a fundamental role in combating state-space explosion in model checking. In a complete abstract interpretation-based view, the authors reduce the state space of a Kripke structure in order to obtain a minimal abstract state translation system that strongly preserves a given tempora