A Proof Theory for Model Checking: An Extended 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 pro...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2017-01-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1701.04915v1 |
| _version_ | 1817968051717406720 |
|---|---|
| author | Quentin Heath Dale Miller |
| author_facet | Quentin Heath Dale Miller |
| author_sort | Quentin Heath |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T20:03:56Z |
| format | Article |
| id | doaj.art-549bcc134e6249fa9dc89592d85edd8a |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T20:03:56Z |
| publishDate | 2017-01-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-549bcc134e6249fa9dc89592d85edd8a2022-12-22T02:32:06ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-01-01238Proc. LINEARITY 201611010.4204/EPTCS.238.1:9A Proof Theory for Model Checking: An Extended AbstractQuentin Heath0Dale Miller1 LIX, Ecole Polytechnique 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.http://arxiv.org/pdf/1701.04915v1 |
| spellingShingle | Quentin Heath Dale Miller A Proof Theory for Model Checking: An Extended Abstract Electronic Proceedings in Theoretical Computer Science |
| title | A Proof Theory for Model Checking: An Extended Abstract |
| title_full | A Proof Theory for Model Checking: An Extended Abstract |
| title_fullStr | A Proof Theory for Model Checking: An Extended Abstract |
| title_full_unstemmed | A Proof Theory for Model Checking: An Extended Abstract |
| title_short | A Proof Theory for Model Checking: An Extended Abstract |
| title_sort | proof theory for model checking an extended abstract |
| url | http://arxiv.org/pdf/1701.04915v1 |
| work_keys_str_mv | AT quentinheath aprooftheoryformodelcheckinganextendedabstract AT dalemiller aprooftheoryformodelcheckinganextendedabstract AT quentinheath prooftheoryformodelcheckinganextendedabstract AT dalemiller prooftheoryformodelcheckinganextendedabstract |