Emiliano Lorini
email: emiliano.lorini@irit.fr

François Schwarzentruber
email: francois.schwarzentruber@ens-rennes.fr

A Path in the Jungle of Logics for Multi-agent System: On the Relation between General Game-playing Logics and Seeing-to-it-that Logics

Keywords: modal logic, STIT logic, general game playing, dynamic logic

In the recent years, several concurrent logical systems for reasoning about agency and social interaction and for representing game properties have been proposed. The aim of the present paper is to put some order in this 'jungle' of logics by studying the relationship between the dynamic logic of agency DLA and the game description language GDL. The former has been proposed as a variant of the logic of agency STIT in which agents' action are named, while the latter has been introduced in AI as a formal language for reasoning about general game-playing. The paper provides complexity results for the satisfiability problems of both DLA and GDL as well as a polynomial embedding of GDL into DLA.

INTRODUCTION

Several logics for modelling interaction in the context of multiagent systems (MAS) and for the formal representation and specification of games have been proposed in the AI l iterature. Among them, we should mention multi-agent variants of propositional dynamic logics by [START_REF] Ågotnes | Reasoning about joint action and coalitional ability in K n with intersection[END_REF] and [START_REF] Herzig | A dynamic logic of normative systems[END_REF], coalition logic by [START_REF] Pauly | A modal logic for coalitional power in games[END_REF], alternatingtime temporal logic by [START_REF] Alur | Alternating-time temporal logic[END_REF], coalition logic of propositional control by [START_REF] Van Der Hoek | On the logic of cooperation and propositional control[END_REF] and strategy logic by [START_REF] Mogavero | Reasoning about strategies[END_REF]. These logics aim to formally represent the concept of capability, that is, the consequences of the potential action of either an agent or a coalition of agents. 1 More recently, two additional systems have been added to the picture of logics for MAS: the family of seeing-to-it-that logics, whose most representative member is STIT by [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF], and GDL by [START_REF] Zhang | A logic for reasoning about game strategies[END_REF][START_REF] Zhang | Representing and reasoning about game strategies[END_REF].

On the one hand, STIT has been introduced in philosophical logic as a formal system for reasoning about (i) what an agent or a coalition does as a result of her/its individual/collective choice (actuality), and (ii) what an agent or a coalition can do as a result of her/its individual/collective choice (potentiality). It has been shown to be a valuable formal language for modelling socio-cognitive concepts such as emotion [START_REF] Lorini | A logic for reasoning about counterfactual emotions[END_REF], responsibility [START_REF] Lorini | A logical analysis of responsibility attribution: emotions, individuals and collectives[END_REF] and intention [START_REF] Broersen | Making a start with the stit logic analysis of intentional action[END_REF]. One central feature of Belnap et al.'s STIT is that agents' actions are not named. Thus, this logic allows to represent the result of an agent's choice but does not allow to represent the chosen action that 1 Cf. [START_REF] Herzig | Logics of knowledge and action: critical analysis and challenges[END_REF] for a recent survey of existing logics for MAS. produces the result. For example, in this logic one can represent the fact that an agent 1 kills another agent 2 (agent 1 sees to it that agent 2 is dead) but one cannot represent the fact that agent 1 kills agent 2 by deciding to shoot. To overcome this limitation, DLA has been introduced by [START_REF] Herzig | A dynamic logic of agency I: STIT, abilities and powers[END_REF], as a variant of STIT in which agents' choices are explicitly named. A deterministic variant of DLA called DDLA has been proposed by [START_REF] Lorini | A dynamic logic of agency II: deterministic DLA, Coalition Logic, and game theory[END_REF]. While DDLA assumes that the outcome of the collective choice of all agents is uniquely determined, DLA drops this assumption.

On the other hand, GDL has been introduced in AI as a minimal formal system for representing game properties and strategies in the context of general game-playing. Similarly to seeing-to-it-that logics, GDL supports reasoning about both actual consequences and potential consequences of an agent's action. Moreover, similarly to DLA, in GDL, actions of agents are explicitly named. Thus, at a conceptual level, GDL and DLA are closely connected.

In this paper, we (i) explore the connection between DLA and GDL at a formal level, and (ii) thus solve some open issues about the computational properties of these two logics (see Table 1). For instance, we prove that the satisfiability problem of GDL is in NP by translating a GDL-formula into a DDLA-formula without any occurrence of the temporal operator "next" (X). This result highlights that GDL does not allow to express a property about the "next" state without mentioning the action leading to it. We also show that the satisfiability problems for DLA and for the nondeterministic variant of GDL become PSPACE-hard. Moreover, we prove that the complexity of the satisfiability problem for DDLA increases from 'in NP' to PSPACE-hard when the temporal operator "next" is given as a primitive operator in the logical language.

The paper is organized as follows. Section 2 is devoted to DLA and DDLA We first recall the syntax and the semantics of these two logics. Then, we investigate the complexity of the satisfiability problems of both DLA and DDLA, an issue that has not been explored up to now. Then, in Section 3, we move to GDL. The original GDL semantics for actions being deterministic, we present a new variant of GDL called IGDL, dropping the assumption that outcome resulting from the execution of an action is unique. We investigate the complexity of the satisfiability problems of both GDL and IGDL. Finally, in Section 4, we provide a polynomial embedding of GDL into DDLA and of IGDL into DLA helping proving upper bound of complexity for the satisfiability problems of GDL and IGDL. The paper concludes in Section 5 with a discussion of perspectives of future research.

DYNAMIC LOGIC OF AGENCY

We recall the syntax and the two semantics of the dynamic logic of agency: the non-deterministic one [START_REF] Herzig | A dynamic logic of agency I: STIT, abilities and powers[END_REF] called DLA and the deterministic one [START_REF] Lorini | A dynamic logic of agency II: deterministic DLA, Coalition Logic, and game theory[END_REF] called DDLA.

NP-complete:

DDLA without X-modalities GDL PSPACE-complete: DDLA DLA IGDL

Syntax

Let Atm be a countable set of atomic propositions denoted by p, q, . . ., let Agt be a finite set of agents denoted by 1, . . . , n and let Act be a finite set of action names denoted by a, b, . . . The set of joint action names is defined to be JAct = Act n . Elements of JAct are denoted by δ, δ , . . . For every δ ∈ JAct, δ(i) denotes the element in δ corresponding to agent i. The language L DLA (Atm, Agt, Act) of DLA is defined by the following grammar:

ϕ, ψ ::= p | ¬ϕ | (ϕ ∧ ψ) | ϕ | [[δ]]ϕ | Xϕ
where p ranges over Atm and δ ranges over JAct.

The formula ϕ is read "ϕ is true for all histories passing through the current moment" or, more shortly, "ϕ is necessarily true". The formula [[δ]]ϕ is read "if the joint action δ is chosen by the agents, then ϕ is true afterwards". The formula Xϕ is read "ϕ holds in the next moment". A formula is said to be X-free if it does not contain any occurrence of the temporal operator "next" X.

We provide the following abbreviations:

ϕ def = ¬ ¬ϕ δ ϕ def = ¬[[δ]]¬ϕ i:a ϕ def = δ∈JAct:δ(i)=a δ ϕ
that read respectively "ϕ is true for at least one history passing through the current moment", "the joint action δ is chosen by the agents and ϕ is true afterwards" and "action a is chosen by agent i and ϕ is true afterwards".

Semantics

The semantics of DLA is based on DLA models. A DLA model is a structure that provides information about agents' actual choices and available choices as well as about the consequences of the agents' choices. A DLA model can also be seen as a variant of a STIT model, as defined by [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF], in which time is assumed to be discrete and agents' choices are explicitly named. 2 Definition 1.

A DLA model is a tuple M = (W, ≡, (C) i∈Agt , S , V) where:
• W is a non-empty set of worlds,

• ≡ is an equivalence relation on W,

• C i : W -→ Act is the choice function for agent i,

• S : W -→ W is a successor state function, • V : W -→ 2 Atm is a valuation function,
such that for all w, v, u ∈ W and δ ∈ ∆: where:

(C1) if δ(i) ∈ CS i (w) for all i ∈ Agt then δ ∈ CS(w),
• CS i (w) = {a ∈ Act : ∃v ∈ W | w≡v and C i (v) = a}; • CS(w) = {δ ∈ JAct : ∃v ∈ W | w≡v and C(v) = δ}; • ⇒ δ is the relation {(w, v) : S (w) = v and C(w) = δ}; • C(v) = (C i (w)) i∈Agt .
In Definition 1, a world corresponds to a time point. Equivalence classes generated by the equivalence relation ≡ are called moments. At every world w, every agent i chooses exactly one action denoted by C i (w). Let ≡ (w) = {v ∈ W : w ≡ v} be the moment including world w. Agent i has a set of individual choices available at this moment denoted by CS i (w). Moreover, the agents have a set of collective choices available at this moment denoted by CS(w). Every world w has exactly one successor denoted by S (w): S (w) is the world resulting from the agents' collective choice at world w. Function S can be associated with a serial and deterministic relation ⇒ on W such w ⇒ v iff S (w) = v. Let F be the transitive closure of ⇒. F(w) = {(w, v) : wFv} denotes the history starting in w, i.e., the sequence of worlds in the future of w. 3 Constraint C1 says that if a 1 is a possible choice for agent 1,..., a n is a possible choice for agent n then (a 1 , . . . , a n ) is a possible collective choice. More intuitively, this means that agents can never be deprived of choices due to the choices made by other agents. Figure 1 illustrates constraint C1 in Definition 1: as it is possible for agent 1 to play b and for agent 2 to play b, there must be a world in which both agents play b. This is called independence of choices according to the STIT terminology. Constraint C2 expresses a basic relation between action and time: if v is in the future of w and u and v are in the same moment, then there exists an alternative z in the collective choice of all agents at w such that u is in the future of z. Figure 1 illustrates Constraint C2 in Definition 1. This is called no choice between undivided histories according to the STIT terminology. It captures the idea that if two histories come together in some future moment then, in the present, each agent does not have a choice between these two histories. This implies that if an agent can choose between two histories at a later stage, then she does not have a choice between them in the present. 3 As shown by [START_REF] Herzig | A dynamic logic of agency I: STIT, abilities and powers[END_REF], one can safely assume that, for all w, v ∈ W, if wFv then w v, as this property is not modally characterizable in DLA. Since ≡ is reflexive, the latter implies that F(w) can be safely assumed to be a linearly ordered set.

M, w | = p ⇐⇒ p ∈ V(w) M, w | = ¬ϕ ⇐⇒ M, w | = ϕ M, w | = (ϕ ∧ ψ) ⇐⇒ M, w | = ϕ and M, w | = ψ M, w | = ϕ ⇐⇒ ∀v ∈ W : if w ≡ v then M, v | = ϕ M, w | = [[δ]]ϕ ⇐⇒ if C(w) = δ then M, S (w) | = ϕ M, w | = Xϕ ⇐⇒ M, S (w) | = ϕ
As usual, a formula ϕ is DLA-valid iff ϕ is true for every DLA model M and every world w in M. A formula ϕ is DLA-satisfiable iff ¬ϕ is not DLA valid.

The deterministic variant of DLA (DDLA) has the same language as DLA. It is interpreted with respect to deterministic DLA models that are defined as follows:

Definition 3. A deterministic DLA model (DDLA model) is a DLA model such that for all w, v ∈ W: (C3) if w ≡ v and C(w) = C(v) then S (w) ≡ S (v).
Constraint C3 says that the collective choice of all agents leads to a unique next moment. Notions of validity and satisfiability for DDLA with respect to DDLA models are defined in the usual way.

Let us illustrate the DLA and DDLA-semantics.

Example 1. The left side of Figure 2 represents a DLA model that illustrates non-determinism: the collective choice (b, a) leads to two moments, the collective choice (a, a) leads to four moments, etc. The right side represents a DDLA model: for instance the collective choice (b, a) leads to a unique moment. Let us consider world w 0 in the model on the right. We have C(w 0 ) = (b, b). Formula ( (a, a)

→ Xp) holds at w 0 . Indeed, at moment ≡(w 0 ), if the joint action (a, a) is chosen (for instance at the unique q-world of the moment ≡(w 0 ) but also at the three other worlds where (a, a) is chosen), then p will be necessarily true in the next world.

Example 2. Formula Xϕ → [[δ]]ϕ is DLA-valid (thus also DDLAvalid): if ϕ is true in the next state, then, in particular, if δ is actually played, then ϕ is true in the next state.

Example 3. Formula ( (a, a)

∧ X p) → [[(a, a)]
]p is a DDLA-valid formula. Indeed, suppose (a, a) is played and p is necessarily true in the next state. Then, necessarily if (a, a) is played, then p is true in the next state since the model is deterministic. But the formula is not DLA-valid. Indeed, ( (a, a) ∧ X p) holds in world u of the DLA-model shown in the left side of Figure 2, but [[(a, a)]]p is false ([[(a, a)]]p does not hold at world v).

Related work

The interesting aspect of DLA is its connection with STIT, the logic of "seeing to it that" by [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF] and [START_REF] Horty | Agency and Deontic Logic[END_REF] one of the most prominent logical theories of agency proposed in the recent years.

Specifically, in [START_REF] Herzig | A dynamic logic of agency I: STIT, abilities and powers[END_REF], an embedding of the 'group STIT' by [START_REF] Horty | Agency and Deontic Logic[END_REF] with discrete time and bounded choices into DLA is given. 4"Bounded choices" means that, at every moment in time, an agent can choose among at most n actions.

STIT logic, as defined by [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF] and [START_REF] Horty | Agency and Deontic Logic[END_REF], is non-deterministic, as the consequence of the joint action of a coalition is not uniquely determined. This distinguishes STIT from the family of logics of coalitional power in games of which ATL (Alternating-time Temporal Logic) [START_REF] Alur | Alternating-time temporal logic[END_REF] and CL (Coalition Logic) [START_REF] Pauly | A modal logic for coalitional power in games[END_REF] are the most representative ones, CL being the one-step fragment of ATL [START_REF] Goranko | Coalition games and alternating temporal logics[END_REF]. The standard semantics of ATL and CL is based on the concept of concurrent game structure (CGS) according to which, once every agent has made her choice at a given state, the successor state is uniquely determined. 5 In [START_REF] Lorini | A dynamic logic of agency II: deterministic DLA, Coalition Logic, and game theory[END_REF], an embedding of CL into DDLA is given.

The CL language includes the classical boolean constructions plus modal operators of coalition capability of the form [J] , where [J] ϕ has to be read "the coalition of agents J can see to it that ϕ is true in the next state, regardless of what the agents outside J choose". The translation tr of the CL operator [J] into the DLA language proposed by [START_REF] Lorini | A dynamic logic of agency II: deterministic DLA, Coalition Logic, and game theory[END_REF] is the following:

tr( [J] ϕ) = δ∈JAct δ J ∧ ( δ J → Xϕ) .

Complexity of DLA and DDLA: Lower bound

For a given logic L, the satisfiability problem of L is denoted by L-sat.

Theorem 1. If |Agt| ≥ 2, DDLA-sat is PSPACE-hard.
Proof. We give a polynomial-time reduction from the (PSPACEhard) satisfiability problem for modal logic B defined by the class of infinite binary trees (cf. [START_REF] Blackburn | Modal logic[END_REF] and the use of this logic to prove a PSPACE-hardness result in [START_REF] Lorini | Epistemic games in modal logic: Joint actions, knowledge and preferences all together[END_REF]) to the satisfiability problem of DDLA. We write for the operator of that logic B. We define f ( ϕ) = Xtr(ϕ). We define the formula

twoActions(T ) := T t=0 X t [ δ ∧ δ ∧ ( δ ∨ δ )]
where δ = (a, a, . . . a) and δ = (b, a, . . . , a) with a b. Informally, twoActions(T ) means that until time T , agent 1 has exactly two actions a and b while the other players only can play action a.

The reduction is tr(ϕ) := f (ϕ) ∧ twoActions(T ) where T is the modal depth of ϕ. Formula ϕ is B-satisfiable iff tr(ϕ) is DDLAsatisfiable. Proof. The logic DDLA restricted to X-free formulas is a conservative extension of classical propositional logic. Theorem 3. DLA-sat (even for X-free formulas) is PSPACEhard.

q 0 , p 1 p 1 p 1 p 1
Proof. We polynomially reduce the (PSPACE-hard) satisfiability problem for modal logic K to it. We write for the operator of K. Let δ be a fixed joint action. We define tr( ϕ) := [[δ]]tr(ϕ). Formula ϕ is K-satisfiable iff tr(ϕ) is DLA-satisfiable.

Complexity of DLA and DDLA: Upper bound

For giving upper bounds for satisfiability problems of DLA and DDLA, the idea is to flatten DLA models so that histories are represented by single worlds. As in [START_REF] Schwarzentruber | Complexity results of STIT fragments[END_REF], we introduce fresh propositions p t saying that "proposition p is true at time t". Furthermore, we introduce propositions δ t i meaning that "δ i is played at time t" and we write δ t for n i=1 δ t i , meaning that the joint action δ is played at time t. These notations are used in the proofs of the following Theorems 4 and 5.

Theorem 4. DDLA-sat restricted to X-free formulas is in NP.

Proof. We polynomially reduce the satisfiability problem of DDLA restricted to X-free formulas to the satisfiability problem of S5, which is the modal logic where the accessibility relation is an equivalence relation. We recall that the satisfiability problem of S5 is in NP. The modal operator of S5 is denote by . The idea is that S5 models are flattened versions of DDLA models and we use modality to simulate the modality and to guard the quantification to the current moment.

In the sequel, we will define a reduction tr. The idea of the translation tr(ϕ) of ϕ is to simulate the semantics of DDLA in S5models that look like the model shown in Figure 3.

In the world on the bottom left of the picture, q 0 and p 1 holds. That world corresponds to a history where q holds at time 0 and p holds at time 1. The big rectangle corresponds to the moment at time 0 and we use modality to quantify over all worlds in that moment at time 0. The sub-rectangles corresponds to moment at time t > 0 (in picture, at time t = 1). Modality interpreted in the moment at time 1 after joint action δ at time 0 is simulated by the guarded construction (δ 0 → ...). Modality interpreted in the moment at time 2 after joint action δ at time 0 and δ at time 1 is simulated by the guarded construction ((δ 0 ∧ δ 1 ) → ...).

More generally, a moment at time t is actually identified with a sequence L of joint actions. That is why, we first define mappings tr L from the language L DLA (Atm, Agt, Act) into the language of S5formulas, indexed by a sequence of joint actions L. In the sequel, we write L for δ 0 0 ∧• • •∧δ t t if L = (δ 0 , . . . , δ t ) (δ j j meaning that joint action δ j is played at time j). We write for the empty sequence, L::δ for the sequence L where we added δ at the end of it, and |L| for denoting the length of L.

We define a translation function tr L by:

• tr L (p) = p |L| ; • tr L ( ϕ) = (L → tr L (ϕ)); • tr L ([[δ]]ϕ) = (δ |L| → tr L::δ (ϕ)).
In the clauses tr L (p) and tr L ([[δ]]ϕ), superscripts |L| refer to time |L|. In the clause tr L ( ϕ), the guard L → ... ensures that we are in the current moment, uniquely determined by sequence L because the determinism of DDLA.

Example 4. Let ϕ := (p → [[δ]] q). We have tr (ϕ) = (p 0 → (δ 0 → (δ 0 → q 1 ))).

Let S(ϕ) be the set of sequences L such that L = (δ 0 , . . . , δ t ) and [δ 0 ], . . . , [δ t ] is a list of nested modalities in that order in ϕ, of formulas. Note that the cardinality of S(ϕ) is polynomial in |ϕ|.

We define C1(ϕ) to be the formula

L∈S(ϕ) δ∈JAct        n i=1 ¬ ¬(L ∧ δ |L| i )        → ¬ ¬(L ∧ δ |L| )
Intuitively, C1(ϕ) expresses that the Constraint C1 of Definition 1 is true in all moments that the evaluation ϕ can reach, that is, in all moments reachable from a sequence L in S(ϕ). The guard L∧... ensures that we impose Constraint C1 in the moment uniquely determined by sequence L. We define actions(T ) to be the formula:

T t=0 [( δ∈JAct δ t ) ∧ ( δ,δ ∈JActδ δ δ t → ¬δ t )]
Intuitively, formula actions(T ) expresses that there exists a unique joint action δ that is performed at each time t up to depth T . The reduction is tr(ϕ) = tr (ϕ) ∧ C1(ϕ) ∧ actions(T ) where denotes the empty sequence and T the [δ]-modal depth of ϕ. tr(ϕ) can be computed in polynomial time in the size of ϕ. We have ϕ is DDLA-satisfiable iff tr(ϕ) is S5-satisfiable.

The rest of the section is devoted to prove: Theorem 5. Both DLA-sat and DDLA-sat are in PSPACE.

For both DLA and DDLA, we adapt a polynomial-space nondeterministic algorithm given in [START_REF] Schwarzentruber | Complexity results of STIT fragments[END_REF]. 6 Thus, by Savitch's theorem (NPSPACE = PSPACE) [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], Theorem 5 is proven. Let us define the multi-modal language, called L , whose modality are [t] for all integer t denoting the time t. A construction [t]ϕ means that ϕ holds for all histories passing through the moment at time t.

We first translate a DLA-formula ϕ into a L -formula tr 0 (ϕ) where tr t , for any integer t, is defined by:

• tr t (p) = p t ; • tr t ( ϕ) = [t]tr t (ϕ); • tr t ([[δ]]ϕ) = (δ t →tr t+1 (ϕ)); • tr t (Xϕ) = tr t+1 ϕ.
Whereas tr L (ϕ) in the proof of Theorem 4 is written with a single type of modality, tr t (ϕ) contains several types of modality [t] for each time t. We claim that a formula ϕ is DLA-satisfiable iff tr 0 (ϕ) is satisfiable in a Kripke structure where:

Example 5. Let ϕ := (p → [[δ]]( q ∧ Xr)). We have tr 0 (ϕ) = [0](p 0 → (δ 0 → ([1]q 1 ∧ r 2 ))).
K1 [t]-modality is interpreted by an equivalence relation R t ; K2 R t+1 is finer than R t ;
K3 all points in an R t+1 -equivalence class satisfy the same joint action δ t ; K4 an adaptation of Constraint C1 of Definition 1 holds in each R t -equivalence class with respect to propositions δ t .

Such a Kripke structure can be depicted as in Figure 5(a). The big rectangle is the moment at time 0 (an R 0 -equivalence class), sub-rectangles are sets of worlds where players choose the same joint actions at time 0, sub-sub-rectangles in the picture above are moment at time 1 (R 1 -equivalence classes), etc. Contrary to the proof of Theorem 4 where we quantified over worlds in a moment at time t by guarded constructions, here we quantify over worlds in a moment at time t with modality [t].

We moreover claim that a formula ϕ is DDLA-satisfiable iff tr 0 (ϕ) is satisfiable in a Kripke structure satisfying K1-K4 and: K5 an R t+1 -equivalence class consists exactly of those points where the same joint action δ t is played.

Such a Kripke structure can be depicted as in Figure 5(b). The big rectangle is again the moment at time 0 (an R 0 -equivalence class). But now, thanks to constraint K5, sub-rectangles and subsub rectangles coincide. Sets of worlds where agents choose the same joint actions at time 0 are exactly moments at time 1.

Let φ := tr 0 (ϕ). The set cl(φ) is the smallest set containing φ, closed under subformulas, negations and such that if [t]ψ ∈ cl(φ) then [t ]ψ ∈ cl(φ) for t < t and t smaller than any t in ϕ. The size of cl(φ) is polynomial in |ϕ|, where |ϕ| is the length of ϕ. Now, we concentrate on the satisfiability problem of DDLA. We will now explain step by step the pseudo-code given in Figure 4. The algorithm takes as an input a time t, the formula φ := tr 0 (ϕ) and a finite set Σ of Hintikka sets of φ defined as follows. 6 It is the algorithm for the satisfiability problem of atemporal STIT for coalitions of the form {1, . . . , i}. Definition 4. A Hintikka set H of φ is a subset of cl(φ) such that:

• if (ψ 1 ∧ ψ 2 ) ∈ H then ψ 1 ∈ H and ψ 2 ∈ H; • if ¬(ψ 1 ∧ ψ 2 ) ∈ H then ¬ψ 1 ∈ H and ¬ψ 2 ∈ H; • if ¬¬ψ ∈ H, then ψ ∈ H; • ψ H or ¬ψ H;
• for all t, there exists δ such that δ t ∈ H;

• for all t, for all δ δ , δ t H or δ t H;

• if [t]ψ ∈ H then ψ ∈ H and [t ]ψ ∈ H if t > t.
Intuitively, such a Hintikka set represents a world in a Kripke structure, that is, a history in a DDLA model.

The base case in the algorithm is when there is no [t ]-modality with t ≥ t in ψ: it means that we have considered enough steps in time. Otherwise, in the inductive case, we guess a t-witness set containing Σ. The role of a t-witness set is to represent the current moment at time t, that is, an R t -equivalence class. Formally: Definition 5. A t-witness set W of φ is a set of Hintikka sets such that

• if for all i ∈ {1, . . . , n}, there exists H i ∈ W such that δ t i ∈ H i , then there exists H ∈ W such that for all i ∈ {1, . . . , n}, δ t i ∈ H;

• if [t]ψ ∈ H ∈ W then for all H ∈ W, [t]ψ ∈ H ; • if ¬[t]ψ ∈ H ∈ W then there exists H ∈ W, ¬ψ ∈ H ;
• for all t < t, for all δ if δ t ∈ H ∈ W, then for all H ∈ W, δ t ∈ H .

The first item in Definition 5 is a reformulation of Constraint C1 of Definition 1. The second and third items correspond to the semantics of the [t]-operators. The last item means that previous joint actions (at time t < t) are the same in all Hintikka sets. We impose such a t-witness to contain at most max(n t (Σ) + |Σ|, |JAct|) Hintikka sets where n t (Σ) is the number of [t]-modalities in Σ. The bound |JAct| guarantees that we have a sufficient number of worlds for Constraint C1 of Definition 1. The bound n t (Σ) + |Σ| is imposed because we do not need to create more worlds than the number of subformulas of the form [t]ψ in φ that should be false.

We then perform all the recursive calls to explore consistency of next moments. Given a t-witness set W, a cell in W is the subset of Hintikka sets in W that all contain the same δ t for a given δ. The fact that recursive calls of satL are performed on cells corresponds to the constraint of determinism (C3) of Definition 3. Proposition 1. The two following statements are equivalent:

• H(t, φ, Σ): there exists a Kripke structure M satisfying (K1 -5) and a mapping f from Σ into a R t -equivalence class such that for all H ∈ Σ, all formulas that do not contain any [t ]-modality with t < t in H are true in M at point f (Σ);

• satL (t, φ, Σ) does not fail.

Proof. By induction on t. The base case corresponds to t such that there is no [t ]-modality with t ≥ t in φ. The result is true since we only consider Boolean formulas in Hintikka sets of Σ.

Inductive case. (⇓) Let M be as in the first statement. We consider the execution of satL (t, φ, Σ) that guesses a t-witness set W that is satisfied in M, that is such that the mapping f can be naturally extended from W into the R t -equivalence class such that for all H ∈ W, all formulas that do not contain any [t ]-modality with t < t in W are true. Such a W exists since:

• all ¬[t]ψ formulas that are true implies the existence of a world in the R t -equivalence class such that ¬ψ holds;

• and the number of such ¬[t]ψ is bounded by n t (φ). in M at point f (Σ).

Hence, for all cells C in W, we have H(t + 1, φ, C). By induction, we have that all calls satL (t + 1, φ, C) do not fail. Hence, call satL (t, φ, Σ) does not fail.

(⇑) Conversely, suppose that satL (t, φ, Σ) does not fail. Let W be the t-witness set. We have that for all cells C in W, calls satL (t + 1, ϕ, C) do not fail. By induction, H(t + 1, φ, C): there are M C models corresponding to each cell C. We construct a model M by gluing models M C and assigning the corresponding values to propositions p t and δ t : models M C corresponds to 'sub-rectangles' at time t + 1 and we juxtapose them to obtain a 'rectangle' at time t. We prove that we obtain a Kripke structure M satisfying (K1 -5) and such that there exists a mapping f from W into the R t -equivalence class as required in H(t, φ, Σ). In particular, the restriction of f to Σ makes H(t, φ, Σ) true. Proposition 2. Let H 0 be a Hintikka set containing φ. The call satL (0, φ, {H 0 }) requires a polynomial amount of memory in the size of φ.

Proof. The number of nested recursive calls is clearly bounded by O(|φ|). We only require to store at most O(|φ|) parameters Σ and local variables. It suffices to convince ourselves that |Σ| is polynomial in |φ|. Let n k be the maximal size of a set Σ at depth k in the tree of computation of satL (0, φ, {H 0 }). We have n 0 = 1. We have

n k ≤ max(n t (Σ) + n k-1 , |JAct|) ≤ max(|φ| + n k-1 , |JAct|). So n k is polynomial in |φ| for all k.
The algorithm for the DDLA-sat is: compute φ := tr 0 (ϕ), guess a Hintikka set H 0 , call satL (0, φ, {H 0 }). The algorithm for DLA-sat is similar except that 'for C : cell in M' is replaced by 'for C : singleton {H} such that H ∈ W' in the algorithm satL given in Figure 4. In other words, the Constraint C3 is dropped.

GAME DESCRIPTION LANGUAGE

In this section we shortly present the syntax and the semantics of a modal variant of GDL recently introduced in the AI community by [START_REF] Zhang | A logic for reasoning about game strategies[END_REF][START_REF] Zhang | Representing and reasoning about game strategies[END_REF] as a general logic for reasoning about strategies in general game playing. We abstract away from Zhangh and Thielscher (Z&T)'s modality α . At the end of the paper, we will introduce this modality when presenting perspectives of our future research.

GDL as defined by Z&T is deterministic. We also define a nondeterministic variant of GDL (IGDL) that relates with DLA.

Syntax

In GDL it is assumed that each agent i in the finite set of agents Agt is associated with a finite set of actions A i defining i's action repertoire and that if i j then A i ∩ A j = ∅. The set A = i∈Agt A i defines the set of all actions. The language L GDL (Prop, Agt, A) of GDL is defined by:

ϕ, ψ ::= p | ¬ϕ | (ϕ ∧ ψ) | initial | terminal | does(a) | legal(a) | [a]ϕ | a ϕ
where p ranges over the set of atomic propositions Atm and a ranges over A.

Intuitively, formula [a]ϕ means that "if action a is executed at the current state, ϕ is going to be true in the next state". Formula a ϕ means that "if action a were chosen (but not yet executed), then ϕ would be true".

Constants initial, terminal, does(a) and legal(a) denote, respectively, the fact that the current state is an initial state, that the current state is a terminal state, that action a is executed and that action a is legal.

Semantics

The semantics of GDL is based on state transition models. Definition 6. A state transition model is a tuple M = (X, I, T, U, L, V) such that:

• X is a non-empty set of worlds or states,7

• I ⊆ X is the initial states,

• T ⊆ X is the terminal states,

• U : X × A -→ X \ I is an update function,
• L ⊆ X × A is a legality relation, and

• V : X -→ 2 Atm is a valuation function.
Truth conditions of GDL formulas are given in the following definition.

Definition 7 (Truth conditions). Let M = (X, I, T, U, L, V) be a state transition model and let (x, a) ∈ X × A. Then:

M, (x, a) | = p ⇐⇒ p ∈ V(x) M, (x, a) | = ¬ϕ ⇐⇒ M, (x, a) | = ϕ M, (x, a) | = (ϕ ∧ ψ) ⇐⇒ M, (x, a) | = ϕ and M, (x, a) | = ψ M, (x, a) | = initial ⇐⇒ x ∈ I M, (x, a) | = terminal ⇐⇒ x ∈ T M, (x, a) | = does(b) ⇐⇒ a = b M, (x, a) | = legal(b) ⇐⇒ (x, b) ∈ L M, (x, a) | = [b]ϕ ⇐⇒ ∀c ∈ A : M, (U(x, b), c) | = ϕ M, (x, a) | = b ϕ ⇐⇒ M, (x, b) | = ϕ
As usual, a formula ϕ is GDL valid iff ϕ is true for all state transition models M = (X, I, T, U, L, V) and all (x, a) ∈ X × A. A formula ϕ is GDL satisfiable iff ¬ϕ is not GDL valid.

We here define a new non-deterministic variant of GDL (IGDL) that has the same language as GDL and that is interpreted with respect to non-deterministic state transition models. Definition 8. A non-deterministic state transition model is a tuple M = (X, I, T, U, L, V) where X, I, T, L, V are as in the definition of state transition model and:

• U : X × A -→ 2 X\I is a non-deterministic state transition function.
The only difference about the interpretation of formulas between GDL and IGDL is relative to the modality [b] that in IGDL is interpreted as follows: Definition 9 (Truth conditions (cont.)). Let M = (X, I, T, U, L, V) be a non-deterministic state transition model and let (x, a) ∈ X × A. Then:

M, (x, a) | = [b]ϕ ⇔∀c ∈ A and ∀y ∈ U(x, b) : M, (y, c) | = ϕ
Notions of validity and satisfiability for IGDL with respect to non-deterministic state transition models are defined in the expected way.

RELATIONSHIP BETWEEN GDL AND DLA

In this section we provide a polynomial translation of the GDL language into the DLA language and we show that our translation preserves validity. Before proving that the previous translation preserves satisfiability, let us introduce the following concept of ϕ-theory expressed in terms of the DLA language. Let ϕ be a GDL formula. Moreover, let Atm(ϕ) denote the set of atoms occurring in formula ϕ, let depth(ϕ) denote the modal depth of ϕ and let |ϕ| denote the length of ϕ. We define: where k = depth(ϕ). But we can actually avoid using X-modalities by taking τ(ϕ) to be: For every world x ∈ X, let H x denote the set of histories starting in state x, a history being an infinite sequence of state-action pairs ordered by the update function. That is:

Σ ϕ = { α ∨ ¬α : α ∈ Atm(ϕ) ∪ {initial, terminal}} ∪ { legal(δ) ∨ ¬legal(δ) : δ ∈ JAct} ∪ { [[δ]]¬initial : δ ∈ JAct} ∪ { δ : δ ∈ JAct}
τ(ϕ) = b∈S eq(ϕ)
H x = {x 0 , a 0 , x 1 , a 1 , . . . : x 0 = x and ∀k ≥ 0 : U(x k , a k ) = x k+1 } H = x∈X H
x denotes the set of all histories. Histories are denoted by symbols h, h , . . . For every h ∈ H and for every k ≥ 0, h state (k) denotes the state in the k-th position in h, while h action (k) denotes the action in the k-th position in h.

For every history h = x 0 , a 0 , x 1 , a 1 , . . ., h ≥1 = x 1 , a 1 , . . . denotes the longest proper suffix of h.

We build a corresponding structure M = (W, ≡, (C i ) i∈Agt , S , V ) as follows:

• W = H,
• for every h, h ∈ W, h ≡ h iff h state (0) = h state (0),

• for every i ∈ Agt and for every h ∈ W, C i (h) = f (h action (0)),

• for every h ∈ W, S (h) = h ≥1 ,

• every p ∈ Atm and for every h ∈ W, p ∈ V (h) iff p ∈ V(h state (0)).

It is routine to check that M is a DLA model. We have that there exists h ∈ H such that h state (0) = x and h action (0) = a. Moreover, by induction on the structure of ϕ, we can prove that M , h | = τ(ϕ) ∧ tr(ϕ) for every h ∈ H such that h state (0) = x and h action (0) = a.

(⇐) Let M = (W, ≡, (C) i∈Agt , S , V) be a DLA model and let w ∈ W such that M, w | = tr(ϕ).

We call the quotient set W/ ≡ the set of moments and denote it by Mom. Elements of Mom are denoted by m, m , . . . We build a corresponding structure M = (X, I, T, U, L, V ) as follows:

• X = Mom, • I = {m ∈ X : ∃w ∈ m such that M, w | = initial}, • T = {m ∈ X : ∃w ∈ m such that M, w | = terminal},
• for every m ∈ Mom and for every a ∈ A, U(m, a) = m iff ∃w ∈ m such that C(w) = f (a) and S (w) ∈ m ,

• L = {(m, a) ∈ X × A : ∃w ∈ m such that M, w | = legal(a)},
• for every p ∈ Atm and for every m ∈ X, p ∈ V (m) iff ∃w ∈ m such that p ∈ V(w).

It is routine to check that M is a well-defined GDL model. Moreover, by induction on the structure of ϕ, we can prove that M , (m, f -(C(w))) | = ϕ where f -is the inverse function of f and w ∈ m. Theorem 7. Let ϕ be in L GDL (Atm, Agt, A). Then, ϕ is IGDLsatisfiable iff τ(ϕ)∧tr(ϕ) is DLA-satisfiable.

Proof. The proof is similar to proof of Theorem 6. As for the ⇒-direction, we only need to change the definition of H x as follows:

H x = {x 0 , a 0 , x 1 ,

Complexities of GDL and IGDL

Although a sound and complete axiomatization for GDL has been given by [START_REF] Zhang | A logic for reasoning about game strategies[END_REF], the complexity of its satisfiability problem remains an open problem. Theorem 8. GDL-sat is NP-complete.

Proof. The NP-hardness comes from the fact that GDL is a conservative extension of classical propositional logic. The NPmembership comes from Theorem 4 and the polynomial-time reduction given in Theorem 6. Note that Theorem 8 strongly relies on the fact that τ(ϕ) ∧ tr(ϕ) does not contain any temporal operator X. The definition of the modal variant proposed by [START_REF] Zhang | A logic for reasoning about game strategies[END_REF][START_REF] Zhang | Representing and reasoning about game strategies[END_REF] does not have this temporal operator in the language. Note that if we extend the language of GDL by the temporal operator X, and we call GDL X the obtained language, we could reduce the satisfiability of GDL X into DDLA and obtain a PSPACE-upper bound. As for DDLA, the satisfiability problem of GDL X would have been PSPACE-hard.

Concerning Theorem 9, using a reduction involving the temporal operator X τ(ϕ) := 0≤i≤k X k χ∈Σϕ χ would also have given an PSPACE-upper bound since Theorem 5 does not impose a restriction to X-free formulas.

PERSPECTIVES

The variant of GDL presented in [START_REF] Zhang | A logic for reasoning about game strategies[END_REF] is equipped with an additional modal operator ψ that we have not considered so far. It is a model-update operator in the sense of dynamic epistemic logic [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. Formula ψ ϕ is read "ϕ holds, after the declaration that only the states in which ψ is true are legal". It is interpreted as follows: ] that guarantee the existence of a reduction procedure such that, for every GDL formula ϕ, it returns an equivalent GDL formula ϕ with no occurrence of the dynamic operators ψ . It is routine to verify that the reduction principles given by Z&T are also valid in the context of IGDL. Let us denote by dynGDL (dynIGDL) the GDL (IGDL) logic extended with ψmodalities. Thus, because of Theorems 8 and 9, both dynGDL-sat and dynIGDL-sat are decidable.

Actually, in order to simulate ψ ϕ-modality in DLA, we extend DLA (and DDLA) with modal-update operators of type [(p, ψ)], where the event (p, ψ) corresponds to a propositional assignment in the sense of [START_REF] Van Ditmarsch | Dynamic epistemic logic with assignment[END_REF]. The extensions are respectively denoted by dynDLA and dynDDLA. Formula [(p, ψ)]ϕ is read "ϕ holds, after the declaration that atom p should be true only in the worlds in which ψ holds". It is interpreted relative to a DLA (or DDLA) model M and world w in M as follows:

M, w | = [(p, ψ)]ϕ ⇐⇒ M (p,ψ) , w | = ϕ
where M (p,ψ) is the same as M except for replacing the valuation function V by the following function V (p,ψ) :

V (p,ψ) (w) = V(w) ∪ {p} if M, w | = ψ V (p,ψ) (w) = V(w) \ {p} if M, w | = ¬ψ
It is routine to verify that the following formulas are both dynDLA valid and dynDDLA valid:

[(p, ψ)]p ↔ ψ (1)
[(p, ψ)]q ↔ q if p q (2)

[(p, ψ)]¬ϕ ↔ ¬[(p, ψ)]ϕ (3)
[(p, ψ)](ϕ

1 ∧ ϕ 2 ) ↔ ([(p, ψ)]ϕ 1 ∧ [(p, ψ)]ϕ 1 ) (4)
[(p, ψ)] ϕ ↔ [(p, ψ)]ϕ

with ∈ { , [[δ]], X}. Since the rule of replacement of equivalents preserves both dynDLA and dynDDLA validity:

ψ 1 ↔ ψ 2 ϕ ↔ ϕ[ψ 1 /ψ 2 ] ( 6
)
by the preceding validities (1)-( 5), we can find a reduction procedure such that, for every formula ϕ of the language L DLA (Atm, Agt, Act) extended by the formulas [(p, ψ)]ϕ, it returns an equivalent formula ϕ without any dynamic operator [(p, ψ)].

Because of Theorem 5, this reduction guarantees that dynDLA-sat and dynDDLA-sat are decidable. Finally, dynGDL ψ -constructions are translated in dynDLA as follows: tr( ψ ϕ) = [(legal, tr(ψ))]tr(ϕ). Theorems 6 and 7 generalize straightforwardly to this new case.

An interesting perspective of future research is to study the complexity of of dynGDL-sat, dynIGDL-sat, dynDLA-sat and dynDDLA-sat. To this aim, we plan to adapt the technique proposed by [START_REF] Lutz | Complexity and succinctness of public announcement logic[END_REF] to study the complexity of public announcement logic (PAL).

Another perspective is to go beyond games with perfect information and to study the relation between the epistemic extension of DLA given in [START_REF] Herzig | A dynamic logic of agency I: STIT, abilities and powers[END_REF] and the epistemic extension of GDL proposed by [START_REF] Jiang | Epistemic GDL: A logic for representing and reasoning about imperfect information games[END_REF].

We also plan to consider a variant of GDL in which actions of agents are executed in parallel and with modal operators of type [δ], where [δ]ϕ has to be read "if the joint action δ is executed at the current state, ϕ is going to be true in the next state". We believe that this better corresponds to the way actions are represented in game theory. We plan to study its relationship with DLA and DDLA.

Finally, we plan to show how DLA and DDLA can be concretely used to model scenarios of general game playing and to highlight their advantages compared to IGDL and GDL.

2Figure 1 :

 1 Figure 1: Illustrations for constraints C1 and C2

Figure 2 :

 2 Figure 2: Structure of a (a) DLA model and (b) DDLA model

Figure 3 :

 3 Figure 3: Fresh propositions in the flattened version of a DDLA model

Figure 4 :Figure 5 :

 45 Figure 4: Non-deterministic subroutine satL used for the satisfiability problem of DDLA

4. 1

 1 Embedding of GDL into DLA Let us suppose that the cardinality of JAct (the set of joint actions in DLA) is equal to or bigger than the cardinality of A (the set of all actions in GDL). Hence there exists an injective function f from A to JAct: f (a) f (b) implies a b. Moreover, let Atm + = Atm ∪ {initial, terminal, legal}. Then, our translation is a function: tr : L GDL (Atm, Agt, A) -→ L DLA (Atm + , Agt, Act) such that for all α ∈ Atm ∪ {initial, terminal} and a ∈ A: tr(α) = α tr(¬ϕ) = ¬tr(ϕ) tr(ϕ ∧ ψ) = tr(ϕ) ∧ tr(ψ) tr(does(b)) = f (b) tr(legal(b)) = ( f (b) → legal) tr([b]ϕ) = [[ f (b)]] tr(ϕ) tr( b ϕ) = ( f (b) → ϕ)

Example 6 .Theorem 6 .

 66 b denotes a sequence b 1 , . . . , b , [ b] is [b 1 ][b 2 ] . . . [b ] and Seq(ϕ) is the set of sequences of actions as they appear in ϕ in the nesting order. Note that Seq(ϕ) is polynomial in |ϕ| therefore |τ(ϕ)| is polynomial in |ϕ|. The new definition τ(ϕ) clearly shows that we can express properties about the future by mentioning explicitly actions in the language without any occurrence of the temporal operator X. If ϕ = [a][b]p∧[c]q then S eq(ϕ) = { , (a), (a, b), (c)}. The two following theorems highlight that the previous translation provides both an embedding of GDL into DDLA and an embedding of IGDL into DLA. They are proven by transforming a GDL model (IGDL model) into a corresponding DDLA model (DLA model) and vice versa. Let ϕ be in L GDL (Atm, Agt, A). Then, ϕ is GDLsatisfiable iff τ(ϕ)∧tr(ϕ) is DDLA-satisfiable. Proof. (⇒) Let M = (X, I, T, U, L, V) be a state transition model, let x ∈ X and let a ∈ A such that M, (x, a) | = ϕ.

  a 1 , . . . : x 0 = x and ∀k ≥ 0 : x k+1 ∈ U(x k , a k )} As for the ⇐-direction, we only need to change the definition of the function U as follows: for every m ∈ Mom and for every a ∈ A, m ∈ U(m, a) iff ∃w ∈ m such that C(w) = f (a) and S (w) ∈ m .

Theorem 9 .

 9 IGDL-sat is PSPACE-complete.Proof. The PSPACE-hardness is proven by providing the following polynomial reduction tr of the satisfiability problem of modal logic K into the satisfiability problem of IGDL: tr(p) = p, tr( ϕ) := [a]tr(ϕ). The PSPACE membership comes from Theorem 5 and the polynomial-time reduction given in Theorem 7.

M

  , (x, a) | = ψ ϕ ⇐⇒ M ψ , (x, a) | = ϕ where the state transition model M ψ is the same as M except for replacing the legality relation L by the following relation: L ψ = {(x, a) ∈ X × A : M, (x, a) | = ψ}. Z&T provide reduction principles [28, Axioms D1-D8

Table 1 :

 1 Logics with new complexity results for the satisfiability problem (symbols denote upper bound results obtained via embedding.)

  function satL (t, φ, Σ : set of Hintikka sets) if there is a [t ] modality with t ≥ t in φ then Guess W a t-witness set of φ such that Σ ⊆ W and |W| ≤ max(n t (Σ) + |Σ|, |JAct|) Fail if the guess was not possible. for C : cells in W satL (t + 1, φ, C)

In the literature on STIT logic (cf.[START_REF] Balbiani | Alternative axiomatics and complexity of deliberative STIT theories[END_REF][START_REF] Lorini | Temporal STIT logic and its application to normative reasoning[END_REF][START_REF] Herzig | Properties of logics of individual and group agency[END_REF]), it is common to distinguish 'individual STIT' from 'group STIT'. The former only considers the consequences of the choices of individual agents, while the latter also considers the consequences of the collective choices of coalitions.

Alternative semantics for CL and ATL based on the concept of effectivity function are presented respectively by[START_REF] Pauly | A modal logic for coalitional power in games[END_REF] and[START_REF] Goranko | State and path coalition effectivity models of concurrent multi-player games[END_REF].

Z&T use the symbol W to denote the set of states. We use the symbol X to avoid confusion with the set of worlds in the semantics of DLA.


Keywords: Graph transformation, Description Logics, weakest precondition calculus, static analysis, alias calculus

We aim at assisting developers to write, in a Hoare style, provably correct graph transformations expressed in the ALCQ Description Logic. Given a postcondition and a transformation rule, we compute the weakest precondition for developers. However, the size and quality of this formula may be complex and hard to grasp. We seek to reduce the weakest precondition's complexness by a static analysis based on an alias calculus. The refined p recondition i s p resented t o t he d eveloper i n t erms of alternative formulae, each one specifying a potential matching of the source graph. The developer chooses then the formulae that correspond to his intention to obtain finally a correct-byconstruction Hoare triple.

A Precondition Calculus for Correct-by-Construction Graph Transformations

Amani Makhlouf, Christian Percebois, Hanh Nhi Tran IRIT, University of Toulouse Toulouse, France Email: {Amani.Makhlouf | Christian.Percebois | Hanh-Nhi.Tran}@irit.fr the rule is proved by a dedicated tableau reasoning, which is sound, complete and which results in a counter-example when a failure occurs.

Since writing complete and correct specifications may not be easy for novice developers, we aim to assist them in achieving provably correct transformations [START_REF] Makhlouf | Combining dynamic and static analysis to help develop correct graph transformations[END_REF]. In this context, we propose a static analysis of the weakest precondition based on an alias calculus in order to suggest precondition formulae that are easier to understand but still ensuring the correctness of the Hoare-triple. The result is presented to developers in a disjunctive normal form. Each conjunction of positive and negative literals specifies a potential matching of the source graph. By letting developers choose a conjunction as a premise that reflects the rule's intention, our approach can filter and reduce some combinatorial issues.

In this paper, Section II first defines logic-based formulae to annotate pre-and postconditions of a transformation rule. This choice yields manageable proof obligations in a Hoare's style for rules'correctness. Then, we introduce in Section III Small-tALC atomic statements that manipulate graph structures. Each statement is characterized by a weakest precondition with respect to a given postcondition. On the basis of an alias calculus that is presented in Section IV, we show in Section V how to reduce some combinatorial issues while ensuring the program correctness by finely analyzing the weakest precondition. An illustrative example is presented in Section VI. We finally give some discussions on related work in Section VII and wrap up the paper with a conclusion and possible improvements in Section VIII.

II. LOGIC-BASED CONDITIONS

Slightly diverged from the standard approach, we choose a set-theoretic approach for our transformation system [START_REF] Nagl | Set theoretic approaches to graph grammars[END_REF]. The basic idea is to specify sets of nodes and edges of a subgraph using a fragment of first-order logic. It turns out that replacing graph patterns by graph formulae yields manageable proof obligations for rules'correctness in a Hoare style {P }S{Q} [START_REF] Strecker | Modeling and verifying graph transformations in proof assistants[END_REF]. A precondition formula P designates a subgraph matching a substructure that should exist in the source graph. The postcondition Q requires the existence of the subgraph represented by Q in the target graph. For instance, consider a rule requiring that: [START_REF] Habel | Correctness of high-level transformation systems relative to nested conditions[END_REF] x must be a node (individual) not connected by the relation (role) R to a node y; (2) y is of class (concept) C; [START_REF] Courcelle | Graph Rewriting: An Algebraic and Logic Approach[END_REF] x is linked to at most three successors (qualified number of restrictions) of class C via I. INTRODUCTION All approaches applying production rules to a graph require to implement a binary relation between a source graph and a target graph. In the theory of algebraic graph transformations, Habel and Pennemann [START_REF] Habel | Correctness of high-level transformation systems relative to nested conditions[END_REF] defined nested graph conditions as a graphical and logical formalism to specify graph constraints by explicitly making use of graphs and graph morphisms. Nested conditions have the same expressive power as Courcelle's first-order g raph l ogic [START_REF] Habel | Correctness of high-level transformation systems relative to nested conditions[END_REF][2] [START_REF] Courcelle | Graph Rewriting: An Algebraic and Logic Approach[END_REF]. H owever, t hey n eed t o be derived into specific i nference r ules i n o rder t o b e proved in a specific t heorem-prover t hat s uits t hem [START_REF] Pennemann | Resolution-like theorem proving for high-level conditions[END_REF] [START_REF] Orejas | A logic of graph constraints[END_REF]. Moreover, this transformation requires the proof of a sound and complete proof system for reasoning in the proposed logic.

Another way to express and reason about graph properties is to directly encode graphs in terms of some existing logic [START_REF] Strecker | Modeling and verifying graph transformations in proof assistants[END_REF]. This solution leads to consider connections between graph constraints and first-order g raph f ormulae. A dopting t his approach, we define graphs axiomatically by ALCQ Description Logic (DL) predicates [START_REF] Baklanova | Coding, executing and verifying graph transformations with small-tALCQe[END_REF] and manipulate them with specific statements. In this way, we designed a non-standard imperative programming language named Small-tALC dedicated to transform labeled directed graphs. Note that ALC is prototypical for DLs.

Despite the above differences from algebraic graph transformations, we point out the common idea to use satisfiability solvers to prove rules'correctness. This technique requires to assign a predicate transformer to a rule in order to compute the rule's weakest precondition. The setup is rather traditional: given a Hoare triple {P }S{Q}, we compute the weakest (liberal) precondition wp(S, Q) of the rule transformation statements S with respect to the postcondition Q, and then verify the implication P ⇒ wp(S, Q). The correctness of R. This precondition can be expressed by the logic formula x ¬R y ∧ y : C ∧ x : (≤ 3 R C). At this point, readers familiar with Description Logics (DLs) may recognize a DL formula. Labeled directed graphs can be directly modeled by entities of DLs, a family of logics for modeling and reasoning about relationships in a domain of interest [START_REF] Krötzsch | A description logic primer[END_REF]. Most DLs are decidable fragments of firstorder logic. They are organized around three kinds of entities: individuals, roles and concepts. Individuals are constants in the domain, roles are binary relations between individuals and concepts are sets of individuals. Applied to our graphs, individuals are nodes labeled with concepts and roles are edges. Accordingly, pre-and post-assertions are interpreted as graphs by using unary predicates for nodes and binary predicates for edges. The correctness of a graph transformation rule is checked by assigning to each of its statements a predicate transformer in order to compute the corresponding weakest precondition.

To design our own experimental graph transformation language, we chose the ALCQ logic, an extension of the standard DL Attributive Language with Complements (ALC) [START_REF] Schmidt-Schauß | Attributive concept descriptions with complements[END_REF], which allows qualifying number restrictions on concepts (Q). ALCQ is based on a three-tier framework: concepts, facts and formulae. The concept level enables to determine classes of individuals (Ø, C, ¬C, C1 ∪ C2 and C1 ∩ C2). The fact level makes assertions about individuals owned by a concept (i : C, i : ¬C, i : (≤ n R C) and i : (≥ n R C)), or involved in a role (i R j and i ¬R j). The third level is about formulae defined by a Boolean combination of ALCQ facts (f, ¬f, f 1 ∧ f 2 and f 1 ∨ f 2).

Figure 1 depicts a model (graph) satisfying the previous precondition x ¬R y ∧ y : C ∧ x : (≤ 3 R C). In this graph, the white circles designate the nodes variables x and y manipulated by the formula. Nodes variables refer (by a dotted edge) to real nodes represented by black circles. The « » node outlines a concept labeled with C. Note that the subgraph having two anonymous nodes each one outfitted with an incoming edge from x and an outgoing edge to the concept C is a model which checks the fact x : (≤ 3 R C).

used in atomic transformation actions on nodes (individuals) and edges (roles), as well as in traditional control-flow constructs as loops (while) and conditions (if...then...else...). In the transformation code, statements manipulate node variables which are bound to the host graph's nodes during the transformation's execution.

We have defined five atomic Small-tALC statements according to the following grammar where i and j are node variables, C is a concept name, R is a role name, F is an ALCQ formula and v is a list of node variables: atomic_statement ::= add(i : C)

(node labeling) | delete(i : C) (node unlabeling) | add(i R j) (edge labeling) | delete(i R j) (edge unlabeling) | select v with F (assignment)
The first four statements modify the graph structure by changing the labeling of nodes and edges. Note that since we consider a set-theoretic approach, the statements add(i : C) and add(i R j) have no effects if i belongs to the set C and (i, j) to R respectively. Hence, no parallel edges with the same label are allowed. An original construct is the select statement that non-deterministically binds node variables to nodes in the subgraph that satisfies a logic formula. This assignment is used to handle the selection of specific nodes where the transformations are requested to occur. For instance, select i with i : C selects a node labeled with C. If the selection is satisfied the execution continues normally with the value of the node variable i. Otherwise, the execution meets an error situation.

A Small-tALC program consists of a sequence of transformation rules. A rule is structured into three parts: a precondition, the transformation code (a sequence of statements) and a postcondition. We illustrate in Figure 2 an example of a transformation rule written in Small-tALC. The rule first selects a node n of concept A that is R-linked to a. Then, it deletes this link and removes a from the concept A.

pre: We aim at using a Hoare-like calculus to prove that Small-tALC graph programs are correct. This verification process is based on a weakest (liberal) precondition (wp) calculus [START_REF] Dijkstra | Predicate Calculus and Program Semantics[END_REF]. Each Small-tALC statement S is assigned to a predicate transformer yielding an ALCQ formula wp(S, Q) assuming the postcondition Q. The correctness of a program prg with respect to Q is established by proving that the given precondition P implies the weakest precondition: every model that satisfies P also satisfies wp(prg, Q). Weakest preconditions of Small-tALC statements are given in Figure 3.

(a : A) ∧ a : (≥ 3 R A); select n with (a R n) ∧ (n : A) delete(a R n); delete(a : A); post: (a : ¬A) ∧ a : (≥ 2 R A);
The weakest precondition calculus computes predicates which are not closed under substitutions with respect to Our formulae contain free variables that assign references to nodes in a graph. Equality and inequality assertions can be used to define constraints on the value o f these variables. If x and y are node variables, x = y means that x and y refer to the same node and x = y means that x and y are distinct. The inequality relationship enforces injective graph morphisms.

III. THE SMALL-TALC LANGUAGE

The ALCQ formulae presented in the previous section have been plugged into our Small-tALC imperative language and wp(add

(i : C), Q) = Q[C + i/C] wp(delete (i : C), Q) = Q[C -i/C] wp(add (i R j), Q) = Q[R + (i, j)/R] wp(delete (i R j), Q) = Q[R -(i, j)/R] wp(select v with F, Q) = ∀v(F ⇒ Q) Figure 3
. Small-tALC weakest preconditions ALCQ. To resolve this situation, substitutions are considered as constructors and should be eliminated. For instance, wp(add(i : C), x :

C) = x : C [C + i/C] = x : (C + i) = x : C ∨ x = i.
The conventional precondition calculus presented above does not take into account particular situations of a transformation program and thus may result in a complex precondition. In the following sections, we look at how the precondition's formula can be improved to be more specific and simple on the basis of an alias calculus.

IV. ALIAS CALCULUS

The principle of alias calculus was proposed by Bertrand Meyer in order to decide whether two reference expressions appearing in a program might, during some execution, have the same value, meaning that the associated references are attached to the same object [START_REF] Meyer | Steps towards a theory and calculus of aliasing[END_REF].

Since our rewriting system allows non-injective morphisms, two or more node variables may reference to the same node in a graph. On the other hand, a node variable can be assigned to a random node of the graph. This is one reason why a Small-tALC formula can be represented by several graph patterns. For example, Figure 4 shows two potential models satisfying the formula x : C ∧ i R j. In Figure 4a, i and j refer to the same node. In 4b, i and j are different but i and x are combined. In this regard, for a transformation program, we apply an alias calculus to determine the node variables that can never refer to the same node. Discerning such specific circumstances helps to discard later unsatisfied subformulae of the weakest precondition. Thus, our method consists in assigning to each node variable x, a set of other node variables that may reference to the same node in the graph as x. We identify four atomic conditions in which two individuals x and y can never refer to the same node in the graph:

(a) i = j, i = x (b) i = j, i = x
• x = y • ∃C /x : C ∧ y : ¬C • ∃R.∃z /x R z ∧ y ¬R z • ∃R.∃z /z R x ∧ z ¬R y
The first case (x = y) states that x and y are naturally distinct so they can never be assigned to the same node. The second one asserts that x and y belong to two complement subsets C and ¬C. The same applies to the last two cases where the nodes connected by R and ¬R refer to two disjoint subsets R and ¬R.

For each of the above four conditions, x and y are said to be non-possibly equivalent nodes. We note this relation by x y. As a result we assert that x y ⇒ x = y. However, no conclusion can be drawn from the possibly equivalent relation x y.

Consider, as a simple example, the following formula that is presented in the disjunctive normal form: (x = y ∧ x R y) ∨ (x : C ∧ x ¬R y), and suppose that a static analysis deduces from the code that x and y are non-possibly equivalent, which means that x = y. As a result, the initial formula can be reduced to x : C∧x ¬R y because the first conjunction x = y∧ x R y can never be true in this case. In the section that follows, we show how this calculus helps in reducing the complexness of the weakest precondition.

V. PRECONDITION EXTRACTION To formally verify the correctness of a Small-tALC graph transformation, besides the code, the program's pre-and postconditions must be properly specified. This task may not be easy for novice developers, so a suggestion of a valid precondition that corresponds to a given code and a postcondition would be useful to them.

Since the computed weakest precondition is often very complex and hard to comprehend, we propose a finer static analysis on the basis of the alias calculus of the program to achieve a simpler precondition. The resulting precondition P is presented in a disjunctive normal form (DNF) where each conjunction of P can be considered as a valid precondition on its own. The analysis consists first in converting the postcondition Q to DNF i.e., Q = ∨Q i where Q i = ∧q j is a conjunction of facts, then calculating for each statement and for each conjunction Q i the weakest precondition. This process maintains correctness because wp(S, Q 1 ) ∨ wp(S, Q 2 ) ⇒ wp(S, Q 1 ∨ Q 2 ). In each and every step, the formula of the wp(S, Q i ) may be filtered by discarding subformulae according to the identified non-possibly equivalent node variables. A precondition P is obtained such that P ⇒ wp(prg, Q), which makes the transformation program prg correct. This process is applied to add and delete statements as detailed in Section V-1. Regarding the select statement, wp is reduced differently as presented later in Section V-2.

1) add and delete statements: Let us consider first the add(i : C) statement. Its weakest precondition with respect to the postcondition x : C is x : C ∨ x = i, which means that either the node x was already of concept C before adding i to C, or x and i are equal. Knowing that x and i are non-possibly equivalent, it can be stated that x = i, and so the weakest precondition can be reduced to the first subformula x : C of the disjunction.

A more glaring example is reducing the weakest precondition of the add(i R j) statement with respect to the postcondition Q = x : (≤ n R C) which indicates that there are at most n edges labeled R outgoing from the node x to nodes of concept C. Adding an R-edge between i and

x : C ∨ x = i x i x : C x : ¬C x : ¬C ∧ x = i x i x : ¬C x : (≤ n R C) (x R i ∧ i : ¬C ∧ x : (≤ (n -1) R C)) ∨ (x ¬R i ∧ x : (≤ n R C)) ∨ (i : C ∧ x : (≤ n R C)) ∨ (x : (≤ (n -1) R C))
x ¬R i x : (≤ n R C)

add(i R j) x R y (x = i ∧ y = j) ∨ x R y x i ∨ y j x R y x ¬R y (x = i ∨ y = j) ∧ (x ¬R y) x i ∨ y j x ¬R y x : (≤ n R C) (x = i ∧ j : C ∧ i ¬R j ∧ x : (≤ (n -1) R C)) ∨ (x = i ∧ x : (≤ n R C)) ∨ (j : ¬C ∧ x : (≤ n R C)) ∨ (i R j ∧ x : (≤ n R C)) ∨ (x : (≤ (n -1) R C))
x i ∨ j : ¬C x : (≤ n R C) j may have a direct impact on Q regarding the concept of j, the existence of a relation between i and j and the equality between i and x. Hence, wp(add(i R j), x :

(≤ n R C)) = (x = i ∧ j : C ∧ i ¬R j ∧ x : (≤ (n -1) R C)) ∨ (x = i ∧ x : (≤ n R C)) ∨ (j : ¬C ∧ x : (≤ n R C)) ∨ (i R j ∧ x : (≤ n R C)) ∨ (x : (≤ (n -1) R C))
Consider the first row of the Table II. If a fact x R y is identified within the postcondition during calculation, we look for simplifying wp(add(i R j), x R y) = (x = i ∧ y = j) ∨ x R y. If the alias calculus asserts that at least one of the conditions x i or y j is true, wp is reduced to x R y.

As observed in Tables I and II, many complex disjunctions in the wp can be reduced to only one conjunction on the basis of a condition calculated by the alias calculus or a condition given explicitly in the postcondition. Note that the results of the delete(i : C) and delete(i R j) statements are similar to the add statements.

2) The select statement: So far, the static analysis transforms the predicate Q into a new predicate P regarding statements already presented. However, it operates differently when it comes to the select statement where wp(select v with F, Q) = ∀v (F ⇒ Q). The weakest precondition here involves two formulae that may be complex: F given by the select, and the postcondition Q. Consequently, the implication F ⇒ Q makes the wp more obscure for the developer. In this case, the static analyzer simplifies the wp by eliminating this implication as further detailed below.

For each conjunction Qi of the postcondition Q, the static analysis isolates first the facts that manipulate the node variables v of the select statement. Let Qi v be the conjunctive formula of these identified facts, and Qi v the conjunctive formula of the others facts, so that Qi = Qi v ∧ Qi v . For example, given a formula Q 1 = x R y∧y : C and the statement select x with x : C, we have

Q 1v = x R y and Q 1v = y : C.
Then, the static analysis checks, via our logic formula evaluator, if the implication ∀v (F ⇒ Qi v ) holds. If so, the precondition wp(select v with F, Qi) = ∀v (F ⇒ Qi) is reduced to Qi without affecting the validity of the Hoare triple as Qi ⇒ wp(select v with F, Qi). Conversely, the non-validity of the implication ∀v (F ⇒ Qi v ) results in transforming Qi to the predicate f alse (⊥) so that nothing can be concluded Knowing that x i or j : ¬C, the first c onjunction x = i ∧ j : C ∧ i ¬R j ∧ x : (≤ (n-1) R C) can be discarded as it will never be satisfied in this case. Furthermore, the whole formula of the wp can be reduced to x : (≤ n R C) according to the second and third conjunction which indicates that the number of restrictions remains unchanged in case one of these two conditions is satisfied.

We illustrated how to reduce the wp with respect to a postcondition composed of a single fact. In case of a postcondition consisting of a conjunction of facts, only the facts that manipulate the same concepts and roles given in the statement parameters are identified a s a fi rst st ep. Fo r ex ample, adding an instance to a concept (add(i : C) results in considering in the given postcondition only the facts that manipulate this concept (x : C, x : ¬C, x : (≤ n R C)).

Tables I and II represent the preconditions calculated by our static analyzer for the statement add(i : C) and add(i R j) respectively. For each statement s, we show in the second column the facts that should be identified in the postcondition to derive a precondition. The third column shows the standard weakest precondition wp(s, f) of the statement s with respect to an identified f act f . T o s implify t his f ormula, w e present in the fourth column the conditions that allow to discard some conjunctive clauses of the wp. The resulting formula is presented in the last column. about the transformation correctness. This situation is meant to warn the developer that there are inconsistencies in his transformation between the select statement and the predicate formula Q. The two presented cases are given in Table III.

select v with F Qi ∀v (F ⇒ Qi) ∀v (F ⇒ Qiv) Qi ∀v (F ⇒ Qiv) ⊥
We presented how the static analyzer filters the weakest precondition of a statement with respect to each conjunction Q i = ∧q j of Q where Q = ∨Q i . Hence, the final result of the precondition will be presented as a DNF formula too that expresses different possible alternatives. Each alternative represents a conjunction of facts, constituting a graph that matches a subgraph of the source graph on which the transformation rule is applied.

We filter the weakest precondition by discarding conjunctive clauses that are invalid. This reduction leads to a precondition P stronger than the weakest precondition wp(S, Q). In particular, when two node variables are non-possibly equivalent, a deductive reasoning is carried out by applying equivalence and implication connectives between P and wp(S, Q). We adopt a similar deduction for a node variable belonging to a concept complement and for a role complement. Using these deductions and the well-behaved wp properties, such as distributivity of conjunction and disjunction, we construct the formula P , which satisfies the implication P ⇒ wp(S, Q) so that the triple {P }S{Q} is always correct-by-construction.

VI. EXAMPLE

Using the static analyzer to suggest a precondition formula in the disjunctive normal form, the developer can select the conjunctions that reflect his intention. He can then update his transformation code or refine his specification by injecting into them the facts of the chosen conjunctions.

Consider as an example the transformation code and the postcondition given in Figure 5. The first statement adds a node y to the concept C. The second one adds an R-edge between nodes x and y. The postcondition asserts that x has at most three R-successors to nodes of concept C, and that y belongs to C. To achieve the given postcondition, a precondition calculus is done in two stages: the first to extract a precondition P with respect to the statement add(x R y) and the given postcondition, the second to extract a precondition with respect to the statement add(y : C) and P , as wp(s1; s2, Q) = wp(s1, wp(s2, Q)). Consequently, the static analyzer extracts seven possible conjunctions as a precondition:

x : (≤ 1 R C) (1)
y : C ∧ x : (≤ 2 R C) (2)
x R y ∧ x : (≤ 2 R C)

x ¬R y ∧ x : (≤ 2 R C)

x ¬R y ∧ y : C ∧ x : (≤ 2 R C)

x R y ∧ y : ¬C ∧ x : (≤ 2 R C)

x R y ∧ y :

C ∧ x : (≤ 3 R C) (7)
Each of these conjunctions is a potential precondition that yields a correct Hoare triple. The first formula is the weakest one. It does not take into account neither the concept of y nor the existence of an R-edge between x and y. On the contrary, the other conjunctions are stronger formulae specifying the mentioned properties of x and y. For example, the formula [START_REF] Baklanova | Coding, executing and verifying graph transformations with small-tALCQe[END_REF] indicates that there exists an R-edge between x and y and that y is of concept C. In this case, both of the two statements of the code have no effects, and so the number of restrictions remains 3 in the fact x : (≤ 3 R C). The various levels of formulae's strength gives the choice to the developer to specify the constraints of rule's applicability in the precondition as much as he wishes to.

Suppose that the developer focuses on the non-existence of an R-edge between x and y before the transformation as it is indicated in the formulae (4) and [START_REF] Orejas | A logic of graph constraints[END_REF]. Thus, he decides to inject the fact x ¬R y into the transformation by adding the statement select y with x ¬R y at the beginning of his code. By relaunching the static analyzer, the number of conjunctions extracted decreases from seven to one conjunction which is x : (≤ 2 R C). At this point, the developer can choose to put the resulting formula as a precondition as shown in Figure 6. In this sense, we help developers to update and annotate their code with specifications based on their intention to achieve finally a correct-by-construction triple.

As described below, our framework guides developers to achieve correct transformation programs. Moreover, it verifies the resulting triple formally using the Small-tALC prover. The latter is a formal verification tool that verifies a transformation program with respect to its pre-and postconditions by translating it into Isabelle/HOL logic and generating verification conditions. In case of failure, the prover displays a counterexample which is a model of the precondition that does not satisfy the postcondition when applying the transformation.

VII. RELATED WORK

Most of the logic-based approaches for graph transformations focus on the verification question. Thus, they attempt to encode graph conditions in an appropriate logic that is both expressive and decidable. Like us, Selim et al. [START_REF] Selim | Specification and verification of graph-based model transformation properties[END_REF] proposed a direct verification framework for their transformation language DSLTrans so that no intermediate representation for a specific proving framework is required. They used symbolic execution to build a finite set of path conditions representing all transformation executions through a formal abstraction relation and thus allow formal properties to be exhaustively proved. Their property language based on graph patterns and propositional logic proposes a limited expressiveness and the propertyproving algorithm was presented as a proof-of-concept.

The works in [START_REF] Becker | Iterative development of consistency-preserving rule-based refactorings[END_REF] and [START_REF] Clarisó | Backwards reasoning for model transformations[END_REF] share with ours some ideas with respect to the assistance in producing a Hoare triple. Given a modeling language with well-formedness constraints and a refactoring specification, Becker et al. [START_REF] Becker | Iterative development of consistency-preserving rule-based refactorings[END_REF] uses an invariant checker to detect and report constraint violations via counter-examples and lets developers modify their refactoring iteratively. Similarly to us, Clariso et al. [START_REF] Clarisó | Backwards reasoning for model transformations[END_REF] used backward reasoning to automatically synthesize application conditions for model transformation rules. Application conditions are derived from the OCL expression representing the rules's postconditions and the atomic rewriting actions performed by the rule. However, OCL expressions are not really suitable for exploring the graph properties of the underlying model structures. It is thus rather cumbersome when used for verifying complex model transformations.

VIII. CONCLUSION AND FUTURE WORK

The distinctive feature of Small-tALC is that it uses the same logic ALCQ to represent graphs, to code a transformation and to reason about graph transformations in a Hoare style. In order to assist users in developing correct transformations, we propose a fine analysis of the weakest precondition to take into account special situations of a program on the basis of an alias calculus. Our approach allows developers to select a precondition to annotate their code according to their intention.

It would be interesting in our framework to automatically infer and test invariant candidates for loop constructs gathered from their corresponding postcondition 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-tALC loop often iterates on individuals selected from a logic formula in order to achieve the same property for the transformed elements.

As a complement to a Hoare triple verification, we expect to focus on effects of rules execution in terms of DL reasoning services at the specification rule level. A Small-tALC rule execution updates a knowledge base founded upon a finite set of ALCQ concept inclusions (TBox) and a finite set of ALCQ concept and role assertions (ABox). This leads to a reasoning problem about a knowledge base consistency embodied by a graph in Small-tALC [START_REF] Sattler | Reasoning in description logics: Basics, extensions, and relatives[END_REF].

Figure 2 .

 2 Figure 2. Example of a Small-tALC rule

Figure 1 .

 1 Figure 1. Model satisfying the precondition x ¬R y ∧ y : C ∧ x : (≤ 3 R C)

Figure 4 .

 4 Figure 4. Example of models satisfying the formula x : C ∧ i R j

  add(y : C); add(x R y); post: x : (≤ 3 R C) ∧ (y : C);

Figure 5 .

 5 Figure 5. Example of an initial code and postcondition

  pre: x : (≤ 2 R C); select y with x ¬R y; add(y : C); add(x R y); post: x : (≤ 3 R C) ∧ (y : C);

Figure 6 .

 6 Figure 6. The final correct-by-construction triple

TABLE I .

 I WEAKEST PRECONDITION'S FILTERING FOR THE add(i : C) STATEMENT

	Statement	Identified fact	wp	Condition	Precondition
		x : C
	add(i : C)

TABLE II .

 II WEAKEST PRECONDITION'S FILTERING FOR THE add(i R j) STATEMENT

	Statement	Identified fact	wp	Condition	Precondition

TABLE III .

 III REDUCING THE WP OF THE select STATEMENT

	Statement	Postcondition	wp	Condition	Precondition

ACKNOWLEDGMENT

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