|
Main /
TechnicalProject managementIn order to work on specific tasks, the appropriate participants of the project will meet regularly in small working groups. Global project meetings will take place once a year in which external colleagues might be invited to share expertise. They will be registered on the web page. Coordination: The project will be coordinated by Didier Galmiche (LORIA - Nancy) helped in this task by the two heads of the partner teams : Ph. Balbiani (IRIT - Toulouse) and S. Demri (LSV – Ens Cachan). In order to fulfill the objectives of the project, they shall evaluate the work progress and adapt the efforts according to the difficulties. The coordinator and the responsibles will plan the meetings and make a review of the work at each meeting. Scientific programmeThis programme is dedicated, as explained in previous sections, to the foundational study of separation and update of resources from non-explored but challenging research directions that are the specification of systems and resource properties and their verification through the construction of proofs and refutations usable in the process of system developments. In order to make significant steps towards achieving the previously stated long term goal, we need to make a renewed and sustained effort at understanding the foundations of logics for separation and update. Such a deep and fundamental study can be carried out from the following three complementary standpoints: I) Resource models and high-level (resource) properties
II) Separation and update resource logics and their decidable fragments
III) Proof systems for separation and update resource logics
Description by taskWe can distinguish three main scientific tasks divided as follows: Task 1: Resource : models and high-level properties
Task 2: Separation and update for dynamic resources: from expressivity to decidability
Task 3: Proof systems for separation and update logics
Task 1: Resources: Models and High-level PropertiesResponsible: Stéphane Demri (LSV); Main partners: IRIT, LORIA, LSV Models from Separation Logic (SL) are based on memory heaps (aggregation of memory cells) composed through disjoint union. This type of model can be considered as a concrete model of the resources shared by programs with pointers [Reynolds02]. However, the language of the logic SL has been used to represent separation properties on a much wider class of models, some being concrete models and other more abstract. The study of abstract and concrete resource models and mainly their relationships is central here in connection with the high-level properties we want to express and reason about. The main goals of this task is not only to integrate notions coming from abstract models (e.g. invertibility, non-aggregation, etc.) or other resource logics (production/consumption of money tokens) into existing or variants of existing resource models but also to integrate temporal aspects into Boolean BI and SL-like logics in order propose a framework to model interaction through interleaved and lock-controlled sharing of resources. We shall investigate new ressource models having in mind to deal with differents aspects: descriptive / static / spatial aspects (e.g.,"structure s is a linked-list without cycles"); evolution / dynamic / temporal aspects (e.g., "the system repeatedly evolves towards state where non-referenced memory cells are garbage-collected"); quantitative aspects (e.g., "every ten read operations to the database, the system checks for a pending write operation"). Moreover we aim at dealing with different classes of properties: quantitative properties (typically, check that the output of a program is an ordered list); dynamic properties about the evolution of resources/data: temporal constraints between events, possibly with quantitative aspects, properties about alternative models (typically, specify what happens when a node is down in a network). The substasks below concern the investigation of the mathematical properties of new enriched abstract resource models (subtask 1.1), the development of temporal constraints on resource models (subtask 1.2) and the design of specification languages with quantitative aspects, such as arithmetical constraints (subtask 1.3). Subtask 1.1: Abstract resource models Responsible: Dominique Larchey-Wendling (LORIA); Main partners: IRIT, LORIA, LSV Following the initial definitions of abstract and concrete models, we first point out that the distinction between them should be given some nuance. Abstraction is the process by which one tries to distinguish the essential properties from the accessory properties, or the high-level properties from the low-level ones. Hence, the modeling process is itself an abstraction: the memory heap of SL is a function from places to data, not an array of memory chips. On the other hand, once linear logic was singled out and characterized as a logic of interest, people tried to interpret its formulae on models which where more concrete that phase spaces such as for instance production/consumption models like Petri nets [Engberg&Winskel90]. So abstraction and concretization are the two faces of a same coin. There is a back and forth movement between abstract and concrete models and we want to use it to capture high-level properties of resources and the logical languages suitable for such a task: we abstract concrete models to try to obtain completeness of some proof-system. We may then single out a new property which does not appear in the original concrete model but is expressible in the logic, and is thus essential for completeness. Then, we may try to extend or generalize the concrete models so that the new property is represented in the concrete models. Then the whole process starts again. For instance, when considering partial monoids as an abstraction of the SL models (memory heaps and aggregation), it appears that the notion of invertible resource is definable within the logical language of SL, even if memory heaps only contain one invertible resource, the empty heap which is the neutral element of the monoid. Then, it seems desirable to take invertibility of some resource into account and design concrete models which generalize the memory heap and which contain non-trivial invertible resources. The guideline of the methodology we use is neither purely the logic which may be subject to change or extension, nor purely the model which maybe subject to concretization or abstraction. We wish to have properties expressed in a logical language for which an analytical proof-system can be designed and the question of completeness of the class of models can be stated and eventually proved. A typical subject that we wish to explore lies in the difference between interaction and interference: when two processes interact or interfere, it is vitally important that the resources they share should be maintained in a coherent state. About this last point, Static SL for example ensures coherence by stating that no resource is shared between the processes. Thus coherence is obviously maintained because the shared resource is empty and thus, its state cannot evolve: in fact there is no interference at all. Then, adding temporal operators to SL, it is possible to model the evolution of resource separation over time: a given resource always belongs to at most one process at some given time but this process may change over time. Hence, process interact by exchanging resource and, usually, coherence is ensured by some locking mechanism (mutual exclusion) and the fact that the processes themselves behave in an internally coherent way on their privately owned resources. By micro-managing locking, we can model systems where processes interact in a coherent way. But from a macroscopic point of view, considering locks as a hidden or internal mechanism, these processes interfere in a coherent way. A typical model for such process interaction scheme are the threads of an operating system kernel. We wish to abstract this micro-management of locking and design models and logics which may prove coherence properties of interference without necessarily going down the microscopic level of locking. This would allow the user of such logics to design modular proofs that do not depend too heavily on the particular mechanisms used to implement coherence, like mutual exclusion for example. Moreover, it is observed that mutual exclusion is actually not the only way to ensure coherence. We eventually wish to design models where interference is not reducible to interaction based on resource exchange and locking. In abstract monoidal models, some resources may be invertible whereas other are not. And resource may contain some invertible part and some non-invertible part. These notions which appear in the context of abstract models do not have a very clear computational interpretation for the moment. A possible way to extend existing models with some non-trivial notion of invertibility would be for example to start from some variant of Petri nets where some tokens would be subject to loans, like for instance money. Processes would be able to borrow an unlimited amount of money, even exchange money between themselves as well as ordinary tokens, but in the end of the computation, the total amount of borrowed money should be returned, invertible resource being thus represented by debt or credit. A complementary task consists in designing models where the monoidal composition is not an aggregation: a o b = e does not entail a=b=e, where e is the monoidal unit. In a model like MBI [Pym&Tofts06], resources are processes endowed with a specific resource context and the monoidal operation is the parallel composition of SCCS. It is an example of interpretation of SL operators within a more general context. Resource trees [Biri&Galmiche07] are another example of interpretation of SL on a hybrid model which mixes the concrete model of static spatial logic [Caires&Cardelli03] and an abstract monoidal model which live at the level of nodes and interacts with the concrete model. We wish to design concrete models of such kind, integrating notions that appear at the abstract level. Our main objectives in this subtask are:
Subtask 1.2: Temporal constraints and resource evolution Responsible: Stéphane Demri (LSV); Main partners: IRIT, LORIA, LSV Specification languages for stating properties of resources usually cannot express dynamic properties that can be useful for instance to specify properties of executions of programs with pointers. In Hoare-like proof systems, deduction of new triples for composed instructions provides the most dynamic aspects. In this subtask, our aim is to provide a temporal dimension to specify the behaviour of resources. Indeed, there is a need to design languages for specifying sequences of resources and to verify such properties on computer systems with resources. A standard way to do so, is to design a temporal logic whose underlying assertion language speaks about resources. Indeed, since [Pnueli77], temporal logics are used as specification languages for formal specification of programs. We shall design temporal logics to express evolution of memory states with underlying language variants of separation logic since separation logic is a static logic for program annotation [Reynolds02]. Extending the scope of application of separation logic to standard temporal logic-based verification techniques has many potential interests. For example, it provides a rich underlying assertion language where properties more complex than accessibility can be stated, see e.g.[Yahavetal03]. The originality of the approach we advocate and for which a first attempt can be found in [Brochenin&Demri&Lozes09] (LSV partners) consists in taming rich interactions between temporal constraints and local constraints about memory states by designing automata-based techniques in which deduction methods can be used. We follow an approach similar to [Bennett&Wolter&Zakharyaschev02,Balbiani&Condotta02] (IRIT partners) but for different spatial domains that are related to resource models such as memory states. In the same line, we shall design separation logics including various modalities in order to deal for example with locations or temporality [Biri&Galmiche07] (LORIA partners). The main point is to compare and share results about the specification of properties of programs with pointers. Our main objectives are:
Subtask 1.3: Separation and quantitative properties Responsible: Daniel Méry (LORIA); Main partners: LORIA, LSV Many interesting properties of real-life programs (termination, correctness, sortedness, ...) depend on numerical aspects of their inputs. Therefore, there is an actual need to study arithmetic extensions of SL (in the presence of recursive predicates representing data structures such as lists or trees) from a proof-theoretic perspective, all the more since the theorem-proving approach has been left aside so far (cf. sections 2.1 and 2.2). A major issue we need to address is to devise analytic proof-methods (for example in tableau or sequent style) for various quantitative extensions of resource logics. Our starting point is the work on SL in [Galmiche&Mery09] which we expect to extend so as to allow a joint and internal (non ad-hoc) treatment of recursive predicates and integer constraints expressed in the Presburger arithmetic. In this regard, we need to find, inside the proof-search process, some way of dealing with predicates representing recursively defined data structures on one hand, and with integer constraints expressed in the Presburger arithmetic on the other hand. One valuable expected contribution of having such an analytic proof-search method is that it would help us identify, among all the conditions required to characterize provability in Separation Logic, those that are purely specific to the particular nature of the underlying heap model and those that could be more widely applicable to other resource logics. Such a clear view of how the heap model and the separation operators exactly interact would then allow the proof-search method to be more flexible, making it easier to adapt to other resource logics. Further investigations could then lead us to consider more general recursive data structures (finitary branching trees, for example) and resources composition other than disjoint union of heaps (such as the composition of two distinct trees which requires merging branches that are similar in both trees). Another difficult problem we aim to study is to identify new decidable fragments for quantitative Separation Logic which are more expressive than the purely existential fragment. Moreover, we preferentially would like to characterize these decidable fragments through a proof-theoretic approach. Recently, an interesting fragment of plain SL with one selector, called the positive fragment, has been shown decidable [Galmiche&Mery09], the full logic being undecidable as shown in [Brochenin&Demri&Lozes08]. This particular fragment is more general than the purely existential fragment and is a good starting point for extending plain SL with Presburger arithmetic constraints and recursive predicates. However, the main challenge in order to tackle the decidability problem for more general resource logics that include both separation, recursive predicates and Presburger arithmetic is to find some criterion for which the proof-search method is guaranteed to terminate. One advantage of studying decidability via an analytic proof-search method is that the input (the formula to prove or disprove) does not have to be in any kind of prenex form. Therefore, such an approach can be used to identify decidable fragments in intuitionistic variants of resource logics (BI + PA, for example) for which quantifier elimination cannot be performed (because negation does not commute with the separation operator, for example). Let us remark that because many useful properties of real data structures depend on numerical values that may themselves be stored as parts of these data structures, designing analytic proof-methods and proving decidability results in the context of recursive and arithmetic extensions of SL is by no means trivial and is more than just a matter of combining well-known decision procedure and decidability results for the underlying theories. On the contrary, one needs a deep understanding of the intricate intertwining between arithmetic constraints and recursive predicates in order to take it into account. Our main objectives in this subtask are:
The complementary expertise of LORIA and LSV partners on proof search and decidability in this perspective is a key point for this work. Task 2: Separation and Update: from Expressivity to DecidabilityResponsible: Philippe Balbiani (IRIT); Main partners: IRIT, LORIA, LSV Indeed, this is a genuine challenge to be able to combine properties of different nature. Finally, it pays sometimes to consider properties in more abstract models in order to generalize symbolic representations of resources/data and also proof methods. The expression of (static, dynamic or high-level) properties, their combination or their abstraction are performed via adequate non-classical logics for which the precise nature and novelty will be described in the project. However, the non-classical logics we shall consider are among resource logics, modal logics, temporal logics and logics with updates. As said before about resource models, we aim at developing extensions or variants of separation logics with different modalities and constraints: locations or places, temporal constraints and also with quantitative properties, recursion or data. In this context the main challenge is the study of the relationship and possible mix between separation and update on order to tackle not only with static resources but also dynamic resources. This original task covers several aspects from study of the expressivity to study of decidable logical fragments. The substasks below concern the exploration of the map of resource logics (subtask 2.1), the study of the possible mix of separation and modalities for updates (subtask 2.2) and the design of fragments of separation and update logics for which validity problem and satisfiability are decidable (subtask 2.3). Subtask 2.1: Exploring the map of resource logics Responsible: Dominique Larchey-Wendling (LORIA); Main partners: LORIA, LSV Our project will lead us to consider various logics either viewed by their proof-systems or their models. Some may be extensions of other logics by the addition of new operators (like a time modality for example) and other are fragments composed of formulae of particular shapes, restriction of the use of modalities or quantifiers, etc. We aim at being able to classify logics according to different criteria like decidability, complexity, inclusion, expressivity. For this classification goal, we will use two families of tools that are translations and embeddings on the one hand and bisimulation on the other hand. Embedding a logic into another one is a process that takes place at the syntatic level but it also involves semantical consideration as explained later. The idea is to encode formulae of one logic into formula of another one and to show that this encoding preserves both validity and refutability (if the embedding is sought to be faithful). Once an embedding is proved faithful, relative decidability and complexity results come for free. For instance, we first found a faithful embedding [Galmiche&Larchey06] of S4 within Boolean BI and thus, we knew that the complexity of Boolean BI must be at least PSPACE, should it be decidable. Later, we found [Larchey&Galmiche09] an unexpected embedding of (intuitionistic) BI into Boolean BI (on the class of monoidal models). Finally, we proved the embedding of a fragment of linear logic into Boolean BI [Larchey&Galmiche10] holding on a wide range of models including the monoidal model, the relational model and the heap model. As a consequence, we obtained the undecidability of Boolean BI, also an unexpected result as SL had been proved decidable on some models [Calcagno&Yang&OHearn01]. In general, the soundness of an embedding can be obtained by proof-transformation: show how to transform every proof of a formula of logic A into a proof of the corresponding formula of logic B. For this aim, it is usually much easier if the two logics are provided a proof-system of the same nature: two Hilbert type proof-systems, two sequent proof-systems, two tableaux proof-systems, etc. Proving that a logic A is faithfully embedded into logic B might also involve the transformation of counter-models of formulae of the logic A into countermodels of formulae of the logic B. It may be possible that the models of B are strictly more general than the models of A, but the situation is not often that straightforward. Sometimes, it might not be possible to transform a counter-model in the logic A into an isomorphic structure which is a countermodel in the logic B. In this case, we can use bisimulation. Bisimilarity is a relation between models that expresses the fact that two structures cannot be observably distinguished: observation is done by interaction with the structures using for example specific transactions, composition/decompositions and atomic observation operators. If no same sequence (or tree) of such interactions on both structures can lead to atomically distinguishable states, the initial structures are said to be bisimilar. Provided the observation operator correspond to logical operators via their Kripke interpretation, it entails that no formula can distinguish between the structures. To prove the faithfulness of the embedding of logic A into logic B, it is thus sufficient to transform the countermodel in logic A into a bisimilar countermodel in logic B. For instance, S4 is provably complete w.r.t. the class of (potentially infinite) trees. The reduction to the completeness of S4 w.r.t. preorders is done by showing that preorders can be bisimulated by trees [Blackburn&Rijke&Venema01]. This result is at the core of our embedding of S4 into Boolean BI. Bisimilarity is also a way to study the expressivity of a logic. Indeed, if a class of models of a logic can be reduced to a subclass of models such that the structures of the subclass bisimulate those of the superclass, then we can deduce that the logic cannot express properties of structures which are specific to the superclass. The main objectives of this subtask are:
The expertise of LORIA and LSV partners on such embeddings and also bisimulation is a strong guarantee for the completion of this task. The previous works of the partners on adjunct elimination have to be related and developed in this perspective. Subtask 2.2: Separation vs. modalities for updates Responsible: Andreas Herzig (IRIT); Main partners: IRIT, LORIA, LSV Modal logics with an update semantics contain linguistic tools for describing actions and the effects of their executions on the beliefs and the preferences of agents. These actions can be, for example, publicly announcing some true fact to all agents or privately announcing some true fact to a restricted group of agents. After the first announcement, the true fact becomes a common knowledge to all agents whereas after the second announcement, the true fact becomes a common knowledge to the agents of the restricted group. Strictly speaking this is only guaranteed for facts of the world; an announcement of ignorance such as ``p is true, and agent a does not know that'' may be unsuccessful, in the sense that this formula does not become common knowledge after the announcement. An important feature of announcements, whether they are public or private, is that they have also to do with the logical dynamics of what agents believe about each other. Modelling the information flow they involve has been done in a systematic manner by several authors including [Balbiani&al08,Baltag&Moss04,vanBenthem&al06,vanBenthem&Liu07]. Recently, a highly expressive variant of the modal logics with an update semantics described above has been proposed by [Aucher&al08] within the context of graph rewriting. The linguistic tools it contains permit us to talk about properties of graphs considered as relational structures: linearity, well-foundedness, etc. They also permit us to prove invariant properties of graph rewriting systems. These linguistic tools, apart from those of standard epistemic logic, include a universal modal operator. They also include modal operators parametrized by actions called global modifiers and modal operators parametrized by actions called local modifiers. Restricted to its global modifiers, the logic of graph modification generalizes the modal logics with an update semantics introduced by van Benthem et Liu [vanBenthem&Liu07]. Adding the local modifiers dramatically increases its expressive power: the logic of global modifiers and local modifiers is undecidable. Nevertheless, when interpreted over finitely branching structures or over finite structures, the logic of graph modifiers becomes again decidable. The separation logics and the logics for resource trees that have been proposed for reasoning about mutable data structures and their decomposition usually deal with the multiplicative conjunction or the multiplicative implication. These connectives are definable in the language of the logic of global modifiers and local modifiers. Hence, natural questions arise such as: What is the minimal fragment of the language of the logic of global modifiers and local modifiers into which the multiplicative conjunction and the multiplicative implication are definable? What is the maximal fragment of the language of the logic of global modifiers and local modifiers such that the resulting logic remains decidable? When it is decidable, how is it possible to mechanize reasoning in it ? Is there a natural characterization of validity in terms of a theorem-proving approach based on a particular tableau method? The pursue of these goals requires the participation of all the partners. The main objectives of this subtask are:
The complementary expertise of all the partners on separation logics, modal logics and update semantics is a serious guarantee for obtaining original results in this task. Subtask 2.3: Decidable fragments Responsible: Stéphane Demri (LSV); Main partners: IRIT, LORIA, LSV The design of decidable fragments from rich logical formalisms is usually motivated by the need to identify expressive enough fragments with nice computational properties, typically in order to develop effective decision procedures for them. In this subtask, we aim at designing fragments of separation and update logics for which validity problem and satisfiability are decidable; this is crucial to improve the proof search in Hoare-like proof systems with separation logic as an assertion language since validity checks are needed in order to apply some of its inference rules. To do so, we shall consider logical formalisms dealing with data values and arithmetical constraints. Moreover, we shall also develop techniques for showing general undecidability results by using and extending essential ideas from [Larchey&Galmiche10] for Boolean BI. In that way, we aim at better understanding the borders for decidability. Towards general techniques for undecidability. In the context Boolean BI (BBI), which can be considered as the core of separation logics, has recently been proved undecidable undependently by Larchey-Wendling and Galmiche [Larchey&Galmiche10] and Brotherston and Kanovich [Brotherston&Kanovich10] by using respectively phase semantics and an undecidable fragment of ILL and specific encodings of two-counter Minsky machines. Moreover the undecidability of Classical BI and its neighbours can also be derived from these results. Such essental results have been obtained from a deep study of semantics and calculi for fragments of ILL and BBI and related encodings [Larchey10] and this approach will be deeper studied in order to study non only the decidability of particular fragments of separation logics and its modal extensions for update. but also to establish further undecidability results. Decidable fragments of first-order separation logic. There is a room for many investigations since first-order separation logic is undecidable in full generality whereas propositional separation logic is "only" PSPACE-complete. Today, we do not know which restrictions of the syntactic resources allow to regain decidability; for instance the interactions between the separating connectives and first-order quantification are not well-understood and this is one of the main tasks for us in this part. Nevertheless, we know that separation logic with one selector and restricted to the separating conjunction is decidable but with a non-elementary complexity [Brochenin&Demri&Lozes08] (LSV Partners) and it is strictly less expressive that the corresponding version of monadic second-order logic [Antonopoulos&Dawar09]. These recent results use techniques that could be successfully applied again. Separation logics with data. A standard approach for the fully automatic verification of programs manipulating recursive data structures via pointers is to abstract the data from the data structure, and focus on shape properties (TVLA, [Sagiv&Reps&Wilhelm02]). It has been refined by quantitative shape analysis [Finkel&Lozes&Sangnier09],where the length of the list segments of the shape are taken in consideration, allowing to check properties like termination, or the fact that the resulting list is of length the sum of the initial lists. However, refinements of shape analysis that care about the data stored in the recursive data structure are very weak. For instance, they are essential to state and check other natural functional properties: for instance, merging two ordered lists gives an order list. There is hence a need for automatic methods for checking logical entailment of Separation Logic extended with size and value properties. Our main objective is to design extensions of separation logic with data by providing effective local reasoning, pursuing the work [Bansal&Brochenin&Lozes09] and taking advantage of recent works on data logics, see e.g.[Bojanczyketal09,Demri&Lazic09]. Since expressing properties on data can quickly lead to undecidability, we shall pay a special attention to the design of decidable syntactic fragments. Decidability could be obtained by reduction into decidable theories or ad-hoc decision procedures (techniques familiar to LSV partners) or by proof-theoretical means (techniques familiar to LORIA partners). Decidable fragments of separation logics with quantitative constraints. There is another research direction that needs to be explored when dealing with enriched separation logics. Indeed, in full generality, the addition of quantitative properties, for instance to express arithmetical constraints between list lengths, leads to undecidability. However, our experience on proof systems for resource logics and more specifically on decision procedures will be precious to push further the decidability borders. It is clear that the main problem is to find strategies, criteria and classes of formulae for which our proof-methods are guaranteed to terminate. We have already applied such an approach to prove the decidability of a fragment of first-order SL1 (SL with one-selector heaps) that is more expressive than the purely existential fragment [Galmiche&Mery09] (LORIA Partners). This is a precious starting point in order to tackle decidability issues in the more general context of quantitative and recursive extensions of SL. One advantage of decision procedures advocated in [Galmiche&Mery09] is that it does not rely on formulae being in prenex (or Skolem) form, thus making it easier to adapt to resource logics for which quantifier elimination cannot be performed. The main objectives of this subtask are:
The recent results of LSV and LORIA partners, see e.g.[Brochenin&Demri&Lozes08b] [Galmiche&Mery09,Larchey&Galmiche10] provide key techniques to reach our goals, for instance by using proof-theoretical decision procedures. The ultimate goal is really to experiment decision procedures in a tableau-based prover, and therefore it is important to design those procedures with IRIT partners since they have a great experience in tableau-based decision procedures. Task 3: Proof Systems for Separation and Update LogicsResponsible: Didier Galmiche (LORIA); Main partners: IRIT, LORIA, LSV The definition of proof theories and the development of related theorem-proving methods could improve the way to verify properties and systems in the context of resource models. There exist some interesting results (calculi and procedures) for BI logic, for BI-Loc, that is an extension of BI with a modality for locations and also for Separation Logic. As said before, we plan for instance to extend separation logics with quantitative constraints while preserving decidability (length of lists, number of unrolling of recursive definitions, counting quantification...). In this context we aim at defining calculi and decision procedures with countermodel generation for various extensions of separation logics and modal logics with updates. For that we shall consider structures with labels and semantic constraints, for instance resource graphs, in order to deal with various modalities in a uniform way and then possibly to combine them with our central notions of separation and update. We also expect to develop automata-based techniques for logics combining temporal operators and separation connectives. Combinations of automata-based procedures and sequent-based decision procedures shall be also investigated. We aim at studying new characterizations of provability based on mixing proof and refutation search with a focus on the generation of countermodels. One interesting way to explore is the game-theoretic approach in which appropriate winning and counter-winning strategies for our resource logics would provide useful hints on how to combine proof and countermodel construction and on how these two aspects could interact and exchange information during the proof-search process in order to guide it more efficiently. A common point here is the study of new resource semantics, like relational semantics, for these logics in connection with our preliminaries works on resource graphs (for separation) and automata (for update). The substasks below concern the design new calculi for various extensions of separation logics and modal logics with updates, the development of automata-based techniques for logics combining temporal operators and separation connectives and also the combination of automata-based procedures and sequent-based decision procedures (subtask 3.1), the design of decision procedures based on proof and refutation construction for various extensions of separation and updates logics, with a main focus on countermodel generation (subtask 3.2) and the implementation of such procedures with a particular interest of the countermodel representation (subtask 3.3). Subtask 3.1: Structures, calculi and automata Responsible: Stéphane Demri (LSV); Main partners: IRIT, LORIA, LSV After designing new logical formalisms interpreted over new resource models that are able to express high-level properties (see Task 2), it is important and natural to design proof systems for most logical problems related to such logics. The term "proof system" should be understood in the broad sense since it may involve proof search and model building (techniques mainly developed by IRIT and LORIA partners), or it may be an automata-based decision procedure when the resource logics are able to perform temporal reasoning (technique mainly developed by LSV partners). Even though we are aware that these methods are often related at some abstract level, they necessarily need to represent models by constraints. That is why, in this subtask, apart from designing decision procedures based on analytic calculi, we aim at introducing symbolic representations of models that could be used by various calculi. Aiming at unification of symbolic representations is a major originality of this subtask. In this context we have also recently worked on natural deduction and sequent calculi in various intuitionistic and classical modal logics and provided calculi, based on particular label-free sequent structures, that have good properties like cut-elimination and subformula properties also in the intuitionistic case [Galmiche&Salhi10b]. In the context of mixing separation and update in resource logics the study of extensions of such calculi with the separation connectives is a first step to consider some modal separation logics in the perspective of proof-theory. Sequent-style proof systems are not the only mechanisms to design decision procedures. Indeed, the automata-based approach for temporal logics is a standard method, see e.g. [Vardi&Wolper94], to design optimal decision procedures for the corresponding model-checking problems. In general, this approach is successful when the target class of automata admits nice properties, and the systems to be verified can be also encoded as automata. However, in order to use this approach with infinite-state systems, one needs to abstract the states of the systems. That is why, verifying systems with resources requires the use of symbolic representations of resources in order to be as successful as in the finite case. In that respect, we are interested in developing automata-based techniques for temporal logics stating evolution of resources and to analyze what are the optimal algorithms, when they exist. It is the approach we wish to follow for the above-mentioned formalisms that deal with temporal constraints, following [Brochenin&Demri&Lozes09]. Our aim is to study theorem proving in our new spatial and temporal logics and their fragments in both perspectives based on constraints through resource graphs and automata. Then we intend to study theorem-proving for based-on BI logics associated to various resource models. We can mention BBI and SL in which the additives are classical but also other logics like BI-Loc [Biri&Galmiche07] and MBI [Pym&Tofts06] that includes different modalities. A more general challenge consists in providing, from such foundations, proof theories for fragments of spatial and separation logics and proof-search methods (based on tableaux or automata) dedicated to the verification of system properties expressed in such logics. Our approach will be also studied for temporal and modal logics including separation and spatial modalities with a strong focus on countermodel generation. For example, a serious candidate for the method is local model-checking that can be viewed as a proof system approach verification even for infinite-state systems. It is a method developed to modal and temporal logics and we plan to investigate it for logical formalisms dealing with temporal reasoning and local reasoning about resources. The main objectives of this subtask are:
Subtask 3.2: Proofs, refutations and countermodels Responsible: Didier Galmiche (LORIA); Main partners: IRIT, LORIA, LSV The combination of proof search and countermodel building has already been successful for various substructural logics like intuitionistic logic [Galmiche&Larchey99], intermediate Gödel-Dummett logic [Larchey07], BI logic [Galmiche&Mery&Pym05] or hybrid modal logics [Galmiche&Salhi10b]. (LORIA partners). The main idea of the combination is to start from an analytic system that decomposes propositions (e.g. formulae, sequents…) and to associate semantical operations to the decomposition rules that build a semantical structure on which countermodel search can be performed. The semantical structures can be of different nature: labels, constraints, resource graphs, colored / oriented graphs or multi-graphs. Usually, the semantical search for countermodels is performed when no more decomposition rule is applicable, i.e. when an irreducible proposition is reached, but this is not a strict requirement. Once such a proof-system is defined and proved complete with respect to some given logic, the main challenge is to choose semantical structures that carry the correct level of information (no information is missed which is vital to the search of countermodels) as well as simple enough so that data structures and semantic search algorithms can be efficiently implemented. In previous works the role of specific structures that mix syntactic aspects of a proof-search process (to achieve more efficient guidance) with semantic aspects (to achieve countermodel construction) has been emphasized in order to characterize provability in resource logics. In the particular context of separation logics, such structures based on labels and constraints – represented as resource graphs – have been proposed for BI and SL [Galmiche&Mery05, Galmiche&Mery05a] (LORIA partners). A key and original feature of a resource graph is that it can be indifferently understood from either a proof, or a refutation point of view. Our results on resource graphs are related to recent works on games semantics [Fagian&Hyland02, Fermüller03] and the semantics of interaction [Abramsky97] which show the existence of relationships between winning strategies in a particular game and proofs or refutations Therefore, one goal is the definition of appropriate games for our resource logics in order to have a better view of the combination of proof and refutation search but also in order to improve the other decision procedures from such a perspective. Our approach to proof and refutation could be described also as two-player games on collections of resource graphs, called resource games, in which the first player (the proponent) tries to solve reachability constraints between two nodes of a resource graph using the assumptions made on its structure by the second player (the opponent). An expected benefit of such an approach would be a more intrinsic, subtle and algorithmic understanding of the notion of interaction which is usually captured in resource models or resource logics in a rather plain and declarative way through algebraic or structural rules. A challenging issue we would like to tackle, and which goes beyond the characterization of provability in resource logics, is to provide winning strategies for the proponent, and (counter-)winning strategies for the opponent, that share a tight relationship to proofs and refutations. Therefore, given a resource graph G for a formula F, we are looking for game strategies that should allow us to translate any play on G that is a win for the proponent into a proof strategy of F in a tableau or sequent based calculus and, similarly, translate any play on G that is a win for the opponent into a countermodel of F with respect to a monoidal or relational semantics. The definition of appropriate winning and counter-winning strategies for our resource logics would provide useful hints on how to combine proof and countermodel construction and on how these two aspects could interact and exchange information during the proof-search process in order to guide it more efficiently. In turn, getting a modular and well-integrated way of dealing with the combination of proof and countermodel construction would likely help us improve and refine the existing decision procedures for resource logics. Let us recall that although there exists back-and-forth game à la Ehrenfeucht - Fraïssé to compare the expressive power of various fragments of SL (more precisely, adjunct elimination [Dawar&Gardner&Ghelli04]), little to no work has been done so far to define games or games semantics in order to study or explain proof-search in resource logics (as dialogue games do in intuitionistic and intermediate logics). Moreover, except for our preliminary and ongoing research on intuitionistic logic, the notion of resource games and their use as a tool to study both proof and countermodel construction is a new concept that we wish to investigate further in the context of separation and resource logics. An alternative and complementary approach consists in studying appropriate semantics for our logics like relational or monoidal semantics and then to define if possible translations or faithful embeddings between our new logics and known logics for which efficient proof search methods are known. For instance, faithful embeddings of S4 modal logic, and then of intuitionistic logic into BBI have been recently defined [Galmiche&Larchey06] and thus could be a starting point for proof search in separation and update logics. The main objectives in this subtask are:
The expected results could be used to improve decision procedures for resource and update logics with a strong focus on combining proof and countermodel search. A complementary objective, shared with the previous subtask, is also to propose new semantics for resource and update logics capturing and combining different modalities through constraints. The expertise of all the partners on semantics, labelled calculi and games is a good starting point for this original task on unexplored characterizations of provability based on proofs and refutations for resource logics. Subtask 3.3: Decision procedures in tools Responsible: Olivier Gasquet (IRIT); Main partners: IRIT, LORIA, LSV Semantic countermodel search can provide validity (when it fails) or else a countermodel when it succeeds. From a designer (and more practical) point of view, to obtain a countermodel is often more valuable than to obtain a proof (all the more since proofs are usually enormous and non-manageable by humans). A countermodel is a tool to analyze a design flaw in a specification, but we cannot expect designers to be specialists in logical semantics. We thus distinguish the (abstract) notion of counter-model from the (concrete) notion of counter-example. When we provide a counterexample, it has to be in a form intelligible to the designer: for example, an attack on a protocol exposing a security flaw, or a run exposing a computational path to an undesired state of a system... The challenge is thus to be able to translate abstract resource countermodels which are well suited for semantic counter-model search to concrete counterexamples suited for the designer and the user of theorem provers. A preliminary study of such an approach for resource logics and in particular BI [Galmiche&Mery05a] has to be improved in the context of our new models and logics. Even though the project is focused on foundations of resource models and on logics of separation and updates, we plan to implement some of the deduction and verification methods developed in the previous tasks. Indeed, the design of new calculi with related symbolic representations will be, for instance, experimented within the publicly available tool LoTREC. We plan to mechanize the satisfiability problem associated with our logics of separation and updates through a theorem prover rewriting called LoTREC and developed by Gasquet and Said [Gasquet&Said08] (IRIT partners). LoTREC is a generic prover for modal logics that works on relational structures. It is based on the tableau method and can be executed via the URL www.irit.fr/Lotrec. Within LoTREC we have mechanized the satisfiability problem for all the basic modal logics as well as for several modal logics encountered in artificial intelligence and computer science. The resolution of the satisfiability problem for the variants of modal logics we are thinking of elaborating is still to be developed. And this is probably the most important question we will address. We plan also to enrich the prover BILL in order to experiment in the extended prototype some decision procedures for extension of separation logics that use rich symbolic representations for memory states. BILL is a prover for propositional Bunched Implication Logic (BI), written in CAML, that is able to decide whether a propositional BI formula is provable or not and thus to build a countermodel under the form of a particular graph representation, that is a resource graph [Galmiche&Mery05a]. It is based on our particular decision procedure for BI dealing with labels, constraints and resource graphs [Galmiche&Mery&Pym05]. Another tool, called CheckBI and written in Java, implements a dual functionality: verifying whether a resource graph G is a countermodel for a given BI formula F under some valuation v of atomic formulae over the nodes of the graph. We see this tool as a first step towards studying the combination of the model-checking and theorem proving approaches in BI, i.e., how to combine proof-search and countermodel- search in order to achieve efficient decision procedures including countermodel generation facilities. The main objectives of this subtask are :
|