TITRE : Tableaux and Partial Model Synthesis
Context
Traditionally tableaux calculi constitute a method used to decide the satisfiability problems in the case of several logics, that is to answer to the question whether a formula of the given logic language is contradictory or not. Tableaux provide a constructive method, that not only gives a “Yes” or “No” answer to the question, but also, when the given formula is indeed satisfiable, provides an algorithm for the construction of an interpretation for the given logic where the formula is true: a model for it. Hence, when the formula is a specification of a system, tableaux are a tool for model synthesis.
In the case of modal logics, the interpretations -the so called “Kripke structures”- are labeled transition systems. As a consequence, they are particularly suitable to model systems, and modal formulae are useful to express specifications for the systems (that can be of different kinds, depending on the given modal logic).
When tableau calculi are used as a decision tool for satisfiability checking, the synthesis of a model satisfying a given formula is done “from scratch”. That is, the input to the tableaux algorithm is just the formula to be satisfied, but the construction of the satisfying model is not constrained at all. In other words, in the case of modal logics the satisfying transition systems built by the tableau may have any number of states and the transition relation may be any binary relation on that set of states respecting the frame conditions of the logic, provided that the output Kripke structure is indeed a model of the input formula.
However, model synthesis can be of interest also to complete an already given partial construction of a model, that therefore is also a part of the input. For instance, given a specification of a system SYS, given by means of a modal formula A expressing the conjunction of the properties that the system must have, some components of SYS, verifying some local properties, might have already been defined (possibly only partially, in their turn), but they need to be properly assembled to get the final model of the overall specification A. In this case the choice of the states and/or the transition relation is constrained by what has already been built.
In this framework the problem that the algorithm must solve can be formulated more precisely as follows:
« Given a partially constructed Kripke structure M, a designated state s in it, and an input formula A, build a completion M of the transition system M which satisfies the input formula A at the designated state s. »
Gereral aim
The general aim of the internship is the development of appropriate tableaux methods to solve such generic problem, starting with the case of basic modal logic (aka, the logic K), then moving to the more complex case of linear and branching time temporal logics, such as LTL and CTL, whose languages are generally used to specify the behavior of reactive systems.
In the case of partial model synthesis for basic modal logic several cases may be studied :
- The transition system is given, by means of a set of states S and a transition relation T on S, but the valuation of the atomic propositions (or state labelling function) is not.
- Only (possibly proper) subsets S’ of S and T’ of T are given, however the valuation of the atomic proposition on S’ is completely defined.
- The state space S and the valuation of the atomic propositions are completely defined but the transitions are only partly defined, or not at all.
- Combinations of the previous cases.
For the case of linear temporal logic LTL the following versions of the partial model synthesis problem may be considered:
- The input consists of the formula to be satisfied and of a linear model (interpretation) with a partially defined state labelling function.
- The semantical part of the input is a partially defined Kripke structure (a graph) containing a
path (i.e. a linear sub-structure) that is to satisfy the input formula.
Modality
The work will be realized by the student in a relatively autonomous way, however regular contacts with the advisors will occur, in particular regular meetings with the local advisor (S. Cerrito) will be organized.
Contact
- Serenella CERRITO (PR Univ. Évry, IBISC équipe COSMO) – serenellaDOTcerritoATuniv-evryDOTfr
Partial bibliography (other works in the relevant literature will be suggested by the advisors as the work proceeds):
- Demri, V. Goranko and M. Lange, Temporal Logics in Computer Science, Cambridge Tracts in Theoretical Computer Science,Cambridge University Press, 2016.
- Blackburn, M. de Rijke, Y. de Venema, Modal Logic, Cambridge University Press, 2014
- Date de l’appel : 31/01/2021
- Statut de l’appel : Pourvu
- Encadrement coté IBISC : Serenella CERRITO (PR Univ. Évry, IBISC équipe COSMO), Valentin GORANKO (Professeur Stockholm University)
- Sujet de stage niveau Master 2 (format PDF)
- Web équipe COSMO
