A Proof Theory for Model Checking: An Extended Abstract

Quentin Heath
(LIX, Ecole Polytechnique)
Dale Miller
(Inria Saclay and LIX, Ecole Polytechnique)

While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide an appealing foundation for model checking. Since the emphasis of model checking is on establishing the truth of a property in a model, we rely on the proof theoretic notion of additive inference rules, since such rules allow provability to directly describe truth conditions. Unfortunately, the additive treatment of quantifiers requires inference rules to have infinite sets of premises and the additive treatment of model descriptions provides no natural notion of state exploration. By employing a focused proof system, it is possible to construct large scale, synthetic rules that also qualify as additive but contain elements of multiplicative inference. These additive synthetic rules—essentially rules built from the description of a model—allow a direct treatment of state exploration. This proof theoretic framework provides a natural treatment of reachability and non-reachability problems, as well as tabled deduction, bisimulation, and winning strategies.

In Iliano Cervesato and Maribel Fernández: Proceedings Fourth International Workshop on Linearity (LINEARITY 2016), Porto, Portugal, 25 June 2016, Electronic Proceedings in Theoretical Computer Science 238, pp. 1–10.
Published: 17th January 2017.

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