Amani Makhlouf
email: amani.makhlouf@irit.fr

Hanh Nhi Tran
email: tran@irit.fr

Christian Percebois
email: percebois@irit.fr

Martin Strecker
email: strecker@irit.fr

Combining Dynamic and Static Analysis to Help Develop Correct Graph Transformations

Keywords: Symbolic execution, Test case generation, Graph transformation development

Developing provably correct graph transformations is not a trivial task. Besides writing the code, a developer must as well specify the pre and post conditions. The objective of our work is to assist developers in producing such a Hoare triple in order to submit it to a formal verification tool. By combining static and dynamic analysis, we aim at providing more useful feedback to developers. Dynamic analysis helps identify inconsistencies between the code and its specifications. Static analysis facilitates extracting the pre and post conditions from the code. Based on this proposal, we implemented a prototype that allows running, testing and proving graph transformations written in small t ALC , our own transformation language.

Introduction

For most of untrained developers, writing Hoare-style provably correct graph transformations is particularly demanding because besides the transformation code, they have to specify formally the pre-and post-conditions in a suitable logic.

Our ultimate goal is an integrated development environment that allows developing and reasoning about graph transformations written in small-t ALC , a logic-based graph transformation language. In the previous work [START_REF] Baklanova | Provably correct graph transformations with small tALC[END_REF], we focused on using a prover to verify a given Hoare triple presenting the transformation. However, in practice, a proof based on Hoare logic is difficult to perform and often many programing efforts are needed before submitting a transformation to the prover. Thus, in this work, we turn our attention to assisting developers in writing provably correct transformations.

Section 2 presents briefly our graph transformation language small-t ALC . Section 3 presents our approach to help developers analyzing better their transformations. On the one hand, we use dynamic analysis to detect inconsistencies between the code and its specifications (Sect. 3.1). On the other hand, we use static analysis to construct the preand post-conditions from a code (Sect. 3.2). This paper reports on how these techniques can complement each other in a testing environment to offer useful feedback to developers. DOI: 10.1007/978 3 319 41135 4 11 Our graph transformation language is based on ALC (Attributive Language with Complements) [START_REF] Schmidt Schauß | Attributive concept descriptions with complements[END_REF], a member of the Description Logic family. This logic uses a three-tier framework: concepts, facts and formulae. A concept represents a set of individuals and a role represents a binary relation between the individuals.

At the concept level, a concept C can be empty, atomic or built from other concepts. ALC provides the following concept constructors: intersection (C1 \ C2), union (C1 [ C2), complement (¬C) and existential or universal restrictions on roles (9r C and 8r C). The fact level allows making assertions about an individual owned by a concept, or involved in a role. The grammar of facts is summarized in the following: (i:C) asserts that an individual i is an instance of a concept C; (i r j) and (i (¬r) j) assert respectively that an instance of a role r exists or not between two individuals i and j. The final level is about formulae defined by a Boolean combination of ALC facts. This formula level includes negation (¬f), conjunction (f1 ^f2) and disjunction (f1 _ f2) of formulae.

Concepts, facts and formulae are the core of small-t ALC , a rule-based imperative programming language that we've developed for specifying and reasoning about graph transformations [START_REF] Baklanova | Provably correct graph transformations with small tALC[END_REF]. Note that individuals of a concept can be represented as the nodes of a graph; in the same way, a role between two individuals corresponds to an edge. Thus, a graph can be described by a formula in which each node is represented by a fact (i:C) and each edge between two nodes i and j is represented by a fact (i r j). Manipulating a graph results in modifying the formula representing it. small-t ALC provides statements to manipulate the structure of a graph: add (i:C) and delete (i:C) for adding and respectively deleting a node (an individual) from a concept 1 ; add (i r j) and delete (i r j) for adding and respectively deleting an edge (a role) between two nodes. small-t ALC also proposes (select i with f), a non-deterministic assignment statement allowing to select a set of individuals satisfying a formula. In this work, we focus only on transformation of graph structure and do not deal with the values of attributes that maybe associated to graph's elements. small-t ALC enables sequential composition, branching, iteration and modularity. A small-t ALC program comprises transformation rules and a main function, as the program's entry, that orders the rules to be executed. To allow reasoning about graph transformation programs, a rule is annotated with assertions specifying its pre-and post-conditions. The distinctive feature of small-t ALC is that formulae occur not only in assertions (such as pre-and post-conditions or loop invariants), but also in statements (branching and iteration conditions, select conditions). In this way, assertions are akin to graph manipulation statements and based on the same logic dialect. Assertions lead to a Hoare-like calculus for small-t ALC with potential tests and proofs. Figure 1 gives an example of a small-t ALC rule which redirects the edges between nodes of concept A and nodes of concept B to the edges between nodes of concept A and new nodes of concept C. The rule is structured into three parts: a pre-condition, the code (a set of statements) and a post-condition. small-t ALC is designed as a domain specific language, not a general purpose one. Thus, to simplify its syntax, all rules work on the same input and output graphs and the pre-and post-conditions are specified on these global graphs. In this example, the pre-condition expresses that a is a node of concept A, b a node of concept B and that a is linked to b via role (or edge) r. While there are nodes a and b satisfying the while condition, the rule selects these nodes, deletes the link between them, add a new node c of concept C, then connects the selected node a with the new node c via the role r. The post-condition expresses that there are three nodes a, b and c of concepts A, B and C respectively and that a is connected to c via role r2 .

For executing and reasoning on small-t ALC programs, we developed an environment composed of a Java code generator to enable executing small-t ALC rules, a JUnit test case generator for rule testing and an Isabelle/HOL verification condition generator coupled to a tableau prover for Hoare triples.

Assistance for Writing Small-t ALC Programs

Our objective is to provide assistance on writing both small-t ALC code and specifications by combining static and dynamic analysis [START_REF] Smaragdakis | Combining static and dynamic reasoning for bug detection[END_REF]. In Sect. 3.1 we report how testing can help developers correct their code with respect to given specifications. In Sect. 3.2 we investigate the symbolic execution technique to help a developer construct pre-and post-conditions from a given code.

Dynamic Analysis for Detecting Defects in Transformation Code

We consider a situation where the correct specifications of a code are given, especially the pre-condition. As presented in Sect. 2, the pre-and post-conditions are formulae specifying graphs before and after a transformation. Each fact of the pre-condition represents the existence of a node or an edge in the source graph. Each fact of the post-condition represents the existence of a node or an edge in the target graph. Thus, from the given pre-condition we can generate a source graph and, from the given post-condition, generate a set of test cases for the required properties. In our framework, dynamic analysis consists in testing the target graph obtained by the transformation with the generated test cases which are expressed in JUnit. In this context, we defined and implemented a unit testing library for small-t ALC having about twenty assertion methods allowing testing the existence and multiplicity of nodes and edges.

Figure 2 shows the result of the generation of a source graph and the test cases corresponding to the pre-and post-conditions of the example in Fig. 1. The generated source graph represents the minimal graph configuration satisfying the pre-condition.

Suppose that the developer did not write the statement add(a r c) in the code. Because of this missing statement, the corresponding test assertExistEdge(a r c) fails. This test result reveals then an inconsistency between the code and its specifications. Moreover, it informs the developer about the non-existence of the edge r between a and c3 .

When the proof fails on verifying a program, the prover can give a counter example without further suggestions about the code's inconsistencies. This counterexample can be used as the program's graph input instead of a graph generated from the precondition to provide more feedback about the behavior of the code in such situation.

Static Analysis for Constructing Specifications from Code

Assume now that a code is correct, but developers need help to define the formal specification. We aim at computing, from the given code, conditions that must be satisfied before and after applying the transformation. For small-t ALC programs whose symbolic values are explicitly defined in the code's formulae, such computation can be easily done by using a technique based on symbolic execution. We analyze the code's control flows to generate all possible execution paths and then execute each path symbolically to construct incrementally the pre-and post-conditions by considering the required conditions of each path.

We recall that the axiomatic semantics of each small-t ALC statement is defined by the formulae representing its pre-and post-conditions, which specify a graph before and after executing the statement. Thus, on tracing the path's statements, we can compute progressively the formulae representing the pre-and post-conditions of the path by updating them according to the pre-or post-conditions of each encountered statement. An execution path is analyzed in two directions. A forward computation extracts a formula representing the post-condition and a backward computation extracts a formula representing the pre-condition. Path statements are processed differently in each computation mode. Figure 3 presents, in a simplified functional style, the algorithms to update the extracted specification according to the semantics of the encountered statement.

In this figure, FC represents the Forward Condition formula and BC the Backward Condition formula. st(f) denotes a small-t ALC statement, where st can be add, delete or select and f is the formula specifying the manipulated graph element. If st is add or delete, f can be (i:C) to represent a node, or (i r j) to represent an edge. The auxiliary functions pre(st(f)) and post(st(f)) extract respectively the pre-and post-conditions of st (f). For example, pre(add(i r j)) = (i (¬r) j) and post(add(i r j)) = (i r j) as we allow only one edge of a given relation between two nodes. For the select statement, pre (select(f)) = post(select(f)) = f. The auxiliary functions addFM(C, f) and delFM(C, f) are used respectively to add the formula f into the path's conjunction C (if C does not already contain f) or delete the formula f in the conjunction (if C contains f). C denotes a post-condition Q in a forward computation, or a pre-condition P in a backward computation.

For a given path, FC and BC of the classic control statements are computed in the same way as strongest post-condition and weakest pre-condition computations respectively [START_REF] Gordon | Forward with Hoare[END_REF]. Figure 4 illustrates the FC computation for the post-condition Q of the example in Fig. 1. We consider only the execution path in which the while condition is true.

The computed formula is then presented to developers in the testing framework (c.f. Sect. 3.3) to allow them to verify if the conditions of the analyzed path are respected in the current rule's pre-and post-conditions issued from analyzing previous execution paths or written by developers themselves. The consequence rule of Hoare logic rule allows to strengthen the precondition and/or to weaken the post-condition of a Hoare triple: given P1 ! P2 and Q2 ! Q1, if {P2} S {Q2} then {P1} S {Q1}. Ideally P1 should be the weakest precondition wp(S, Q1) of S with respect to Q1 and vice versa (i.e. Q1 should be the strongest post-condition sp(S, P) of S with respect to P1). However, developers can write a rule with the independent specifications P2 and Q2 where some facts of the precondition P2 are not necessarily considered for the post-condition Q2. Considering the rule in Fig. 1, (a r b) in the pre-condition has been translated into (a r c) without considering (a ¬r b) in the post-condition.

Combining Dynamic and Static Analysis

The two scenarios represented in Sects. 3.1 and 3.2 are the borderline cases of smallt ALC transformations development. In practice, both of specifications and code are partially and imprecisely defined. Complementary to the diagnostics provided by a prover, we propose an approach that allows treating an incomplete Hoare triple by verifying its consistency in an incremental manner. In general developers prefer testing to proving, so our assistance provides them feedback via a testing framework combining white-box testing and black-box testing [START_REF] Beckert | White box testing by combining deduction based specification extraction and black box testing[END_REF].

A developer may write a code and weak specifications, apply the white-box testing to detect inconsistencies between them and use the static analysis technique to complete them. On the basis of the static analysis technique, extracted specifications from the code are compared to pre-and post-conditions given by the developer to help him correct or complete his specifications. This comparison yields black-box test cases generated from the extracted pre-and post-conditions then executed on a graph generated from the given pre-and post-conditions respectively. Each test which fails corresponds to a missing or an incorrect fact in the formula representing the given specification. Therefore, during the development of a transformation program, in each iteration, a developer can alternate between the two approaches depending on his needs.

Discussion

Our small-t ALC environment combines two techniques for verifying a Hoare triple. The prover we developed [START_REF] Baklanova | Provably correct graph transformations with small tALC[END_REF] can prove the correctness of a transformation for all arbitrary graphs satisfying the pre-condition without executing the transformation. This formal verification technique, although has been well developed [START_REF] Habel | Correctness of high level transformation systems relative to nested conditions[END_REF][START_REF] Poskitt | Hoare style verification of graph programs[END_REF], is not really applicable during the transformation development where the Hoare triple is often still incomplete. The testing environment presented in this paper proposes a more pragmatic solution, from the developer's point of view, to detect inconsistencies in an under-developed transformation. By using both of the above techniques, we try to take advantage of multiple complementary approaches [START_REF] Smaragdakis | Combining static and dynamic reasoning for bug detection[END_REF][START_REF] Liu | Combining specification based testing, correctness proof, and inspection for program verification in practice[END_REF][START_REF] Owre | PVS: combining specification, proof checking, and model checking[END_REF] for assisting transformation developers.

To assist developers, testing has been used for generic imperative languages. Our approach shares with [START_REF] Beckert | White box testing by combining deduction based specification extraction and black box testing[END_REF] the idea to use a deductive program verification mechanism for extracting specification by symbolically executing small-t ALC rules. Our forward and backward test cases generations are based on code-driven paths exploration as in [START_REF] Beckert | White box testing by combining deduction based specification extraction and black box testing[END_REF][START_REF] Engel | Generating unit tests from formal proofs[END_REF]. The transitions from code to specification and vice versa are straightforward with small-t ALC because it uses the same logic to specify programs and properties to be verified. This is often less direct for conventional imperative languages where there is a possible gap between the logic defining the semantics of the language and the logic used for formalizing the correctness of programs. In such cases, sometimes it is difficult to identify symbolic values [START_REF] Xie | Symstra: a framework for generating object oriented unit tests using symbolic execution[END_REF] and symbolic execution is often achieved for only a limited subset of the target language features [START_REF] Engel | Generating unit tests from formal proofs[END_REF].

The design of language GP2 [START_REF] Bak | A reference interpreter for the graph programming language GP 2[END_REF] is close to small-t ALC . Building blocks in GP programs are conditional rule schemata whose nodes and edges are labeled by sequences of expressions over parameters of type integer, string and list. Condition of a rule schema can be expressed then on the existence of a specific labeled edge or the in/out degree of a node. small-t ALC does not propose such computations on nodes and edges: individuals (nodes) and roles (edges) within a rule define only local structural properties of a graph. We do not define variables and values in order to simplify the small-t ALC 's computation model. The conditions of our calculus are ALCQ formulae while GP uses E-conditions [START_REF] Habel | Correctness of high level transformation systems relative to nested conditions[END_REF], i.e. nested graph conditions extended with expressions as labels and assignment constraints for specifying properties of labels [START_REF] Poskitt | Hoare style verification of graph programs[END_REF]. Tools to help the designer when a fail occurs are not addressed in GP.

Few works have been proposed for testing graph transformation implementations. Close to our work, [START_REF] Darabos | Towards testing the implementation of graph transformations[END_REF] generates test cases for the graph pattern matching phase; [START_REF] Geiger | Transforming graph based scenarios into graph transformation based JUnit tests[END_REF] generates JUnit test cases from a Fujaba graphical story diagram. Both approaches are based on the graph pattern matching phase of the transformation rule to generate test cases, not on logical rule specifications as we propose.

Conclusion

Thanks to the formal semantic basis of small-t ALC , we can apply both dynamic and static analysis techniques in an effortless way to reason about small-t ALC programs and give useful feedback to developers during the transformation development.

Our current test data generation is rather simplistic and just covers a minimal configuration of possible source graphs. We are improving our algorithm for generating more graphs from the typical graph on the basis of Molloy-Reed algorithm [START_REF] Molloy | A critical point for random graphs with a given degree sequence[END_REF][START_REF] Molloy | The size of the giant component of a random graph with a given degree sequence[END_REF] and allowing also graph inputs provided by developers as the prover's counterexample.

In this paper we did not deal with loop invariants as conditions of a transformation, we plan to automatically infer and test invariant candidates gathered from their corresponding post-condition as proposed in [START_REF] Zhai | Post condition directed invariant inference for loops over data structures[END_REF]. This attempt is based on the fact that a small-t ALC loop iterates on all individuals selected from a logic formula in order to achieve the same logic property for all transformed elements. We also aim at enhancing interface functionalities between test and proof processes. For instance, suppose that our testing environment validates a rule's post-condition on a given path. One can imagine, with the help of a prover, computing the strongest post-condition of this path by symbolic execution. The correctness of the path can be proven if the strongest post-condition implies the given post-condition. If this implication holds for all paths in the code, then the original Hoare triple is valid [START_REF] Gordon | Forward with Hoare[END_REF].

Fig. 1 .

 1 Fig. 1. Rule redirecting (a r b) to (a r c)

Fig. 2 .

 2 Fig. 2. Source graph and test cases generated from the running example

Fig. 3 .

 3 Fig. 3. Forward and Backward computations for analyzing small t ALC statements

The individual is not deleted from the graph because it can be still owned by other concepts.

We can strengthen the post condition by adding the fact (a ¬r b) to insist that there is no edge between a and b. However, we intentionally keep it weak to illustrate that developers can write any post condition, not exactly the strongest post condition wrt. the given pre condition.

If the post condition was strengthened by the fact (a ¬r b), the corresponding test assertNotExistEdge(a r b) will have been also generated.

Acknowledgment. Part of this research has been supported by the Climt (Categorical and Logical Methods in Model Transformation) project (ANR 11 BS02 016).


Joseph Boudou
email: joseph.boudou@irit.fr

Exponential-Size Model Property for PDL with Separating Parallel Composition

Propositional dynamic logic is extended with a parallel program having a separating semantic: the program (α β) executes α and β on two substates of the current state. We prove that when the composition of two substates is deterministic, the logic has the exponential-size model property. The proof is by a piecewise filtration using an adaptation of the Fischer-Ladner closure. We conclude that the satisfiability of the logic is decidable in NEXPTIME.

Introduction

Propositional dynamic logic (PDL) is a multi-modal logic designed to reason about behaviors of programs [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. With each program α we associate a modal operator [α], formulas [α]ϕ being read "all executions of α from the current state lead to a state where ϕ holds". The set of programs is structured by some operators: sequential composition (α ; β) of programs α and β executes β after α; nondeterministic choice (α ∪ β) of program α and β executes α or β, nondeterministically; test ϕ? on formula ϕ does nothing but can be executed only if the current state satisfies ϕ; iteration α * of program α executes α a nondeterministic number of times. A limitation of PDL is the lack of a construct to reason about concurrency.

Different extensions of PDL have been devised to overcome this limitation, for instance interleaving PDL [START_REF] Abrahamson | Modal logic of concurrent nondeterministic programs[END_REF], PDL with intersection [START_REF] Harel | Recurring dominoes: making the highly undecidable highly understandable (preliminary report)[END_REF] and the concurrent dynamic logic [START_REF] Peleg | Concurrent dynamic logic[END_REF]. PDL with storing, recovering and parallel composition (PRSPDL) [START_REF] Benevides | Propositional dynamic logic with storing, recovering and parallel composition[END_REF] is another extension of PDL for concurrency. The key difference is that in PRSPDL, the program (α β) executes α and β in parallel on two substates of the current state. Hence, (α β) being executable at some state does not imply that α or β is executable at that state. Moreover, since states can be separated in substates (and merged back), PRSPDL is related to the Boolean logic of bunched implication (BBI) [START_REF] Pym | The semantics and proof theory of the logic of bunched implications[END_REF]. Indeed, a multiplicative conjunction semantically similar to the one found in BBI can be defined in PRSPDL. Thus PRSPDL can be compared to the classical version of the multi-modal logic of bunched implication (MBIc) [START_REF] Collinson | Algebra and logic for resource-based systems modelling[END_REF], a difference being that MBIc has only the parallel composition as program constructs, limiting its expressive power [START_REF] Balbiani | Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization[END_REF].

The combination of separation and concurrency provided by the parallel construct of PRSPDL suggests some interesting applications. For instance, a dynamic and concurrent logic on heaps of memory akin to separation logics [START_REF] Demri | Separation logics and modalities: a survey[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], may be envisioned. Moreover, as PDL has been adapted to different contexts, a separating parallel composition may be of interest in some of them. For instance, in dynamic epistemic logics [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF], the parallel epistemic action (!ϕ !ψ) could mean that ϕ is announced to a group of agents and ψ is announced to the agents not in that group. Despite this potential, there has been almost no complexity analysis of dynamic logic with separating parallel composition. The complexity of PRSPDL is not studied in [START_REF] Benevides | Propositional dynamic logic with storing, recovering and parallel composition[END_REF]. In [START_REF] Balbiani | Definability and computability for PRSPDL[END_REF], PRSPDL interpreted over frames where there is at most one decomposition of any state into substates is proved to be highly undecidable.

In this paper, we study the complexity of PDL with separating parallel composition (PPDL). The language of this logic is the fragment of PRSPDL without the store and recover programs which allow to access substates directly. We focus on the class of -deterministic frames where the composition of substates is deterministic: there is at most one way to merge two states. This restriction is quite natural and has been studied in many logics with separation like separation logics, ambient logics [START_REF] Cardelli | Anytime, anywhere: modal logics for mobile ambients[END_REF], BBI [START_REF] Larchey-Wendling | The undecidability of boolean BI through phase semantics[END_REF] and arrow logics [START_REF] Marx | Arrow Logic and Multi-modal Logic[END_REF]. We show that for PPDL, -determinism conveys some interesting properties, notably a strong finite model property leading to a complexity upper bound of NEXPTIME for the satisfiability problem. This result contrasts with the 2EXPTIME complexity of other dynamic logics with concurrency like PDL with intersection [START_REF] Lange | 2-exptime lower bounds for propositional dynamic logics with intersection[END_REF] or interleaving PDL [START_REF] Mayer | The complexity of PDL with interleaving[END_REF]. To prove this result, we provide nontrivial adaptations of existing methods (Fischer-Ladner closure and model unraveling) along with some new concepts (placeholders, marking functions and the neat model property).

The paper is structured as follows. In the next section, the language and semantic of PPDL is formally defined. In Sect. 3, the problem of decomposing formulas of the forms [α β] ϕ is resolved by extending the language and by adapting the Fischer-Ladner closure. In Sect. 4, the new concepts of threads, twines and neat models are introduced. And in Sect. 5, it is proved that the class of neat -deterministic frames satisfies the same formulas as the class of -deterministic frames. In Sect. 6, the strong finite model property is proved by piecewise filtration.

The negation construct is an involution: by definition, ¬¬ϕ = ϕ. Parentheses may be omitted for clarity, but they are taken into account when counting occurrences of symbols. We write |α| and |ϕ| for the number of occurrences of symbols in the program α and the formula ϕ, respectively. We define the abbreviations . = ¬⊥ and α ϕ .

= ¬ [α] ¬ϕ. The missing usual (additive) Boolean operators can be defined too, starting with ϕ → ψ . = [ϕ?] ψ. Additionally, a multiplicative conjunction related to BBI [START_REF] Pym | The semantics and proof theory of the logic of bunched implications[END_REF] may be defined as A frame is a tuple (W, R, ) where W is a non-empty set of states (denoted by w, x, y . . .), R is a function associating a binary relation over W to each atomic program and is a ternary relation over W . Intuitively, x R(a) y means that the program a can be executed in state x, reaching state y. Similarly, x (y, z) means that x can be split into the substates y and z or equivalently that y and z can be merged to obtain x. When the merging of states is functional, the frame is said to be -deterministic. This is a common restriction, for instance in separation logics, expressing the fact that the parts determine the whole. Formally, a frame is -deterministic iff for all x, y, w 1 , w 2 ∈ W , if x (w 1 , w 2 ) and y (w 1 , w 2 ) then x = y. The class of -deterministic frames is denoted by

C -det .
A model is a tuple (W, R, , V ) where (W, R, ) is a frame and V is a function associating a subset of W to each propositional variable. A model is -deterministic iff its frame is -deterministic. The forcing relation is defined by parallel induction along with the extension of R to all programs:

M, x p iff x ∈ V (p) M, x ⊥ never M, x ¬ϕ iff M, x ϕ M, x [α] ϕ iff ∀y ∈ W, if x R(α) y then M, y ϕ x R(α ; β) y iff ∃z ∈ W, x R(α) z and z R(β) y x R(α ∪ β) y iff x R(α) y or x R(β) y x R(ϕ?) y iff x = y and M, x ϕ x R(α * ) y iff x R(α) * y
where R(α) * is the reflexive and transitive closure of

R(α) x R(α β) y iff ∃w 1 , w 2 , w 3 , w 4 ∈ W, x (w 1 , w 2 ) , w 1 R(α) w 3 , w 2 R(β) w 4 and y (w 3 , w 4 )
Given a class C of frames, a formula ϕ is satisfiable in C iff there exists a model M = (W, R, , V ) and a state w ∈ W such that (W, R, ) ∈ C and M, w ϕ. The satisfiability problem of PPDL over a class C of frames is the decision problem determining whether a PPDL formula is satisfiable in C.

Fischer-Ladner Closure

In [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF], Ficher and Ladner proved the strong finite model property of PDL by means of the filtration by a set of formulas called the Fischer-Ladner closure.

To cope with nondeterministic choice and iteration, the original Fischer-Ladner closure extends PDL's language with new propositional variables. In the case of PPDL, a more involved extension of the language is needed to cope with parallel composition of programs. We first introduce this extension before defining the Fischer-Ladner closure adapted to PPDL.

Placeholders and Marking Functions

In order to decompose formulas of the form [α β] ϕ into subformulas, the language is extended with new atomic formulas called placeholders and parallel composition symbols are distinguished by added indices. Using the same sets Φ 0 and Π 0 of propositional variables and atomic programs, the sets Π P H , Φ pure and Φ P H of annotated programs, pure formulas and annotated formulas respectively, are defined by parallel induction as follows:

α, β := a | (α ; β) | (α ∪ β) | ϕ? | α * | (α i β) ϕ := p | ⊥ | ¬ϕ | [α]ϕ ψ := ϕ | (i, j) | ¬ψ | [α]ψ
where i ranges over N and j over {1, 2}. Moreover, for all i ∈ N, there must be at most one occurrence of i in any annotated program, any pure formula and any annotated formula. The integers below the parallel composition symbols are called indices. Formulas of the form (i, j) are called placeholders.

To interpret the annotated formulas, if placeholders were simply considered as new propositional variables, it would be impossible to ensure that whenever w (x, y) and M, w

[α i β] ϕ then M, x [α] (i, 1) and M, y [β] (i, 2
). Therefore we add flexibility in the interpretation of placeholders by adding marking functions which are functions from placeholders to subset of W . The set of all such functions is denoted by B W . The empty marking function m ∅ W ∈ B W binds the empty set to all placeholders. The 4-ary forcing relation F is defined on all models M = (W, R, , V ), all w ∈ W , all m ∈ B W and all ϕ ∈ Φ P H by parallel induction along with the extension of R to all annotated programs, in a similar way than for PPDL except:

M, x, m F (i, j) iff x ∈ m(i, j) x R(ϕ?) y iff x = y and M, x, m ∅ W F ϕ x R(α i β) y iff ∃w 1 , w 2 , w 3 , w 4 , x (w 1 , w 2 ) , w 1 R(α) w 3 , w 2 R(β) w 4 and y (w 3 , w 4 )
There exists a forgetful surjection • : Φ pure -→ Φ associating to each pure formula ϕ the formula ϕ obtained by removing all indices in ϕ. Thanks to the following lemma, we will consider satisfiability of pure formulas instead of satisfiability of PPDL formulas.

Lemma 1. For all model

M = (W, R, , V ), all ϕ ∈ Φ pure and all w ∈ W , M, w, m ∅ W F ϕ iff M, w ϕ. (μ, ϕ) (μ, ¬ϕ) (μ, [a] ϕ) (μ, ϕ) (μ, [α ; β] ϕ) (μ, [α] [β] ϕ) (μ, [α ∪ β] ϕ) (μ, [α] ϕ) (μ, [β] ϕ) (μ, [ϕ?] ψ) (μ, ϕ) (μ, ψ) (μ, [α * ] ϕ) (μ, [α] [α * ] ϕ) (μ, ϕ) (μ, [α i β] ϕ) (μ.L, [α] (i, 1)) (μ.R, [β] (i, 2)) (μ, ϕ)

Fischer-Ladner Closure

The Fischer-Ladner closure is a decomposition of any PDL formula into a set containing sufficiently many subformulas for the filtration. In the case of PPDL, we need to keep track of the level of separation (called depth) of each subformula. Hence we consider localized formulas. A location is a word on the alphabet {L, R}, the empty word being denoted by . A localized formula is a pair (μ, ϕ) composed of a location μ and a formula ϕ.

Then, given a localized formula (μ, ϕ) over Φ 0 and Π 0 , we construct the closure Cl(μ, ϕ) of (μ, ϕ) by applying the rules in Fig. 1. In the remainder of this paper we will be mainly interested in closure of localized formulas of the form ( , ϕ 0 ) where ϕ 0 is a pure formula. For all pure formula ϕ 0 ∈ Φ pure , we define the abbreviations FL(ϕ 0 ) = Cl( , ϕ 0 ) and SP(ϕ 0 ) = {α | ∃μ, ∃ϕ, (μ, α ϕ) ∈ FL(ϕ 0 )}. The cardinality of FL(ϕ 0 ) is denoted by N ϕ0 . The proof from [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF] can be easily adapted to prove the following lemma:

Lemma 2. N ϕ0 is linear in |ϕ 0 |.

Threads, Twines and Neat Models

In this section, new concepts about PPDL's models are introduced. These concepts allow us to restrict the class of models to consider for satisfiability. In the next section, we prove that any formula satisfiable in the class of -deterministic models is satisfied in a model with these additional properties. Firstly, to bound the depth of separation of states, we introduce the notion of hierarchical models. This directly corresponds to locations of formulas from the previous section.

Definition 1. Given a model M = (W, R, , V ), a function λ : W -→ {L, R} * is a hierarchy function for M iff ∀x, y, z ∈ W , x (y, z) ⇒ λ(y) = λ(x).L and λ(z) = λ(x).R (1) ∀x, y ∈ W, ∀α ∈ Π P H , xR(α) y ⇒ λ(x) = λ(y) (2)
λ(x) is called the depth of x. A model for which there exists a hierarchy function is a hierarchical model.

Secondly, in order to restrict the number of states at each level of separation, the notion of reachability is extended. Given a -deterministic model M = (W, R, , V ), consider the reachability relation

R ∃ = ∪ α∈ΠPH R(α).
This relation is obviously reflexive. Hence its symmetric and transitive closure, denoted by ∼, is an equivalence relation. The equivalence classes of W by ∼ are called threads and ∼ the thread relation. Notice that if M is hierarchical, all states in any thread T have the same depth, noted λ(T ). To strengthen the link between threads and depth, threads are grouped into pairs, each thread of a pair corresponding to one side of the separations. These pairs of threads are called twines and are formally defined as follows:

Definition 2. A twine is a pair (T L , T R ) of threads such that for all x, y, z ∈ W if x (y, z) then y / ∈ T R , z / ∈ T L and y ∈ T L ⇔ z ∈ T R .
In the remainder of this paper, a twine (T 1 , T 2 ) is identified with the set

T 1 ∪ T 2 .
Obviously, if a thread T is such that for all (x, y, z) ∈ , y / ∈ T and z / ∈ T , then for any thread T having the same property, (T, T ) is a twine. Such a thread is called an isolated thread. It can be easily proved that if (T 1 , T 2 ) and (T 1 , T 3 ) are twines, then either T 1 , T 2 and T 3 are isolated or T 2 = T 3 . We can now define the notion of neat models.

Definition 3. A model M = (W, R, , V ) is neat if it
satisfies all the following conditions:

1. For any thread T 1 there exists a thread T 2 such that (T 1 , T 2 ) or (T 2 , T 1 ) is a twine; 2. There is exactly one isolated thread T 0 ; 3. There exists a hierarchy function λ for M such that λ(T 0 ) = .

Neat Model Property

In this section we will prove that whenever a pure formula is satisfiable in C -det , it is satisfiable in a -deterministic neat model. Supposing the pure formula ϕ 0 is satisfiable, the proof proceeds as follows:

-by Lemma 3 below, there exists a countable model M B satisfying ϕ 0 ; -in Sect. 5.1, M B is unraveled into M U . -in Sect. 5.2, unreachable states from M U are pruned to obtain M N and M N is proved to be a -deterministic neat model satisfying ϕ 0 .

Lemma 3. For any satisfiable pure formula ϕ 0 , there exists a countable model satisfying ϕ 0 .

Proof. By a proof similar to Corollary 6.3 in [START_REF] Balbiani | Definability and computability for PRSPDL[END_REF].

Unraveling

Let M B = (W B , R B , B , V B ) be a countable -deterministic model satisfying a formula ϕ 0 at x 0 . We will construct the unraveling of M B at x 0 . The following method is an adaptation of the well-known unraveling method (see [START_REF] Blackburn | Modal Logic[END_REF] for instance). The key difference is that the resulting model is not a tree-like model. Let W ∞ be a countably infinite set. For all k ∈ N we will construct the tuple

U k = (M k , h k ) such that M k = (W k , R k , k , V k ) is a model with W k ⊆ W ∞ and h k is a homomorphism from W k to W B ,
thus preserving valuation. The initial tuple U 0 is such that W 0 = {x 0 } for some x 0 ∈ W ∞ , R 0 (a) = ∅ for all a ∈ Π 0 , 0 = ∅ and h 0 (x 0 ) = x 0 . Then for all k ∈ N, U k+1 is constructed from U k by fixing one of the following defects for some v, w 1 , w 2 ∈ W k , a ∈ Π 0 and w , w 1 , w 2 ∈ W B :

Successor Defect (v, a, w ). If h k (v) R B (a) w but there is no w ∈ W k such that h k (w) = w and v R k (a) w, then U k+1 is obtained from U k by adding a new state w ∈ W ∞ \ W k such that h k+1 (w) = w and v R k+1 (a) w, Split Defect (v, w 1 , w 2 ). If h k (v) B (w 1 , w 2 ) but there are no w 1 , w 2 ∈ W k such that h k (w 1 ) = w 1 , h k (w 2 ) = w 2 and v k (w 1 , w 2 ), then U k+1 is obtained from U k by adding two new states w 1 , w 2 ∈ W ∞ \ W k such that h k+1 (w 1 ) = w 1 , h k+1 (w 2 ) = w 2 and v k+1 (w 1 , w 2 ). Merge Defect (w , w 1 , w 2 ). If w B (h k (w 1 ), h k (w 2 )) but there is no w ∈ W k such that h k (w) = w and w k (w 1 , w 2 ), then U k+1 is obtained from U k by adding a new state w ∈ W ∞ \ W k such that h k+1 (w) = w and w k+1 (w 1 , w 2 ).
Since W ∞ , Π 0 and W B are countable sets, there is a sequence δ 0 , δ 1 , . . . of possible defects such that each possible defect appears infinitely often. We enforce that for all k ∈ N, either δ k is a defect for U k fixed in U k+1 or δ k is not a defect for U k and U k+1 = U k . The unraveling

M U = (W U , R U , U , V U ) of M B at x 0 is the union of M k for all k ∈ N. Proposition 1. M U is a -deterministic model satisfying ϕ 0 .
To prove Proposition 1, we adapt the bounded morphism definition to PPDL and prove Lemma 4.

Definition 4. Given two -deterministic models

M = (W, R, , V ) and M = (W , R , , V ), a mapping h : M -→ M is a bounded morphism iff it satisfies the following conditions for all v, w, w 1 , w 2 ∈ W , w , w 1 , w 2 ∈ W and a ∈ Π 0 :
w and h(w) satisfy the same propositional variables

(3) v R(a) w ⇒ h(v) R (a) h(w) (4) h(v) R (a) w ⇒ ∃w, h(w) = w and v R(a) w (5) w (w 1 , w 2 ) ⇒ h(w) (h(w 1 ), h(w 2 )) (6) h(w) (w 1 , w 2 ) ⇒ ∃w 1 , w 2 , h(w 1 ) = w 1 , h(w 2 ) = w 2 and w (w 1 , w 2 ) (7) w (h(w 1 ), h(w 2 )) ⇒ ∃w, h(w) = w and w (w 1 , w 2 ) ( 8
)
Lemma 4. If h is a bounded morphism from M to M , then for all w ∈ W and ϕ ∈ Φ, M, w ϕ iff M , h(w) ϕ.

Considering the functions (h k ) k∈N as subsets of W U × W B , we define h as their union. We prove that h is a bounded morphism, the successor, split and merge defects ensuring conditions ( 5), ( 7) and ( 8) respectively. Finally, since bounded morphisms preserve -determinism, Proposition 1 is proved. Despite M U not being tree-like, it has the following form of acyclicity:

Proposition 2. For all x, y ∈ W U and all α, β ∈ Π P H , if x R(α) y and y R(β)

x then x = y.

Pruning

In this section, we remove unreachable states from M U and prove that the resulting model is neat. The method consists in identifying reachable threads and relies on the fact that new reachable threads are added only by split defects. We use a function r associating to each state x ∈ W U either the first state of x's thread if this thread is reachable or the special value Out otherwise. The function r : W U -→ W U ∪ {Out} is formally defined by induction on the construction of M U as follows:

0. Initially, r(x 0 ) = x 0 ; 1. When fixing a successor defect (w, a, v) by adding w , r(w ) = r(w) ; 2. When fixing a split defect (w, v 1 , v 2 ) by adding w 1 and w 2 , if r(w) = Out then r(w 1 ) = w 1 and r(w 2 ) = w 2 , otherwise r(w 1 ) = r(w 2 ) = Out ; 3. When fixing a merge defect δ k = (v, w 1 , w 2 ) by adding w, if there exists w ∈ W k such that w k (r(w 1 ), r(w 2 )) then r(w) = r(w ), otherwise r(w) = Out.

The function r is well-defined because M U is -deterministic. Then, the model

M N = (W N , R N , N , V N
) is defined as the reduction of M U to the worlds x for which r(x) = Out. The following proposition can easily be proved:

Proposition 3. M N is a -deterministic model satisfying ϕ 0 at x 0 .
It remains to prove that M N is neat. Let ∼ N be the thread relation of M N . The proof of Proposition 4 relies on the following two lemmas:

Lemma 5. For all x, y ∈ W N , r(x) = r(y) iff x ∼ N y. Lemma 6. If z N (x, y) then there exists z ∈ W N such that z N (r(x), r(y))
and (z , r(x), r(y)) has been added to U by a split defect.

Proposition 4. M N is neat.

Proof sketch. For the first two conditions of Definition 3, we prove the corresponding two properties using Lemma 6:

1. For all x 1 , x 2 , y 1 , y 2 , z 1 , z 2 ∈ W N , if z 1 N (x 1 , y 1 ) and z 2 N (x 2 , y 2 ) then r(x 1 ) = r(x 2 ) ⇔ r(y 1 ) = r(y 2 ).
2. x 0 is the only x ∈ W N such that r(x) = x and for all (w, y, z) ∈ N , r(y) = x and r(z) = x.

For the last condition of Definition 3, the hierarchy function λ is constructed such that:

-λ(x 0 ) = ; -for any split defect (w, v 1 , v 2 ) adding w 1 and w 2 to W U , if r(w) = Out then λ(w 1 ) = λ(w).L and λ(w 2 ) = λ(w).R; -for all x, λ(x) = λ(r(x)).

Piecewise Filtration

In this section, we prove the following proposition: R,,V ) in which the cardinality of W is bounded by an exponential in the number of symbols in ϕ.

Proposition 5. Whenever a formula ϕ ∈ Φ is satisfiable in a -deterministic neat model, it is satisfiable in a -deterministic finite model M = (W,
Suppose M N = (W N , R N , N , V N ) is neat and M N , x 0 , m ∅ W F ϕ 0 for some x 0 ∈ W N
and ϕ 0 ∈ Φ pure . Furthermore, we suppose λ is a hierarchical function for M N such that λ(x 0 ) = . The model M F satisfying Proposition 5 is inductively constructed from M N . At the initial step, the filtration of the thread containing x 0 is added to M F . At the inductive steps, for each pair of states in M F which must be connected by a parallel program, the filtration of a twine of M N corresponding to this parallel program is added to M F .

In order to preserve the -determinism of M N during the filtration, we need to distinguish for any filtered twine, the forward (split) decomposition from the backward (merge) one. For that matter, placeholders are duplicated and the special pair {(0, 1), (0, 2)} of placeholders is used to mark the forward decomposition. Formally, for any formula ϕ ∈ Φ P H and any k ∈ N, let f dup (k, ϕ) be the formula obtained from ϕ by replacing each occurrence of (i, j) in ϕ by (2i + k, j), for all i ∈ N and j ∈ {1, 2}. We define the sets

FL + (ϕ 0 ) = {(μ, f dup (k, ϕ)) | k ∈ {1, 2}, (μ, ϕ) ∈ FL(ϕ 0 )} ∪ {((μ, (0, j)), (μ, ¬(0, j)) | j ∈ {1, 2} and ∃ϕ, (μ, ϕ) ∈ FL(ϕ 0 )} SF + (ϕ 0 ) = ϕ ∃μ, (μ, ϕ) ∈ FL + (ϕ 0 )
The filtrations are done using the ≡ m equivalence relations over W N , defined for any marking function m ∈ B W N such that x ≡ m y iff λ(x) = λ(y) and for all (μ, ϕ) ∈ FL + (ϕ 0 ) if μ = λ(x) then M N , x, m F ϕ ⇔ M N , y, m F ϕ. The functions Ω and Ψ are defined for all X ⊆ W N and m ∈ B W N by:

Ω(X, m) = Y ∩ X Y ∈ W N / ≡ m Ψ (X, m) = ϕ ∃x ∈ W N , (λ(x), ϕ) ∈ FL + (ϕ 0 ) and M N , x, m F ϕ
Finally, the set PF references all the parallel program links for which we may have to add the filtration of a twine. Formally, PF is the greatest subset of N × P SF + (ϕ 0 ) × SP(ϕ 0 ) × P SF + (ϕ 0 ) such that for all (k, F, α, G) ∈ PF, α is of the form (α 1 i α 2 ) and there exists μ ∈ {L, R} * and ϕ ∈ Φ P H such that (μ, α ϕ) ∈ FL + (ϕ 0 ) and for all ψ ∈ F ∪ G, (μ, ψ) ∈ FL + (ϕ 0 ). Since P SF + (ϕ 0 ) and SP(ϕ 0 ) are finite, there exists a total order over PF with a least element and such that (k, F, α, G) < (k , F , α , G ) implies k ≤ k . This order determines a bijective function from N to PF. Moreover, if (k, F, α, G) is the n th tuple in PF then k ≤ n. Now we inductively construct the models

M n = (W n , R n , n , V n ) for n ∈ N, where W n ⊆ N × P (W N ) × B W N .
The following invariants hold for all n ∈ N:

-for all (k, X, m) ∈ W n , all ϕ ∈ Ψ (X, m) and all x ∈ X, M N , x, m F ϕ; -for all (k, X, m), (k , Y, m ) ∈ W n , if k = k then m = m and for all x ∈ X
and all y ∈ Y , x and y belong to the same twine and if x ≡ m y then X = Y .

Initial step. Let T 0 be the thread in M N containing x 0 . We set:

W 0 = (0, X, m ∅ W N ) X ∈ Ω(T 0 , m ∅ W N ) R 0 (a) = {((k, X, m), (k , X , m )) ∈ W 0 × W 0 | k = k and ∃x ∈ X, ∃x ∈ X , x R N (a) x } 0 = ∅ V 0 (p) = {(k, X, m) ∈ W 0 | p ∈ Ψ (X, m)} If PF = ∅ then M n = M 0
for all n ∈ N. Otherwise the following inductive step is applied.

Inductive step. Suppose M n has already been defined and let (k, F, α 1 i α 2 , G) be the n th tuple in PF. If for all X, Y ⊆ W N and all m ∈ B W N , one of the following conditions is not satisfied

Ψ (X, m) = F and Ψ (Y, m) = G (9) (k, X, m) ∈ W n and (k, Y, m) ∈ W n (10) ∃x ∈ X, ∃y ∈ Y, x R N (α 1 i α 2 ) y ( 11
)
then M n+1 = M n . Otherwise, by the invariants, there is exactly one tuple (X, Y, m) satisfying ( 9) and [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. By condition [START_REF] Harel | Recurring dominoes: making the highly undecidable highly understandable (preliminary report)[END_REF], there exists x ∈ X, y ∈ Y and w 1 , w 2 , w 3 , w 4 ∈ W N such that x N (w 1 , w 2 ), w 1 R N (α 1 ) w 3 , w 2 R N (α 2 ) w 4 and y N (w 3 , w 4 ). The marking function m n+1 is defined such that -m n+1 (0, j) = {w j };

-m n+1 (i, j) = w ∃β 1 , β 2 .(β 1 i-1 2 β 2 ) ∈ SP(ϕ 0 ) and w j R N (β j ) w if i is odd; -m n+1 (i, j) = w ∃β 1 , β 2 , (β 1 i-2 2 β 2 ) ∈ SP(ϕ 0 ) and w j+2 R N (β j ) w if i is even and positive.
Since M N is neat, w 1 , w 2 , w 3 and w 4 belong to the same twine θ. For all t ∈ 1 . . 4, there exists X t ∈ Ω(θ, m n+1 ) such that x t ∈ X t . M n+1 is defined by:

W n+1 = W n ∪ {(n + 1, X, m n+1 ) | X ∈ Ω(θ, m n+1 )} R n+1 (a) = {((k, X, m), (k , X , m )) ∈ W n+1 × W n+1 | k = k and ∃x ∈ X, ∃x ∈ X , x R N (a) x } n+1 = n ∪{((k, X, m), (n + 1, X 1 , m n+1 ), (n + 1, X 2 , m n+1 )), ((k, Y, m), (n + 1, X 3 , m n+1 ), (n + 1, X 4 , m n+1 ))} V n+1 (p) = {(k, X, m) ∈ W n+1 | p ∈ Ψ (X, m)} Finally, M F = (W F , R F , F , V F
) is defined as the union of M n for all n ∈ N and we prove that M F satisfies Proposition 5.

Proof sketch of Proposition 5. To prove that the cardinality of W F is bounded by an exponential in |ϕ 0 |, we consider the graph whose vertices are sets of W F 's states having the same first component and such that there is an edge from G to G iff states in G have been added to M F to connect two states in G. We prove that each vertex contains a exponential number of states and that the graph is a tree with branching factor exponential in |ϕ 0 | and depth linear in |ϕ 0 |. -determinism of M F is ensured by the interpretation of the placeholders (0, 1) and (0, 2). Finally, to prove the truth lemma, we prove the following properties by simultaneous induction on |ϕ| for 1 and on |α| for 2 and 3:

1. For all (k, X, m) ∈ W F and all formula ϕ such that (λ(X), ϕ) ∈ FL + (ϕ 0 ), ϕ ∈ Ψ (X, m) ⇔ M F , (k, X, m), m F F ϕ. Finally, since the model checking problem for PPDL is obviously polynomial in the number of states of the model, we deduce a complexity upper bound: Proposition 6. The satisfiability problem of PPDL interpreted over -deterministic frames is in NEXPTIME.

Conclusion

In this paper, we prove that PPDL interpreted over the class C -det of -deterministic frames has a strong finite model property and that the satisfiability problem of this logic is in NEXPTIME. This results rely on the neat model property introduced in the paper and are obtained by a piecewise filtration using an adaptation of the Fischer-Ladner closure. Because formulas with parallel compositions cannot be properly decomposed into subformulas, the language is extended with indices and placeholders. We hope these new concepts will be useful in future works. We briefly list some possibilities. First, a tight complexity result for PPDL over C -det remains to be found. Secondly, the complexity of PPDL interpreted over the class of neat frames could be studied. Finally, since no semantic equivalents of the multiplicative implication of BBI can be defined in PPDL over C -det , it could explicitly be added to the language.

Fig. 1 .

 1 Fig. 1. Fischer-Ladner closure calculus

2 .

 2 If (k, X, m) ∈ W F , x ∈ X, θ x is the twine of x, Y ∈ Ω(θ x , m), y ∈ Y , (λ(x), α ϕ) ∈ FL(ϕ 0 ) and x R N (α) y, then (k, X, m) R F (α) (k, Y, m). 3. If (k, X, m) R F (α) (k, Y, m) and [α]ϕ ∈ Ψ (X, m), then ϕ ∈ Ψ (Y, m).

This work was supported by the "French National Research Agency" (DynRes contract ANR-11-BS02-011).