期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2012
卷号：89
页码：49-64
DOI：10.4204/EPTCS.89.5
出版社：Open Publishing Association
摘要：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.
