Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A Proof Theory for Model Checking

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

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

    Article  MathSciNet  Google Scholar 

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

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

    Article  MathSciNet  MATH  Google Scholar 

  4. 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

  5. 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)

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

    MATH  Google Scholar 

  7. 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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  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)

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  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). Springer

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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  Google Scholar 

  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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  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)

Download references

Acknowledgements

We thank the anonymous reviewers of an earlier draft of this paper for their valuable comments. This work was funded by the ERC Advanced Grant ProofCert.

Author information

Authors and Affiliations

  1. Inria-Saclay, LIX/Ecole Polytechnique, and CNRS UMR 7161, Palaiseau, France

    Quentin Heath & Dale Miller

Authors
  1. Quentin Heath
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dale Miller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dale Miller.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Heath, Q., Miller, D. A Proof Theory for Model Checking. J Autom Reasoning 63, 857–885 (2019). https://doi.org/10.1007/s10817-018-9475-3

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-018-9475-3

Keywords

Search

Navigation