Joseph Boudou

Andreas Herzig

Nicolas Troquard

Resource Separation in Dynamic Logic of Propositional Assignments

Keywords: Dynamic logic, separation logic, propositional assignments, parallel composition, concurrency

We extend dynamic logic of propositional assignments by adding an operator of parallel composition that is inspired by separation logics. We provide an axiomatisation via reduction axioms, thereby establishing decidability. We also prove that the complexity of both the model checking and the satisfiability problem stay in PSPACE.

Introduction

It is notoriously delicate to extend Propositional Dynamic Logic PDL with an operator of parallel composition of programs. Several attempts were made in the literature: Abrahamson as well as Mayer and Stockmeyer studied a semantics in terms of interleaving [START_REF] Abrahamson | Decidability and expressivity of logics of processes[END_REF][START_REF] Mayer | The complexity of PDL with interleaving[END_REF]; Peleg and Goldblatt modified the interpretation of programs from a relation between possible worlds to a relation between possible worlds and sets thereof [START_REF] Peleg | Concurrent dynamic logic[END_REF][START_REF] Goldblatt | Parallel action: Concurrent dynamic logic with independent modalities[END_REF]; Balbiani and Vakarelov studied the interpretation of parallel composition of programs π 1 and π 2 as the intersection of the accessibility relations interpreting π 1 and π 2 [START_REF] Balbiani | PDL with intersection of programs: A complete axiomatization[END_REF]. However, it seems fair to say that there is still no consensus which of these extensions is the 'right' one.

Dynamic Logic of Propositional Assignments DL-PA [BHT13,BHST14] is a version of Propositional Dynamic Logic (PDL) whose atomic programs are assignments of propositional variables p to true or false, respectively written +p and -p. We and coauthors have shown that many knowledge representation concepts and formalisms can be captured in DL-PA, such as update and revision operations [START_REF] Herzig | Belief change operations: a short history of nearly everything, told in dynamic logic of propositional assignments[END_REF], database repair [START_REF] Feuillade | A Dynamic Logic Account of Active Integrity Constraints[END_REF], lightweight dynamic epistemic logics [CS15,CHM + 16,CS17], planning [START_REF] Herzig | On the revision of planning tasks[END_REF], and judgment aggregation [START_REF] Novaro | Judgment aggregation in dynamic logic of propositional assignments[END_REF]. The mathematical properties of DL-PA are simpler than those of PDL, in particular, the Kleene star can be eliminated [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF] and satisfiability and model checking are both PSPACE complete [START_REF] Balbiani | DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE[END_REF].

In this paper we investigate how dynamic logic can be extended with a program operator of parallel composition π 1 ||π 2 of two programs π 1 and π 2 that is inspired by separation logic. The latter was studied in the literature as an account of concurrency, among others by Brookes and by O'Hearn [O'H04, [START_REF] Stephen | A semantics for concurrent separation logic[END_REF][START_REF] Brookes | Concurrent separation logic[END_REF]. Their Concurrent Separation Logic is characterised by two main principles:

1. When two programs are executed in parallel then the state of the system is partitioned ('separated') between the two programs: the perception of the state and its modification is viewed as being local to each of the two parallel programs. Each of them therefore has a partial view of the global state. This entails that parallelism in itself does not modify the state of the system: the parallel execution of two programs that do nothing does not change the state. The formula ϕ → ?|| ? ϕ should therefore be valid, where " ?" is the test that is true (which always succeeds). 2. The execution of a parallel program π 1 ||π 2 should be insensitive to the way the components of π 1 and π 2 are interleaved. Hence "race conditions" [START_REF] Brookes | Concurrent separation logic[END_REF] must be avoided: the execution should not depend on the order of execution of atomic programs in π 1 and π 2 (where we consider tests to be atomic, too). Here we interpret this requirement in a rather radical way: when there is a race condition between two programs then they cannot be executed in parallel. For example, the parallel program +p||-p where +p makes p true and -p makes p false is inexecutable because there is a conflict: the two possible interleavings +p; -p and -p; +p are not equivalent. We even consider that +p||+p is inexecutable, which some may consider a bit over-constrained 4 .

In formal frameworks for the verification of parallel programs such as the one proposed by Brookes and O'Hearn [Bro04,O'H04], allowing race conditions is a necessary feature for the framework to be able to prove a property of programs, namely that they are race-free. On the contrary, dynamic logics permit to prove properties of formulas, and atomic actions are actually even totally abstracted away in most dynamic logics. In such abstract settings, whether two given atomic actions can be executed concurrently is a semantic detail of each model. For instance, in dynamic logics with a parallel composition based on separation (like in [START_REF] Mario | Propositional dynamic logic with storing, recovering and parallel composition[END_REF][START_REF] Boudou | Complexity optimal decision procedure for a propositional dynamic logic with parallel composition[END_REF][START_REF] Balbiani | Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization[END_REF]), the separation relation of the model provides the possibility to forbid race conditions. The race condition issue arises in logics based on DL-PA because atomic actions are concrete: basically, each atomic action potentially changes the valuation of exactly one propositional variable. Hence it is natural to consider access to the propositional variables as the main resource. In this perspective, a decision has to be made on whether the separation of these resources is strict or not, i.e., whether race conditions are allowed or not. In the present work, we have chosen a strict separation semantics because it is the simplest solution satisfying the two principles stated above.

We have not yet said what one should understand by a DL-PA system state. A previous approach of one of us only considered the separation of valuations, i.e., of truth values of propositional variables [START_REF] Herzig | A simple separation logic[END_REF]. Two separating conjunctions in the style of separation logic were defined on such models. This however did not allow one to define an adjoint implication as usually done in the separation logic literature, which was somewhat unsatisfactory. Another paper that was coauthored by one of us has richer models: valuations are supplemented by information about writability of variables [START_REF] Herzig | Dynamic logic of parallel propositional assignments and its applications to planning[END_REF]. It is supposed that a variable can only be assigned by a program when it is writable. Splitting and merging of such models can be defined in a natural way, thus providing a meaningful interpretation of parallel composition. When parallel composition is based on separation, writability information permits to resolve merge conflicts. Consider for instance the executions of the two programs ?||+p and -p||+p from a state in which p is false. We argue that intuitively, the former program should lead to a state in which p is true whereas the latter program should either not be executable or non-deterministically lead to two possible states, one where p is true and one where p is false. However, without writability information, the states before the merge of each of these programs turn out to be identical: p is false in the left branch but true in the right branch. Writability information allows the merge operation to distinguish these two situations and to resolve the conflict in the former case.

We here push this program further and consider models having moreover information about readability of variables. We suppose that writability implies readability5 and that a variable can only be tested if it is readable. Our tests ϕ? ? therefore differ from the standard tests of PDL and DL-PA in that their executability depends on whether the relevant variables are readable. In particular, while p? ? → p, remains valid, its converse p → p? ? becomes invalid in our logic: it may be the case that p is true but cannot be read.

Distinguishing the variables that can be tested permits some useful checks. Consider for instance the execution of the program (-p; q? ?) || (-q; p? ?) from a state in which both p and q are true. Without readability, this program can be executed and results in a state in which both p and q are false. However, no interleaving of this program can be executed. Adding readability of variables permits to detect this issue: we enforce that a variable cannot be read by one subprogram of a parallel composition if it can be written by the other subprogram.

The paper is organised as follows. In Section 2 we define models and the two ternary relations 'split' and 'merge' on models. In Section 3 we define the language of our logic and in Section 4 we give the interpretation of formulas and programs. In Section 5 we axiomatise the valid formulas by means of reduction axioms and in Section 6 we establish that the satisfiability problem is PSPACE complete. Section 7 sums up our contributions and discusses related work and the application to parallel planning. The annex contains a proof of associativity of parallel composition.6

Models and Their Splitting and Merging

Let P be a countable set of propositional variables. We use p, q, . . . for elements of P. A model (alias a system state) is a triple m = Rd, Wr, V where Rd, Wr, and V are subsets of P such that Wr ⊆ Rd. The intuition is that Rd is the set of readable variables, Wr is the set of writable variables, and V is a valuation: its elements are true, while those of its {p, q, r}, {p, q}, {p, q, r} {p, r}, {p}, {p, q, r} {q, r}, {q}, {p, q, r} {p, r}, {p}, {q, r} {q, r}, {q}, {p, r} {p, q, r}, {p, q}, {r} Fig. 1. Examples of split and merge operations: the left side illustrates the split of the model {p, q, r}, {p, q}, {p, q, r} into {p, r}, {p}, {p, q, r} and {q, r}, {q}, {p, q, r} ; the right side illustrates the merge of the models {p, r}, {p}, {p, q, r} and {q, r}, {q}, {p, q, r} into {p, q, r}, {p, q}, {r} . complement P \ V are false. The constraint that Wr ⊆ Rd means that writability implies readability.

The special case when Wr = P is typical when checking the validity or the satisfiability of a formula ϕ. Lemma 1 in Section 4 will prove that, as expected, this case is equivalent to the case where Wr and Rd are the set of propositional variables occurring in ϕ. In fact, the writability and readability sets are mostly useful for checking properties of subprograms of parallel compositions. On the other end of the spectrum, the case Wr = ∅ is of little interest since the only executable programs will be those without assignments.

Two models m 1 = Rd 1 , Wr 1 , V 1 and m 2 = Rd 2 , Wr 2 , V 2 are RW-disjoint if and only if the writable variables of one model and the readable variables of the other are disjoint, i.e., if and only if Wr 1 ∩ Rd 2 = Wr 2 ∩ Rd 1 = ∅. For example, m 1 = {p}, {p}, ∅ and m 2 = {p}, ∅, ∅ fail to be RW-disjoint: in m 1 , some program π 1 modifying the value of p may be executable, while for programs executed in m 2 , the value of p may differ depending on whether it is read before or after the modification by π 1 took place.

As writability implies readability, RW-disjointness of m 1 and m 2 implies that Wr 1 and Wr 2 are disjoint.

We define ternary relations ('split') and ('merge') on models as follows:

m m 1 m 2 iff m 1 and m 2 are RW-disjoint, Rd = Rd 1 ∪ Rd 2 , Wr = Wr 1 ∪ Wr 2 , and V = V 1 = V 2 ; m 1 m 2 m iff m 1 and m 2 are RW-disjoint, Rd = Rd 1 ∪ Rd 2 , Wr = Wr 1 ∪ Wr 2 , V 1 \ Wr = V 2 \ Wr, and V = (V 1 ∩ Wr 1 ) ∪ (V 2 ∩ Wr 2 ) ∪ (V 1 ∩ V 2 ).
For example, for m = Rd, Wr, V and m 2 = Rd 2 , Wr 2 , V 2 we have m m m 2 if and only if Wr 2 = ∅, V 2 = V, and Rd 2 ⊆ Rd \ Wr. In particular, ∅, ∅, ∅ m 1 m 2 if and only if m 1 = m 2 = ∅, ∅, ∅ . Contrarily to splitting, merging does not keep the valuation constant: it only keeps constant the non-modifiable part V \ Wr of the valuation V and puts the results of the allowed modifications of Wr together. These modifications cannot conflict because m 1 and m 2 are RW-disjoint. Figure 1 illustrates each of these two operations by an example. The checks that are performed in the merge operation are reminiscent of the self composition technique in the analysis of secure information flows [START_REF] Darvas | A theorem proving approach to analysis of secure information flow[END_REF][START_REF] Scheben | Information flow analysis[END_REF]. 7 The set Rd of readable variables of a model m determines which models cannot be distinguished from m:

m ∼ m iff Rd = Rd , Wr = Wr , V ∩ Rd = V ∩ Rd .
Hence m and m are indistinguishable if (1) they have the same readable and writable variables and (2) the valuations are identical as far as their readable parts are concerned. This relation will serve to interpret tests: the test ϕ? ? of a formula ϕ is conditioned by its truth in all read-indistinguishable models, i.e., in all models where the readable variables have the same truth value.

Language

Formulas and programs are defined by the following grammar, where p ranges over the set of propositional variables P:

ϕ ::= p | | ¬ϕ | ϕ ∨ ϕ | π ϕ, π ::= +p | -p | r+p | r-p | w+p | w-p | ϕ? | ϕ? ? | π; π | π ∪ π | π * | π||π.
The program +p makes p true and -p makes p false, where the executability of these two programs is conditioned by the writability of p. The program r+p makes p readable and r-p makes p unreadable; similarly, w+p makes p writable and w-p makes p nonwritable. We suppose that these four programs are always executable. The program ϕ? is the PDL test that ϕ, that we call exogenous; ϕ? ? is the endogenous test that ϕ: it is conditioned by the readability of the relevant variables of ϕ.

The formula π ϕ abbreviates ¬ π ¬ϕ. Given an integer n ≥ 0, the program π n is defined inductively by π 0 = ? and π n+1 = π; π n . Similarly, π ≤n is defined by π ≤0 = ? and π ≤n+1 = ? ∪ (π; π ≤n ). For a finite set of variables P = {p i } 1≤i≤n and associated programs {π i (p i )} 1≤i≤n , we use the notation ; p∈P π(p) to denote the sequence π 1 (p 1 );

• • • ; π n (p n ),
in some order. We will make use of this notation with care to guarantee that the ordering of the elements of P does not matter.

The set of propositional variables occurring in a formula ϕ is noted P ϕ and the set of those occurring in a program π is noted P π . For example, P p∨ +q ¬r = {p, q, r}.

Semantics

Let m = Rd, Wr, V be a model. Formulas are interpreted as sets of models:

m | = ; m | = p iff p ∈ V, for p ∈ P; m | = ¬ϕ iff m | = ϕ; m | = ϕ ∨ ψ iff m | = ϕ or m | = ψ; m | = π ϕ iff there is a model m such that m π m and m | = ϕ.
{p, q, r}, {p, q}, {p, q, r} {p, r}, {p}, {p, q, r} {q, r}, {q}, {p, q, r} {p, r}, {p}, {q, r} {q, r}, {q}, {p, r} {p, q, r}, {p, q}, {r} -p -q Fig. 2. Illustration of an execution of -p||-q at the model {p, q, r}, {p, q}, {p, q, r} .

Programs are interpreted as relations on the set of models:

m +p m iff Rd = Rd, Wr = Wr, V = V ∪ {p}, and p ∈ Wr m -p m iff Rd = Rd, Wr = Wr, V = V \ {p}, and p ∈ Wr m r+p m iff Rd = Rd ∪ {p}, Wr = Wr, and V = V m r-p m iff Rd = Rd \ {p}, Wr = Wr \ {p}, and V = V m w+p m iff Rd = Rd ∪ {p}, Wr = Wr ∪ {p}, and V = V m w-p m iff Rd = Rd, Wr = Wr \ {p}, and V = V m ϕ? m iff m = m and m | = ϕ m ϕ? ? m iff m = m and m | = ϕ for every m such that m ∼ m m π 1 ; π 2 m iff there is an m such that m π 1 m and m π 2 m m π 1 ∪ π 2 m iff m π 1 m or m π 2 m m π * m iff there is an n ≥ 0 such that m π n m m π 1 ||π 2 m iff there are m 1 , m 2 , m 1 , m 2 such that m m 1 m 2 , m 1 m 2 m , m 1 π 1 m 1 , Rd 1 = Rd 1 , Wr 1 = Wr 1 , V 1 \ Wr 1 = V 1 \ Wr 1 , m 2 π 2 m 2 , Rd 2 = Rd 2 , Wr 2 = Wr 2 , V 2 \ Wr 2 = V 2 \ Wr 2
In the interpretation of assignments of atomic formulas we require propositional variables to be modifiable, while readability and writability can be modified unconditionally. When a variable is made writable then it is made readable, too, in order to guarantee the inclusion constraint on models; similarly when a variable is made unreadable. The interpretation of parallel composition π 1 ||π 2 is such that both π 1 and π 2 only modify 'their' variables. More precisely, parallel composition π 1 ||π 2 of two programs π 1 and π 2 relates two models m and m when the following conditions are satisfied: (1) m can be split into m 1 and m 2 ;

(2) the execution of π 1 on m 1 may lead to m 1 and the execution of π 2 on m 2 may lead to m 2 ; (3) m 1 and m 2 can be merged into m . Moreover, (4) the modifications are legal: π 1 and π 2 neither change readability nor writability, and each of them only modifies variables that were allocated to it by the split. Figure 2 illustrates the interpretation of the parallel program -p||-q. Some more examples follow.

Example 1. Suppose m = Rd, Wr, V with Wr = Rd = V = {p, q, r}. Then m = Rd, Wr, V with V = {p, r} is the only model such that m +p||-q m . The next example illustrates the last condition in the interpretation of parallel composition.

Example 2. The programs +p||+p and +p||(w+p; -p; r-p) cannot be executed on the model m = {p}, {p}, {p} . For the second, suppose there are m 1 and m 2 such that m m 1 m 2 and suppose +p is executed on m 1 and w+p; -p; r-p on m 2 . For +p to be executable we must have p ∈ Wr 1 , and therefore p Wr 2 (and a fortiori p Rd 2 ) because of the RWdisjointness condition. Hence m 1 = {p}, {p}, {p} and m 2 = ∅, ∅, {p} . Then m 1 = m 1 is the only model such that m 1 +p m 1 ; and m 2 = ∅, ∅, ∅ is the only model such that m 2 w+p; -p; r-p m 2 . These two models cannot be merged because It is clear that parallel composition satisfies commutativity. It is less obvious that it is also associative. The proof is somewhat involved and can be found in the annex.

V 2 \ Wr 2 = ∅ fails to be equal to V 2 \ Wr 2 = {p}.
Let us finally illustrate the different semantics of the two test operators of our logic.

Example 3. Suppose m is such that p Rd and p ∈ V. Then the program p? is executable on m because p ∈ V. In contrast, there is no m such that m p? ? m , the reason being that there is always an m such that m ∼ m and p V , hence p? ? is inexecutable.

In practice, parallel programs should only contain endogenous tests in order to avoid that a subprogram accesses the truth value of a variable that is not among its readable variables. Actually we have kept PDL tests for technical reasons only: we could not formulate some of the reduction axioms without them.

Satisfiability and validity of formulas are defined in the expected way.

Example 4. The formulas ϕ → ? ?|| ? ? ϕ, +p||-p ⊥, +p||+p ⊥ and p? ?||+p ⊥ whose parallel programs were discussed in the introduction are all valid.

The formulas +p and -p both express that p is writable. Moreover, p? ? expresses that p is true and readable, and ¬p? ? expresses that p is false and readable; therefore p? ? ∨ ¬p? ? expresses that p is readable. This will be instrumental in our axiomatisation.

Finally, for any model m = Rd, Wr, V and P ⊆ P, we write m ∩ P for the model Rd ∩ P, Wr ∩ P, V ∩ P . This notation along with the following standard lemma will be used several times in the remainder of this work. Lemma 1. If there is P ⊆ P such that m 1 ∩ P = m 1 ∩ P, P ϕ ⊆ P and P π ⊆ P then

1. m 1 | = ϕ implies m 1 | = ϕ; and 2. m 1 π m 2 implies m 1 π m 2 , for m 2 such that m 2 ∩ P = m 2 ∩ P and m 2 ∩ (P \ P) = m 1 ∩ (P \ P).
Proof (sketch). The proof is by a straightforward simultaneous induction on the size of ϕ and π.

We axiomatise the validities of our logic by means of reduction axioms, as customary in dynamic epistemic logics [START_REF] Hans | Dynamic Epistemic Logic[END_REF]. These axioms transform every formula into a boolean combination of propositional variables and formulas of the form +p and p? ? ∨ ¬p? ? . The former expresses that p is writable: we abbreviate it by w p ; the latter expresses that p is readable: we abbreviate it by r p . Hence we have:

w p def = +p r p def = p? ? ∨ ¬p? ?
The reduction starts by eliminating all the program operators from formulas, where the elimination of parallel composition is done by sequentialising it while keeping track of the values of the atoms. After that step, the only remaining program operators either occur in formulas of the form r p or w p , or in modal operators of the form +p , -p , r+p , r-p , w+p , or w-p . All these modal operators can be distributed over the boolean operators, taking advantage of the fact that all of them are deterministic modal operators (validating the Alt 1 axiom π ϕ → π ϕ). Finally, sequences of such modalities facing a propositional variable can be transformed into boolean combinations of readability and writability statements r p and w p . The only logical link between these statements is that writability of p implies readability of p. This is captured by the axiom schema w p → r p .

The sequentialisation of parallel composition uses copies of variables, so we start by introducing that notion. We then define some programs and formulas that will allow us to formulate the reduction axioms more concisely.

Copies of Atomic Propositions

Our reduction axioms will introduce fresh copies of each propositional variable, one per occurrence of the parallel composition operator. The interpretation of parallel composition being based on separation, each concurrent program operates on its own model. The copies emulate the separation of models: each concurrent program is executed on a set of copies of propositional variables.

In order to keep things readable we neglect that the copies should be indexed by programs and denote the copies of the variable p by p k , where k is some integer. In principle we should introduce a bijection between the indexes k and the subprogram they are attached to; we however do not do so to avoid overly complicated notations.

Given a set of propositional variables P ⊆ P and an integer k ∈ {1, 2}, we define the set of copies P k = {p k : p ∈ P}. Similarly, we define copies of programs and formulas: the program π k and the formula ϕ k are obtained by replacing all their occurrences of propositional variables p by p k . For example, (+p; q? ?) k equals +p k ; q k ? ?.

The following lemma will be instrumental in the soundness proof.

Lemma 2. Let π be a program, let Rd, Wr, V be a model, and let k ∈ {1, 2}. Then

Rd, Wr, V π Rd , Wr , V iff Rd k , Wr k , V k π k Rd k , Wr k , V k .
split(P) = ; p∈P w+p 1 ; w+p 2 ; p?; +p 1 ; +p 2 ∪ ¬p?; -p 1 ; -p 2 ; r-p 1 ; r-p 2 ; ¬r p ? ∪ w p ?; (w+p 1 ∪ w+p 2 ) ∪ ¬w p ∧r p ?; r+p 1 ∪ r+p 2 ∪ (r+p 1 ; r+p 2 ) Proof (sketch). Just as for Lemma 1, the proof is by simultaneous induction on the form of programs and formulas, where the induction hypothesis for the latter is that

store(P) = ; p∈P ; k∈{1,2} w+p k R ; w+p k W ; (r p k ?; +p k R ) ∪ (¬r p k ?; -p k R ) ; (w p k ?; +p k W ) ∪ (¬w p k ?; -p k W ) check(P) = p∈P k∈{1,2} (p k R ↔ r p k ) ∧ (p k W ↔ w p k ) ∧ (¬p k W → (p ↔ p k )) merge(P) = ; p∈P ¬w p ? ∪ (w p 1 ∧ p 1 ) ∨ (w p 2 ∧ p 2 )?; +p ∪ (w p 1 ∧ ¬p 1 ) ∨ (w p 2 ∧ ¬p 2 )?; -p ; ; k∈{1,2} -p k R ; -p k W ; w+p k ; -p k ; r-p k R ; r-p k W ; r-p k flatten(π 1 , π 2 ) = split P π 1 ||π 2 ; store P π 1 ||π 2 ; π 1 1 ;
Rd, Wr, V | = ϕ if and only if Rd k , Wr k , V k | = ϕ k .
It relies on the fact that DL-PA || satisfies the substitution rule.

Moreover, in order to simulate the semantics of the parallel composition operator our reduction axioms associate to each copy p k two fresh variables p k R and p k W , denoting whether p k was respectively readable and writable just after the split. Given a set of propositional variables P, we define

St(P) = {p k R : k ∈ {1, 2}, p ∈ P} ∪ {p k W : k ∈ {1, 2}, p ∈ P}
as the set of all these fresh variables.

Useful Programs and formulas

Let P ⊆ P be some finite set of propositional variables. Table 1 lists programs and formulas that will be useful to concisely formulate the reduction axioms. Observe that the order of the variables in the sequential compositions ; p∈P (• • • ) occurring in the above programs does not matter. Observe also that the only endogenous tests on the right hand side occur in readability statements r p . (Remember that r p abbreviates p? ? ∨ ¬p? ? .)

The split(P) program simulates the split operation by (1) assigning the truth value of every p ∈ P to its copies p 1 and p 2 and (2) non-deterministically assigning two copies of each read and write variable in a way such that a counterpart of the RW-disjointness condition Wr 1 ∩ Rd 2 = Wr 2 ∩ Rd 1 = ∅ is guaranteed. Note that the assignments w+p k also make p k readable. The following lemma formally states the main property of split(P). It can easily be proved by following the previous observations. Lemma 3. For all P ⊆ P, and all models m, m 1 and m 2 such that m ∩ P = m, m m 1 m 2 if and only if m split(P) m

with Rd = Rd ∪ Rd 1 1 ∪ Rd 2 2 , Wr = Wr ∪ Wr 1 1 ∪ Wr 2 2 , and V = V ∪ V 1 1 ∪ V 2 2 .
The store(P) program stores the readability and writability states of the copies of the propositional variable into some fresh variables. These variables are then used only in check(P).

The formula check(P) compares the current state with the state just after the split. It is true if and only if (1) readability values are identical, (2) writability values are identical, and (3) truth values are identical for non-writable variables.

The merge(P) program simulates the merge operation by reinstating all those readand write-atoms that had been allocated to the first subprogram in the sequentialisation. The following lemma formally states the main property of merge(P). This lemma is weaker than Lemma 3 for split(P). The additional hypotheses are guaranteed to hold by the interplay of programs split(P) and store(P), and formula check(P).

Lemma 4. Let m, m 1 and m 2 be models, and P a set of propositional variables such that m ∩ P = m, m 1 and m 2 are RW-disjoint, Rd = Rd 1 ∪ Rd 2 , Wr = Wr 1 ∪ Wr 2 , and

V 1 \ Wr = V 2 \ Wr.
V = V ∪ V 1 1 ∪ V 2 2
where V is any subset of P ∪ St(P) such that V \ Wr = V \ Wr.

Proof (sketch). It suffices to prove that m merge(P) m if and only if

V = (V 1 ∩ Wr 1 ) ∪ (V 2 ∩ Wr 2 ) ∪ (V 1 ∩ V 2 ), which is straightforward.
Finally, the flatten(π 1 , π 2 ) program emulates the execution of the program π 1 ||π 2 as a sequential composition of the previous programs. Notice that there is no occurrence in flatten(π 1 , π 2 ) of the parallel composition operator, except possibly inside π 1 and π 2 . Lemma 6 below states that the emulation is faithful. We first need Lemma 5, which can be seen as an adaptation of Lemma 1 to flatten(P).

Lemma 5. For all models m and m , and all programs π 1 and π 2 ,

m flatten(π 1 , π 2 ) m iff (m ∩ P π 1 ||π 2 ) flatten(π 1 , π 2 ) (m ∩ P π 1 ||π 2 ).
Proof (sketch). It suffices to observe that all variables in P flatten(π 1 ,π 2 ) \P π 1 ||π 2 are (1) made writable and initialized by split or store, and (2) set to false and made unreadable by merge.

We can now prove our main lemma. Lemma 6. For all models m and m , and all programs π 1 and π 2 , m π 1 ||π 2 m if and only if m flatten(π 1 , π 2 ) m . Proof (sketch). Let P = P π 1 ||π 2 . By Lemmas 1 and 5, we can assume that m ∩ P = m and m ∩ P = m .

For the left-to-right direction, suppose there are models m 1 , m 2 , m 1 and m 2 such that

m m 1 m 2 , m 1 m 2 m , m 1 π 1 m 1 , m 2 π 2 m 2 , Rd 1 = Rd 1 , Wr 1 = Wr 1 , V 1 \ Wr 1 = V 1 \ Wr 1 , Rd 2 = Rd 2 , Wr 2 = Wr 2 , and V 2 \ Wr 2 = V 2 \ Wr 2 .
The following statements can be proved:

1. m split(P) m + 1 with Rd + 1 = Rd ∪ Rd 1 1 ∪ Rd 2 2 , Wr + 1 = Wr ∪ Wr 1 1 ∪ Wr 2 2
, and

V + 1 = V ∪ V 1 1 ∪ V 2 2 . The proof relies on Lemma 3. 2. m + 1 store(P) m + 2 with Rd + 2 = Rd + 1 ∪ St(P), Wr + 2 = Wr + 1 ∪ St(P), V + 2 = V + 1 ∪ V St , and V St = {p k R : p k ∈ Rd + 1 } ∪ {p k W : p k ∈ Wr + 1 }. Notice that V St = {p k R : p ∈ Rd k } ∪ {p k W : p ∈ Wr k }. 3. m + 2 π 1 1 m + 3 with Rd + 3 = Rd∪Rd 1 1 ∪Rd 2 2 ∪St(P), Wr + 3 = Wr∪Wr 1 1 ∪Wr 2 2 ∪St(P),
and

V + 3 = V ∪ V 1 1 ∪ V 2 2 ∪ V St .
The proof relies on Lemmas 1 and 2.

4. m + 3 π 2 2 m + 4 with Rd + 4 = Rd∪Rd 1 1 ∪Rd 2 2 ∪St(P), Wr + 4 = Wr∪Wr 1 1 ∪Wr 2 2 ∪St(P),
and

V + 4 = V ∪ V 1 1 ∪ V 2 2 ∪ V St . 5. m + 4 | = check(P). 6. m +
4 merge(P) m . The proof relies on Lemma 4. 7. m flatten(π 1 , π 2 ) m .

For the right-to-left direction, let us suppose that there are models m + 1 , m + 2 , m + 3 and m + 4 such that m split(P) m + 1 store(P) m + 2 π 1 m + 3 π 2 ; check(P)? m + 4 merge(P) m . The following statements can be proved:

1. m m 1 m 2 with Rd 1 = {p : p 1 ∈ Rd + 1 }, Wr 1 = {p : p 1 ∈ Wr + 1 }, V 1 = {p : p 1 ∈ V + 1 }, Rd 2 = {p : p 2 ∈ Rd + 1 }, Wr 2 = {p : p 2 ∈ Wr + 1 }, and V 2 = {p : p 2 ∈ V + 1 }. The proof relies on Lemma 3. 2. m 1 π 1 m 1 with Rd 1 = {p : p 1 ∈ Rd + 3 }, Wr 1 = {p : p 1 ∈ Wr + 3 }, and V 1 = {p : p 1 ∈ V + 3 }.
The proof relies on Lemmas 1 and 2. 3. m 2 π 2 m 2 with Rd 2 = {p :

p 2 ∈ Rd + 4 }, Wr 2 = {p : p 2 ∈ Wr + 4 }, and V 2 = {p : p 2 ∈ V + 4 }. 4. Rd 1 = Rd 1 , Wr 1 = Wr 1 , V 1 \ Wr 1 = V 1 \ Wr 1 , Rd 2 = Rd 2 , Wr 2 = Wr 2 , and V 2 \ Wr 2 = V 2 \ Wr 2 .
The proof relies on the fact that m + 4 | = check(P), and

V + 4 ∩ St(P) = {p k R : p ∈ Rd k } ∪ {p k W : p ∈ Wr k }. 5. m 1 m 2
m . The proof relies on Lemma 4. 6. m π 1 ||π 2 m .

Reduction Axioms for Program Operators

The reduction axioms for program operators are in Table 2. Those for sequential and non-deterministic composition and for exogenous tests (PDL tests) are as in PDL. The one for endogenous tests ϕ? ? checks whether ϕ remains true for any possible value of

ϕ? ψ ↔ ψ ∧ ϕ ϕ? ? ψ ↔ ψ ∧ ; p∈Pϕ r p ? ∪ ¬r p ?; (+p ∪ -p) ϕ π 1 ; π 2 ϕ ↔ π 1 π 2 ϕ π 1 ∪ π 2 ϕ ↔ π 1 ϕ ∨ π 2 ϕ π * ϕ ↔ π ≤2 |Pϕ | ϕ π 1 ||π 2 ϕ ↔ flatten(π 1 , π 2 ) ϕ
Table 2. Reduction axioms for program operators the non-readable variables of ϕ. That for the Kleene star is familiar from DL-PA. That for parallel composition π 1 ||π 2 executes π 1 and π 2 in sequence: it starts by splitting up readability and writability between the two programs, then executes π 1 , checks whether π 1 didn't change the readability and writability variables and whether all truth value changes it brought about are legal, and finally executes π 2 followed by the same checks for π 2 .

Observe that the validity of the reduction axiom for endogenous tests relies on the fact that the copies p 1 and p 2 that are introduced by the program split(P π 1 ||π 2 ) are fresh. The length of the right hand side can be shortened by restricting P π 1 ||π 2 to the propositional variables that are assigned by P π 1 ||π 2 , i.e., to elements p ∈ P such that +p or -p occurs in P π 1 ||π 2 .

The exhaustive application of the equivalences of Table 2 from the left to the right results in formulas whose program operators are either endogenous tests occurring in a readability statement r p = p? ? ∨ ¬p? ? , or assignments of the form r+p, r-p, w+p, w-p, +p, or -p.

Reduction Axioms for Boolean Operators

We now turn to modal operators π where π is an atomic assignment, i.e., π is of the form r+p, r-p, w+p, w-p, +p, or -p. They are deterministic and can therefore be distributed over the boolean operators. The corresponding reduction axioms are in Table 3.

In the first equivalence +p ↔ w p , the right hand side is nothing but an abbreviation of the left hand side. We nevertheless state it in order to highlight that the exhaustive application of these reduction axioms results in sequences of atomic assignments facing either w p or r q . These sequences are going to be reduced in the next step.

Reduction Axioms for Assignments

When atomic programs face propositional variables or readability and writability statements then the modal operator can be eliminated (sometimes introducing a writability statement w p ). The reduction axioms doing that are in Table 4.

As announced, the exhaustive application of the above axioms results in boolean combinations of propositional variables and readability and writability statements.

+p ↔ w p -p ↔ w p r+p ↔ r-p ↔ w+p ↔ w-p ↔ +p ¬ϕ ↔ w p ∧ ¬ +p ϕ -p ¬ϕ ↔ w p ∧ ¬ -p ϕ r+p ¬ϕ ↔ ¬ r+p ϕ r-p ¬ϕ ↔ ¬ r-p ϕ w+p ¬ϕ ↔ ¬ w+p ϕ w-p ¬ϕ ↔ ¬ w-p ϕ +p (ϕ ∨ ψ) ↔ +p ϕ ∨ +p ψ -p (ϕ ∨ ψ) ↔ -p ϕ ∨ -p ψ r+p (ϕ ∨ ψ) ↔ r+p ϕ ∨ r+p ψ r-p (ϕ ∨ ψ) ↔ r-p ϕ ∨ r-p ψ w+p (ϕ ∨ ψ) ↔ w+p ϕ ∨ w+p ψ w-p (ϕ ∨ ψ) ↔ w-p ϕ ∨ w-p ψ
Table 3. Reduction axioms for boolean operators

Soundness, Completeness, and Decidability

Let us call DL-PA || our extension of DL-PA with parallel composition. Its axiomatisation is made up of an axiomatisation of propositional logic; the equivalences of Sections 5.3, 5.4, and 5.5; the inclusion axiom schema w p → r p , which is an abbreviation of the formula +p → p? ? ∨ ¬p? ? ; the rule of equivalence for the modal operator "from ϕ ↔ ψ infer π ϕ ↔ π ψ".

Theorem 1. The axiomatisation of DL-PA || is sound: if ϕ is provable with the axiomatics of DL-PA || then it is DL-PA || valid.

Proof (sketch). We have to show that the inference rules preserve validity and the axioms are valid. For the reduction axiom for endogenous test, it suffices to observe that m +p ∪ -p m if and only if m ∼ m . The proof of validity of the reduction axiom for Kleene star can easily be adapted from the one in [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF]. The case of the reduction axiom for parallel composition is handled by Lemma 6. All other cases are straightforward.

Theorem 2. The axiomatisation of DL-PA || is complete: if ϕ is DL-PA || valid then it is provable in the axiomatics of DL-PA || .

Proof. The reduction axioms of Sections 5.3, 5.4, and 5.5 allow us to transform any formula into an equivalent boolean combination of propositional variables and readability and writability statements. (Their application requires the rule of replacement of equivalents, which is derivable because we have rules of equivalence for all the connectives of the language, in particular the above RE( π ).) Let ϕ be the resulting formula. Then ϕ has a DL-PA || model if and only if

ϕ ∧ p∈P w p → r p +p q ↔        w p if q = p w p ∧ q otherwise -p q ↔        ⊥ if q = p w p ∧ q otherwise r+p q ↔ q r-p q ↔ q w+p q ↔ q w-p q ↔ q +p r q ↔ w p ∧ r q -p r q ↔ w p ∧ r q r+p r q ↔        if q = p r q otherwise r-p r q ↔        ⊥ if q = p r q otherwise w+p r q ↔        if q = p r q otherwise w-p r q ↔ r q +p w q ↔ w p ∧ w q -p w q ↔ w p ∧ w q r+p w q ↔ w q r-p w q ↔        ⊥ if q = p w q otherwise w+p w q ↔        if q = p w q otherwise w-p w q ↔        ⊥ if q = p w q otherwise Table 4
. Reduction axioms for assignments has a model in propositional logic, where in propositional logic, r p and w p are considered to be arbitrary propositional variables; so there is a priori no connection between them nor with the propositional variable p.

Based on the reduction of DL-PA || formulas to boolean formulas (and the transformation of r p and w p from abbreviations into propositional variables), we may check the satisfiability of DL-PA || formulas by means of propositional logic SAT solvers. This is however suboptimal because the reduction may result in a formula that is superexponentially longer than the original formula. In the next section we explore another route.

Complexity via Translation into DL-PA

We establish PSPACE complexity of DL-PA || satisfiability and model checking by translating formulas and programs to Dynamic Logic of Propositional Assignments DL-PA. The language of the latter is the fragment of that of DL-PA || : it has neither endogenous tests, nor readability and writability assignments, nor parallel composition. Hence the language of DL-PA is built by the following grammar:

ϕ ::= p | | ¬ϕ | (ϕ ∨ ϕ) | π ϕ π ::= +p | -p | ϕ? | (π; π) | (π ∪ π) | π *
None of the operators of the language refers to the Rd-component or the Wr-component of models. The interpretation of DL-PA formulas and programs therefore only requires a valuation V. split(P) = ; p∈P p?; +p 1 ; +p 2 ∪ ¬p?; -p 1 ; -p 2 ; -w p 1 ; -r p 1 ; -w p 2 ; -r p 2 ; ¬r p ? ∪ w p ?; ((+r p 1 ; +w p 1 ) ∪ (+r p 2 ; +w p 2 )) ∪ ¬w p ∧r p ?; +r p 1 ∪ +r p 2 ∪ (+r p 1 ; +r p 2 ) store(P) = ; p∈P ; k∈{1,2} (r

p k ?; +p k R ) ∪ (¬r p k ?; -p k R ) ; (w p k ?; +p k W ) ∪ (¬w p k ?; -p k W ) check(P) = p∈P k∈{1,2} (p k R ↔ r p k ) ∧ (p k W ↔ w p k ) ∧ (¬p k W → (p ↔ p k )) merge(P) = ; p∈P ¬w p ? ∪ (w p 1 ∧ p 1 ) ∨ (w p 2 ∧ p 2 )?; +p ∪ (w p 1 ∧ ¬p 1 ) ∨ (w p 2 ∧ ¬p 2 )?; -p ; ; k∈{1,2} -p k R ; -p k W ; -p k ; -w p k ; -r p k flatten(π 1 , π 2 ) = split P π 1 ||π 2 ; store P π 1 ||π 2 ; π 1 1 ; π 2 2 ; check P π 1 ||π 2 ?; merge P π 1 ||π 2
Table 5. Adaptation of the programs and formulas of Table 1 to the translation into DL-PA.

Our translation from DL-PA || to DL-PA eliminates endogenous tests and parallel composition. This is done in a way that is similar to their reduction axioms of Table 2. It moreover transforms readability and writability statements into special propositional variables r p and w p , similar to the reduction axioms of Table 4.

To make this formal, let the set of atomic formulas be

X = P ∪ {w p : p ∈ P} ∪ {r p : p ∈ P}.
Given a set of propositional variables P ⊆ P, R P = {r p : p ∈ P} is the associated set of read-variables and W P = {w p : p ∈ P} is the associated set of write-variables. Hence X = P ∪ R P ∪ W P . As before, the set of propositional variables occurring in a formula ϕ is noted P ϕ and the set of those occurring in a program π is noted P π . This now includes the p's in r p and w p . For example, P p∧ +w q ¬r p = {p, q}.

We translate the DL-PA || programs r+p, r-p, w+p, and w-p into the DL-PA programs +r p , -r p , +w p and -w p . Moreover, we have to 'spell out' that -w p has side effect -r p and that +r p has side effect +w p . Hence the programs and formulas of Table 1 become the DL-PA programs and formulas listed in Table 5. Notice that readability and writability statements are no longer DL-PA || abbreviations, but are now DL-PA propositional variables.

Given a DL-PA || program or formula, its translation into DL-PA basically follows the reduction axiom for endogenous tests ? ? and parallel composition || of Table 2. We replace:

Lemma 7. For all DL-PA || programs π and formula ϕ, and all DL-PA || models m and m such that m ∩ P = m, m π m if and only if V + t(π) DL-PA V + , and

m | = ϕ if and only if V + | = DL-PA t(ϕ) where V + = V ∪ R Rd ∪ W Wr and V + = V ∪ R Rd ∪ W Wr .
Proof (sketch). The proof is by simultaneous induction on the size of π or ϕ. The cases for endogenous test and parallel composition are similar to those in the proof of Theorem 1. The other cases are straightforward.

The following theorem is a direct corollary of the previous lemma.

Theorem 3. A DL-PA || formula ϕ is DL-PA || -satisfiable if and only if the DL-PA formula t(ϕ) ∧ p∈P ϕ (w p → r p ) is DL-PA satisfiable.

We can now state our complexity results.

Lemma 8. The translation t is polynomial.

Proof. It can easily be checked that for all P, split(P), store(P), check(P) and merge(P) are linear in the size of P. Therefore, flatten(π 1 , π 2 ) is linear in the size of π 1 plus the size of π 2 . Similarly, ; p∈P ϕ r p ? ∪ ¬r p ?; (+p ∪ -p) ϕ? is linear in the size of ϕ. All other translation expressions are clearly linear too. Hence applying t from the root of the syntax tree to its leaves, t(ϕ) can be computed in time polynomial in the size of ϕ. We have added to Dynamic Logic of Propositional Assignments DL-PA a parallel composition operator in the spirit of separation logics. Our semantics augments DL-PA valuations by readability and writability information. We have provided an axiomatisation in terms of a complete set of reduction axioms. Our reduction to DL-PA ensures decidability. We have also proved PSPACE complexity via a polynomial translation to DL-PA.

We have adopted a stricter stance on race conditions than in [START_REF] Herzig | Dynamic logic of parallel propositional assignments and its applications to planning[END_REF] where e.g. the program +p||+p is executable. Let us briefly compare these two semantics. In our case, the intuition is that π 1 ||π 2 is executable if any interleaving of the components of π 1 and π 2 is executable, and that any of these interleavings leads to the same outcome. This is not guaranteed in the approach of [START_REF] Herzig | Dynamic logic of parallel propositional assignments and its applications to planning[END_REF], which is motivated by parallel planning. There, it is generally considered that two actions that are executed in parallel should not interfere [START_REF] Blum | Fast planning through planning graph analysis[END_REF]: they should not have conflicting effects and there should be no cross-interaction, where the second condition means that the effect of one action should not destroy the precondition of the other, and vice versa. For example, in a world of blocks the actions [START_REF] Herzig | Dynamic logic of parallel propositional assignments and its applications to planning[END_REF] makes that it is not enough to describe the parallel execution of actions π 1 , . . . , π n as a step of a parallel plan by π 1 || . . . ||π n . Instead, the absence of cross-interactions has to be checked 'by hand', namely by explicitly inserting a DL-PA test after each π i that the preconditions of the other actions are not violated: a step of a parallel plan is described by the program.

π 1 ; j 1 pre(π j )? || . . . || π n ; j n
pre(π j )? . This is not necessary in our semantics where the absence of cross interaction between actions that are performed in parallel is 'built-in'. Indeed, the parallel composition liftLeft(b)||liftRight(b) is not executable in DL-PA || : each subprogram requires writability of OnTable(b) to be executable. Our logic DL-PA || can therefore be expected to provide a more appropriate base for parallel planning.

The language of the extension of DL-PA of [HMV19] also contains an operator of inclusive nondeterministic composition, noted . While the standard inclusive nondeterministic composition π 1 ∪ π 2 of PDL and DL-PA || is read "do either π 1 or π 2 ", the program π 1 π 2 is read "do π 1 or π 2 or both". It has the same semantics as π 1 ∪ π 2 ∪ (π 1 ||π 2 ) and hence does not add expressivity. It is shown in [START_REF] Herzig | Dynamic logic of parallel propositional assignments and its applications to planning[END_REF] that it does not increase succinctness either. This is proved by a polynomial reduction that uses the same 'flattening' programs as the reduction of parallel composition. These programs are similar to our programs in Table 5, we therefore expect that inclusive nondeterministic composition does not increase the succinctness of the language of DL-PA || either.

The mathematical properties of DL-PA || compare favourably with the high complexity or even undecidability of the other extensions of dynamic logic by a separating parallel composition operator that were proposed in the literature [START_REF] Balbiani | Definability and computability for PRSPDL[END_REF][START_REF] Boudou | Complexity optimal decision procedure for a propositional dynamic logic with parallel composition[END_REF]. Just as ours, the latter line of work is in the spirit of separation logic, having splitting and merging operations that are defined on system states. The axiomatisation that was introduced and studied in [START_REF] Balbiani | Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization[END_REF] is restricted to the star-free fragment and the authors had to add propositional quantifiers in order to make parallel composition definable. This contrasts with the simplicity of our axiomatisation of DL-PA || that we obtained by adding reduction axioms to the axiomatisation of DL-PA. This can be related to the fact that propositional quantifiers can be expressed in DL-PA: ∃pϕ is equivalent to +p ∪ -p ϕ and ∀pϕ is equivalent to +p ∪ -p ϕ. Just as DL-PA can be viewed as an instance of PDL-the interpretation of atomic programs moves from PDL's abstract relation between states to concrete updates of valuations-, DL-PA || can be viewed as an instance of the logic of [START_REF] Mario | Propositional dynamic logic with storing, recovering and parallel composition[END_REF] where the interpretation of parallel composition no longer resorts to an abstract relation associating three states, but instead has concrete functions that split and merge valuations and that are constrained by readability and writability information.

Acknowledgements

The paper benefited from comments and remarks from the reviewers as well as from the attendees of DaLí 2019, in particular Alexandru Baltag, Raul Fervari, Rainer Hähnle and Dexter Kozen. We would like to particularly thank the three reviewers of JLAMP who provided detailed and well-informed reviews. We did our best take all these comments into account.

Andreas Herzig was partially supported by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No 952215. Nicolas Troquard was supported by UNIBZ CRC 2019 project IN2092, Computations in Resource Aware Systems (CompRAS).

A Appendix: Associativity of Parallel Composition

Alongside commutativity, associativity is a desirable property of a parallel composition operator. While the operator defined in Section 4 is clearly commutative, whether it is associative does not strike the eye. In fact, a detailed proof of it is rather cumbersome. We present it here. Left to right. Suppose lhs. We define:

1 , m * , m 2 , m 3 , m 1 , m 2 , m 3 , m * ': iff ∃a # , a 3 , a 1 , a 2 , a 1 , a 2 , a # ,
-a # = Rda # , Wra # , Va # = Rd 1 ∪ Rd 2 , Wr 1 ∪ Wr 2 , V , -a 1 = Rda 1 , Wra 1 , Va 1 = m 1 = Rd 1 , Wr 1 , V , -a 2 = Rda 2 , Wra 2 , Va 2 = m 2 = Rd 2 , Wr 2 , V , -a 3 = Rda 3 , Wra 3 , Va 3 = m 3 = Rd 3 , Wr 3 , V , -a # = Rda # , Wra # , Va # = Rd 1 ∪Rd 2 , Wr 1 ∪Wr 2 , (V 1 ∩Wr 1 )∪(V 2 ∩Wr 2 )∪(V 1 ∩V 2 ) , -a 1 = Rda 1 , Wra 1 , Va 1 ) = m 1 = (Rd 1 , Wr 1 , V 1 , -a 2 = Rda 2 , Wra 2 , Va 2 = m 2 = Rd 2 , Wr 2 , V 2 ,
a 3 = Rda 3 , Wra 3 , Va 3 = m 3 = Rd 3 , Wr 3 , V 3 .

We must show that these models satisfy all the properties from 19 through 36.

  Then

m 1 m 2 m

 2 if and only if m merge(P) m with Rd = Rd ∪ Rd 1 1 ∪ Rd 2 2 ∪ St(P), Wr = Wr ∪ Wr 1 1 ∪ Wr 2 2 ∪ St(P), and

Theorem 4 .

 4 DL-PA || model and satisfiability checking are both PSPACE complete. Proof. First, PSPACE membership of DL-PA || model and satisfiability checking follows from Lemmas 7 and 8. Second, since the language of DL-PA || contains that of DL-PA and since model and satisfiability checking are PSPACE hard for the latter [BHST14], it follows that DL-PA || model and satisfiability checking are PSPACE hard, too.

  liftLeft(b) = OnTable(b)?; -OnTable(b); +HoldsLeft(b), liftRight(b) = OnTable(b)?; -OnTable(b); +HoldsRight(b) of lifting block b with the left robot arm and with the right robot arm have crossinteraction because one of the effects of liftLeft(b) is ¬OnTable(b), which makes the precondition pre(liftRight(b)) = OnTable(b) of lifRight(b) false. The more liberal semantics of

Proposition 1 .

 1 m π 1 ||(π 2 ||π 3 ) m iff m (π 1 ||π 2 )||π 3 m .Proof. Figure3illustrates precisely what we are going to show. Suppose m = Rd, Wr, V and m = Rd , Wr , V .

  ∃m

1 Fig. 3 .Item 6 is m m 2 m 3 and m 2 m 3 m iff: 15 . 1 =Wra 1 ∩

 131511 Fig. 3. Illustration of associativity. Visual aid for the proof of Proposition 1.

  However, +p||(w+p; +p; r-p) is executable on m: we have m m ∅,∅,{p} and m +p {p}, {p}, {p} and ∅, ∅, {p} w+p; +p; r-p ∅, ∅, {p} and

	∅,∅,{p} {p},{p},{p}	{p}, {p}, {p} .

Table 1 .

 1 π 2 2 ; check P π 1 ||π 2 ?; merge P π 1 ||π 2 Useful programs and formulas, for all finite P ⊆ P and all programs π 1 and π 2 .

This restriction can be related to the fact that the formula e → e * e → e is unsatisfiable in Separation Logic[START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF].

As suggested by one of the reviewers of a previous version of the present paper[START_REF] Boudou | Resource separation in dynamic logic of propositional assignments[END_REF], this constraint may be relaxed and one may suppose that a program can modify a variable without being able to read its value. This would simplify the presentation of the logic; however, we believe that our inclusion constraint is natural in most applications.

The present paper is a more elaborate version of[START_REF] Boudou | Resource separation in dynamic logic of propositional assignments[END_REF]. It contains proofs of the results, more motivation and explanations, and furthermore proves that our operator of parallel composition is associative.

•

by definition, 3, and 8. We get

. With elementary set theory simplifications and claim 8, we obtain (

• By claim 1, Wr * = Wr * , which by 16 is Wr 2 ∪ Wr 3 which by 8 and 10 is Wr 2 ∪ Wr 3 . So Wr 2 ⊆ Wr * and Wr 3 ⊆ Wr * .

with the first two disjuncts included in

. Moreover, we have V 1 \ Wr 1 = V \ Wr 1 (by 3 and 12) and V 2 \Wr 2 = V\Wr 2 (by 8, 16, and 12). So we have

22 By definition, and 9. 23 By definition, 10, 16, and 12.

Right to left. Suppose rhs. We define: We must show that these models satisfy all the properties from 1 to 18. This is done routinely, analogously to the proof of the left-to-right direction above.