Propositions de stage

Model Checking as Deduction

Encadrement :

Dale Miller, INRIA-Futurs and LIX, Ecole Polytechnique

Description du sujet

Model checking is characterized as an exhaustive check of some conditions within a model and it is usually not considered to be deduction. Recent work by McDowell & Miller & Tiu (in papers listed below) has illustrated that it is possible to strengthen traditional sequent calculus (a la Gentzen's LK and LJ calculi) so that exhaustive checking of conditions against a model (described using simple logical theories) can be explained as provability. For example, in this strengthen logic, it is possible to prove the negation of a formula if all checks of it against the model fail. Induction and co-induction have also been added to this logic to allow for some conclusions to be drawn even when models are infinite.

While the deductive approach should correspond well to model checking, this has yet to be confirmed in detail. Such confirmation is the goal of this stage.

The following questions can be considered in this project. Certainly not all of them need to be (or can be) done. They represent the kinds of questions that would help in understanding to what extent this recent work on strengthening of sequent calculus is a useful approach to representing and reasoning about model checking.

  1. Naive implementations of proof search supporting model checking reveals that often search will repeatedly explore extensions to a state even if that state and its extensions have already been explored. In other words, the naive approach explores the search spaces as if it is a tree, even when the search space is a DAG (directed-acyclic graph). Tabled deduction should provide a better approach. Is it, in fact, a good approach? Answering this questions does not necessarily involve an implementation.
  2. Given that model checking can be seen as deduction, there might be a new approach to dealing with abstractions of model, since logic should also provide a setting for writing down, proving, and using, high-level information about models. For example, statements about invariants and symmetries should be easy to state and prove in logic. Thus, by viewing model checking as deduction, we have one setting for checking models and for describing properties of models as a whole. Specifically, how can one handle symmetry, for example, in a model to improve model checking?
  3. Extended and serious example are available in the model checking literature. Confirming whether or not these work in the deduction setting is important. Work on a number of examples is an important part of any development of this subject. Examples are expected to illustrate problems with enumerating cyclic models, infinite models, unification modulo equalities, scheduling of constraints, etc.
  4. When model checking is completed, what is a good notion of proof regarding the property established?
  5. Model checking often needs to make use of "meta-level" variables to denote values that determine specific models but for which the actual value can be delayed. Logic variables and unification are a natural setting for exploring this aspect of "parametric" model checking. Experience with the Level0/1 prototype illustrates, however, that for unification to work properly in this setting, it must be extended. We envisage a rather general extension to unification that generalizes the notion of "unification under a mixed prefix" (see reference below).

PhD thesis topics are possible based on work done for this stage.

Bibliography

The following bibliography is represents work on the deductive system that should be compared to model checking. The literature on model checking is large and surveys can be found in popular texts and on the web.

  1. Encoding Transition Systems in Sequent Calculus, by Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Theoretical Computer Science, 294(3), 411-437 (2003). (DVI, PostScript, PDF).

  2. Cut-Elimination for a Logic with Definitions and Induction, by Raymond McDowell and Dale Miller. Theoretical Computer Science, volume 232, pages 91 - 119 (2000). (DVI, PostScript, PDF). Some comments and errata.

  3. Unification under a mixed prefix, by Dale Miller. Journal of Symbolic Computation, Vol. 14 (1992), 321-358. (DVI, PDF).

  4. A Proof Search Specification of the π-Calculus, by Alwen Tiu and Dale Miller. Proceedings of FGUC 2004: Foundations of Global Ubiquitous Computing. (PDF).

  5. The Bedwyr system for model checking over syntactic expressions by David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. CADE 2007: 21th Conference on Automated Deduction, Frank Pfenning, editor, LNAI 4603, pages 391-397. Springer, 2007. (pdf)

  6. Incorporating tables into proofs by Dale Miller and Vivek Nigam. CSL'07: Computer Science Logic, J. Duparc and T. A. Henzinger, editors, LNCS 4646, pages 466-480. Springer-Verlag. (PDF).

  7. Induction and Co-induction in Sequent Calculus, by Alberto Momigliano and Alwen Tiu. Proceedings of TYPES 2003, LNCS volume 3085, pages 293 - 308, Springer-Verlag, 2003. PDF

  8. A Logical Framework for Reasoning about Logical Specifications, by Alwen Tiu. PhD thesis, Penn State University, May 2004. PDF.