Expressiveness and Completeness in Abstraction

Maciej Gazda
(Eindhoven University of Technology)
Tim A.C. Willemse
(Eindhoven University of Technology)

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.

In Bas Luttik and Michel A. Reniers: Proceedings Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics (EXPRESS/SOS 2012), Newcastle upon Tyne, UK, September 3, 2012, Electronic Proceedings in Theoretical Computer Science 89, pp. 49–64.
Published: 12th August 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.89.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org