Top

Journal of Automated Reasoning

Published in:

18-06-2018

A Proof Theory for Model Checking

Authors: Quentin Heath, Dale Miller

Published in: Journal of Automated Reasoning | Issue 4/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

next article Linear Numeral Systems

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297–347 (1992)MathSciNetCrossRef

Baelde, D.: A linear approach to the proof-theory of least and greatest fixed points. PhD thesis, Ecole Polytechnique, (2008)

Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Comput. Logic (2012). https://doi.org/10.1145/2071368.2071370 MathSciNetCrossRefMATH

Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning F. (ed.) 21th Conference on Automated Deduction (CADE), number 4603 in Lecture Notes in Artificial Intelligence, pp. 391–397, New York, (2007). Springer

Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz N., Voronkov A. (eds.) International Conference on Logic for Programming and Automated Reasoning (LPAR), volume 4790 of Lecture Notes in Computer Science, pp. 92–106, (2007)

Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press, Cambridge (2008)MATH

Chihani, Z., Miller, D., Renaud, F.: A semantic framework for proof evidence. J. Autom. Reason. 59, 287–330 (2017). https://doi.org/10.1007/s10817-016-9380-6 MathSciNetCrossRefMATH

Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56–68 (1940)MathSciNetCrossRef

Clark, K.L.: Negation as failure. In: Gallaire, J., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Plenum Press, New York (1978)CrossRef

10.

Delande, O., Miller, D., Saurin, A.: Proof and refutation in MALL as a game. Ann. Pure Appl. Logic 161(5), 654–672 (2010)MathSciNetCrossRef

11.

Emerson, E. A.: The beginning of model checking: A personal perspective. In: Grumberg O., Veith H. (eds.) 25 Years of Model Checking–History, Achievements, Perspectives, volume 5000 of Lecture Notes in Computer Science, pp. 27–45. Springer, (2008)

12.

Gacek, A., Miller, D., Nadathur, G.: Combining generic judgments with recursive definitions. In Pfenning F. (ed.) 23th Symposium on Logic in Computer Science, pp. 33–44. IEEE Computer Society Press (2008)

13.

Gacek, A., Miller, D., Nadathur, G.: A two-level logic approach to reasoning about computations. J. Autom. Reason. 49(2), 241–273 (2012)MathSciNetCrossRef

14.

Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1935)

15.

Gentzen, G.: New version of the consistency proof for elementary number theory. In Szabo M. E. (ed.) Collected Papers of Gerhard Gentzen, pp. 252–286. North-Holland, Amsterdam, 1938. Originally published (1938)

16.

Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50, 1–102 (1987)MathSciNetCrossRef

17.

Girard, J.-Y.: Towards a geometry of interaction. In: Categories in Computer Science, volume 92 of Contemporary Mathematics, pp. 69–108. AMS, (1987)

18.

Girard, J.-Y.: A new constructive logic: classical logic. Math. Struct. Comp. Sci. 1, 255–296 (1991)MathSciNetCrossRef

19.

Girard, J.-Y.: A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu, (1992)

20.

Heath, Q., Miller, D.: A framework for proof certificates in finite state exploration. In: Kaliszyk C., Paskevich A. (eds.) Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, number 186 in Electronic Proceedings in Theoretical Computer Science, pp. 11–26. Open Publishing Association, (2015)

21.

Kanovich, M.I.: Petri nets, Horn programs, Linear Logic and vector games. Ann. Pure Appl. Logic 75(1–2), 107–135 (1995)MathSciNetCrossRef

22.

Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoret. Comput. Sci. 410(46), 4747–4768 (2009)MathSciNetCrossRef

23.

Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, Berlin (2012)MATH

24.

McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoret. Comput. Sci. 232, 91–119 (2000)MathSciNetCrossRef

25.

McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Logic 3(1), 80–136 (2002)MathSciNetCrossRef

26.

McDowell, R., Miller, D., Palamidessi, C.: Encoding transition systems in sequent calculus. Theoret. Comput. Sci. 294(3), 411–437 (2003)MathSciNetCrossRef

27.

Miller, D.: Foundational proof certificates. In: Delahaye D., Paleo B. W. (eds.) All about Proofs, Proofs for All

28.

Miller, D., Nigam, V.: Incorporating tables into proofs. In: Duparc J., Henzinger T. A. (eds.) CSL 2007: Computer Science Logic, volume 4646 of Lecture Notes in Computer Science, pp. 466–480. Springer, (2007)

29.

Miller, D., Saurin, A.: A game semantics for proof search: Preliminary results. In: Proceedings of the Mathematical Foundations of Programming Semantics (MFPS05), number 155 in Electronic Notes in Theoretical Computer Science, pp. 543–563, (2006)CrossRef

30.

Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Logic 6(4), 749–783 (2005)MathSciNetCrossRef

31.

Miller, D., Tiu, A.: Extracting proofs from tabled proof search. In: Gonthier G., Norrish M. (eds.) Third International Conference on Certified Programs and Proofs, number 8307 in Lecture Notes in Computer Science, pp. 194–210, Melburne, Australia, (2013). SpringerCrossRef

32.

Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cliffs (1989)MATH

33.

Ramakrishna, Y. S., Ramakrishnan, C. R., Ramakrishnan, I. V., Smolka, S. A., Swift, T., Warren, D. S.: Efficient model checking using tabled resolution. In: Proceedings of the 9th International Conference on Computer Aided Verification (CAV97), number 1254 in Lecture Notes in Computer Science, pp. 143–154, (1997)CrossRef

34.

Ramakrishnan, C.: Model checking with tabled logic programming. ALP News Lett. (2002)

35.

Sangiorgi, D., Milner, R.: The problem of “weak bisimulation up to”. In: CONCUR, volume 630 of Lecture Notes in Computer Science, pp. 32–46. Springer, (1992)

36.

Sangiorgi, D., Walker, D.: \(\pi \)-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)MATH

37.

Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi M. (ed.) 8th Symposium on Logic in Computer Science, pp. 222–232. IEEE Computer Society Press, IEEE, (1993)

38.

Schwichtenberg, H.: Proof theory: Some applications ofcut-elimination. In: Barwise J. (ed.) Handbook ofMathematical Logic, volume 90 of Studies in Logic and theFoundations of Mathematics, pp. 739–782. North-Holland,Amsterdam, (1977)

39.

Tiu, A., Miller, D.: A proof search specification of the \(\pi \)-calculus. In: 3rd Workshop on the Foundations of Global Ubiquitous Computing, volume 138 of ENTCS, pp. 79–101, (2005)

40.

Tiu, A., Miller, D.: Proof search specifications of bisimulation and modal logics for the \(\pi \)-calculus. ACM Trans. Comput. Logic (2010). https://doi.org/10.1145/1656242.1656248 MathSciNetCrossRefMATH

41.

Tiu, A., Momigliano, A.: Cut elimination for a logic with induction and co-induction. J. Appl. Logic 10(4), 330–367 (2012)MathSciNetCrossRef

42.

Tiu, A., Nadathur, G., Miller, D.: Mixing finite success and finite failure in an automated prover. In: Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL’05), pp. 79–98, (2005)

Title: A Proof Theory for Model Checking
Authors: Quentin Heath
Dale Miller
Publication date: 18-06-2018
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 4/2019
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9475-3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 4/2019

QPCF: Higher-Order Languages and Quantum Circuits

Linear Numeral Systems

Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants

Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic

Premium Partner