抽象的表现性与完整性
Expressiveness and Completeness in Abstraction
摘要：
我们研究了在模型检验的抽象理论中出现的两个表达性概念，发现它们在一般情况下是不可比较的。特别是，我们表明，根据最广泛使用的概念，类的Kripke模态转换系统是严格的表达比类的广义Kripke模态转换系统（一个广义的变种Kripke模态转换系统配备hypertransitions）。此外，我们调查的抽象框架的能力，证明一个公式与有限的抽象模型，一个属性被称为完整性。我们从一般的角度来解决完整性问题：它依赖于某些抽象参数的方式，以及它与表达性的关系。
英文摘要：
We study two notions of expressiveness, which have appeared in abstraction theory for model checking, and find them incomparable in general. In particular, we show that according to the most widely used notion, the class of Kripke Modal Transition Systems is strictly less expressive than the class of Generalised Kripke Modal Transition Systems (a generalised variant of Kripke Modal Transition Systems equipped with hypertransitions). Furthermore, we investigate the ability of an abstraction framework to prove a formula with a finite abstract model, a property known as completeness. We address the issue of completeness from a general perspective: the way it depends on certain abstraction parameters, as well as its relationship with expressiveness.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
