Skip to Main content Skip to Navigation
Journal articles

A proof theory for model checking

Quentin Heath 1 Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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 additive inference rules since these provide a natural description of truth values via inference rules. Unfortunately, using these rules alone can force the use of inference rules with an infinite number of premises. In order to accommodate more expressive and finitary inference rules, we also allow multiplicative rules but limit their use to the construction of additive synthetic inference rules: such synthetic rules are described using the proof-theoretic notions of polarization and focused proof systems. This framework provides a natural, proof-theoretic treatment of reachability and non-reachability problems, as well as tabled deduction, bisimulation, and winning strategies.
Document type :
Journal articles
Complete list of metadata

Cited literature [42 references]  Display  Hide  Download

https://hal.inria.fr/hal-01814006
Contributor : Dale Miller <>
Submitted on : Tuesday, June 12, 2018 - 5:25:27 PM
Last modification on : Friday, April 30, 2021 - 10:02:40 AM
Long-term archiving on: : Thursday, September 13, 2018 - 11:55:41 PM

File

hal.pdf
Files produced by the author(s)

Identifiers

Citation

Quentin Heath, Dale Miller. A proof theory for model checking. Journal of Automated Reasoning, Springer Verlag, 2019, 63 (4), pp.857-885. ⟨10.1007/s10817-018-9475-3⟩. ⟨hal-01814006⟩

Share

Metrics

Record views

360

Files downloads

483