Relating some Logics for True Concurrency Tommaso Padoan Dipartimento di Matematica, Università di Padova, Padua, Italy padoan@math.unipd.it Abstract. We study some logics for true concurrency recently defined by several authors to characterise a number of known or meaningful behavioural equivalences, with special interest in history-preserving bisi- milarity. All the considered logics are event-based, naturally interpreted over event structures or any formalism which can be given a causal se- mantics, like Petri nets. Operators of incomparable expressiveness from different logics can be combined into a single logic, more powerful than the original ones. Since the event structure associated with a system is typically infinite (even if the system is finite state), already the known de- cidability results of model-checking in the original logics are non-trivial. Here we show, using a tableaux-based approach, that the model-checking problem for the new logic is still decidable over a class of event structures satisfying a suitable regularity condition, referred to as strong regularity. 1 Introduction In the analysis and verification of concurrent and distributed systems partial or- der semantics can be an appropriate choice since they provide a precise account of the possible steps in the evolution of the system and of their dependencies, like causality and concurrency. This approach is normally referred to as true concur- rency and it is opposed to the so-called interleaving approach, where concurrency of actions is reduced to the non-deterministic choice among their possible sequen- tializations. In the true concurrent world, a widely used foundational model is given by Winskel’s event structures [1]. They describe the behaviour of a system in terms of events in computations and two dependency relations: a partial order modelling causality and an additional relation modelling conflict. Several true concurrent behavioural equivalences have been defined which allow to abstract operational models taking into account different concurrency features of computations (see, e.g., [2]). On the logical side, various behavioural logics have been proposed capable of expressing causal properties of computa- tions (see, e.g., [3,4,5,6,7,8]) and some verification techniques have been con- sidered (see, e.g., [9,10,11]). Recently, event-based logics have been introduced [12,13], capable of uniformly characterising a relevant part of the true concur- rent spectrum. Some of these logics, together with those in [10,11], are among the most expressive true concurrent logics for which verification techniques have been proved to be decidable over suitable classes of true concurrent models. Interestingly, these logics provides the logical characterisation of a number of different meaningful behavioural equivalences, some of them incomparable. The logic referred to as Lhp , corresponding to a classical equivalence in the spectrum, i.e., history-preserving (hp-)bisimilarity [14,15,16], is a fragment of the more general logic in [12], representing instead hereditary history-preserving (hhp-)bisimilarity [4]. Lhp allows to predicate over executability of events in computations and their dependency relations (causality and concurrency). For- mulae include variables which can be bound to events in computations. The logic includes two modalities, diamond and box, which allows to explicitly as- sert the dependency relations between the computational steps. The formula h|x, y < a z|iϕ declares that is possible to execute an a-labelled event, which causally depends on the event bound to the variable x and is concurrent with the event bound to y, and, binding such an event to z, the formula ϕ holds. In general, x and y can be replaced by (possibly empty) tuples of variables. The presence of least and greatest fixpoint operators, in mu-calculus style, allows one to express properties of infinite computations. Recent results [17,18] proved that the model-checking problem for Lhp is decidable over a class of event structures satisfying a suitable regularity condition [19] referred to as strong regularity. In [10] two true concurrent logics have been introduced, namely separation fixpoint logic (SFL) and trace fixpoint logic (Lµ ). Both are based on a core logic with modalities that allow to express properties about causality and concurrency. The difference w.r.t. Lhp is that such modalities can only express causality and concurrency between consecutive steps. For example, the formula hainc ϕ decla- res the possibility to execute an a-labelled event, which is concurrent with (not caused by) the one executed before. The logics SFL and Lµ differ for the way in which they capture the duality between concurrency and conflict, relying on ope- rators on conflict-free sets of events. SFL uses a separating operator ∗ (dual ./) that behaves as a structural conjunction, allowing for local reasoning on conflict- free sets of executable events. The formula ϕ ∗ ψ requires the existence of two concurrent disjunct subsets of the executable events, such that the subformula ϕ (resp. ψ) holds on the first (resp. second) subset. Lµ instead has a second-order modality h⊗i (dual [⊗]) that recognises maximal concurrent subsets of the exe- cutable events. The formula h⊗iϕ requires that the subformula ϕ holds when restricting, locally, the computation of the system to a set of events that can actually execute all concurrently. The two logics have incomparable expressive power, as they characterise incomparable behavioural equivalences [10], in turn incomparable with hp-bisimilarity. Also in this case, model-checking has been proved decidable for both logics [10] over regular trace event structures [19]. In [13] the authors propose an extension of Hennessy-Milner logic called event identifier logic (EIL). The logic is again an event-based modal logic, but this time reverse as well as forward modalities are allowed. The two modalities, i.e., hx : aii (forward) and hhxi (backward), are not capable to assert explicitly the dependency relations between the computational steps, which are instead captured by a proper sequencing of such operators. The meaning of the two operator is quite clear: hx : aiiϕ declares the executability of an a-labelled event, 2 which is bound to x, and then ϕ holds; hhxiϕ requires that the event bound to x can be undone and then ϕ holds. There is also a third operator (x : a)ϕ which states that there is an a-labelled event executed in the past, such that, binding it to x, ϕ holds. The expressiveness of such logic is sufficient to provide a logical characterisation of hhp-bisimilarity, intuitively because the possibility of performing backward steps can be a mean of exploring alternative different futures. Moreover, a fragment of the logic, referred to as EILh , where forward modalities are no longer allowed after backward modalities, corresponds to hp- bisimilarity. In the spirit of the paper we will focus on EILh . The corresponding model-checking problem has not yet been investigated and it will be proved to be decidable here as a secondary result, for strongly regular event structures. In this work we study the mentioned logics, comparing their expressive power. The focus will be on the logic Lhp , used as a benchmark. We will study a logic, L∗⊗ hp , which combines the operators of Lhp , SFL, and Lµ . The logic EILh will be shown to be encodable in L∗⊗ ∗⊗ hp . Hence, Lhp is more powerful than all the considered logics (Lhp , SFL, Lµ , EILh ). Still, we conjecture that the logical equivalence for L∗⊗ ∗⊗ hp is coarser than hhp-bisimilarity and thus that Lhp is less expressive than the full logic EIL. We also show the decidability of model-checking in L∗⊗ hp , providing a local model-checking procedure for strongly regular event structures. The problem is not obvious since event structure models are infinite even for finite state systems and the possibility of expressing properties that depends on the past often leads to undecidability [20]. Indeed, even the results for the three original logics com- bined together in L∗⊗hp are non-trivial. The model-checking procedure is given in the form of a tableau system along the lines of [17] originally inspired by [21]. In order to check whether a system model satisfies a formula, a set of proof trees is constructed by applying suitable rules that reduce the satisfaction of a formula in a given state to the satisfaction of proper subformulae. 2 Event Structures Prime event structures [1] are a widely known model of concurrency. They des- cribe the behaviour of a system in terms of events and dependency relations between such events. Throughout the paper E is a fixed countable set of events, Λ a finite set of labels ranged over by a, b, . . . and λ : E → Λ a labelling function. Definition 1 (prime event structure). A (Λ-labelled) prime event structure ( pes) is a tuple E = hE, ≤, #i, where E ⊆ E is the set of events and ≤, # are binary relations on E, called causality and conflict respectively, such that: 1. ≤ is a partial order and dee = {e0 ∈ E | e0 ≤ e} is finite for all e ∈ E; 2. # is irreflexive, symmetric and hereditary with respect to ≤, i.e., for all e, e0 , e00 ∈ E, if e#e0 ≤ e00 then e#e00 . In the following, we will assume that the components of a pes E are named as in the definition above, possibly with subscripts. The concept of (concurrent) computation for event structures is captured by the notion of configuration. 3 a1 b1 b1 b1 a0 b0 a0 b0 a0 a1 b0 c0 (a) E1 (b) E2 (c) E3 Fig. 1. Some examples of finite (a)(b) and infinite (c) pess. Definition 2 (configuration). A configuration of a pes E is a finite set of events C ⊆ E consistent (i.e., ¬(e#e0 ) for all e, e0 ∈ C) and causally closed (i.e., dee ⊆ C for all e ∈ C). The set of configurations of E is denoted by C(E). The evolution of a system can be represented by a transition system where configurations are states. Definition 3 (transition system). Let E be a pes and let C ∈ C(E). Given e ∈ E r C such that C ∪ {e} ∈ C(E) and X, Y ⊆ C with X ⊆ dee, Y ∩ dee = ∅, we X,Y < e write C −−−−−→λ(e) C ∪ {e}. The set of enabled events at a configuration C is defined as en(C) = {e ∈ E r C | C ∪ {e} ∈ C(E)}. The pes is called k-bounded for some k ∈ N (or simply bounded) if |en(C)| ≤ k for all C ∈ C(E). Transitions are labelled by the executed event e, and they can report its label λ(e), a subset of causes X and a set of events Y ⊆ C concurrent with e. For any configuration it is possible to identify the substructure of the pes corresponding to the transition system rooted in such configuration. Definition 4 (residual). Let E be a pes. For a configuration C ∈ C(E), the residual of E after C, is defined as E[C] = {e | e ∈ E rC ∧ C ∪{e} consistent}. The residual of E can be seen as a pes, endowed with the restrictions of causality and conflict of E. Intuitively, it represents the pes that remains to be executed after the computation expressed by C. Some simple pess are depicted in Fig. 1. Graphically, curly lines represent immediate conflicts and the causal partial order proceeds upwards along the straight lines. Events are denoted by their labels, possibly with superscripts. For instance, in E3 , the event c0 , labelled by c, causes a0 and it is concurrent with b0 . Events a0 and b0 are in conflict. 3 True Concurrent Logics In this section we introduce the syntax and the semantics of the logic L∗⊗ hp which arises as a join of the logics for true concurrency Lhp [12], SFL and Lµ [10]. The logic has formulae that predicate over executability of events in computati- ons and their dependency relations (causality, concurrency), and provide second order power on conflict-free sets of events in two different flavours. 4 3.1 Syntax As already mentioned, formulae of Lhp include event variables, and so do for- mulae of L∗⊗hp . They belong to a fixed denumerable set Var , denoted by x, y, . . .. Tuples of variables like x1 , . . . , xn will be denoted by the corresponding boldface letter x and, abusing the notation, tuples will be often used as sets. The logic, in positive form, includes the diamond and box modalities from Lhp , the separating operators from SFL, and the second-order modalities from Lµ , described before. Fixpoint operators resort to propositional variables, expressed by abstract propositions to let them interact correctly with event variables. Abstract pro- positions belong to a fixed denumerable set X a , ranged over by X, Y, . . .. Each abstract proposition X has an arity ar (X) and represents a formula with ar (X) (unnamed) free event variables. For y such that |y| = ar (X), X(y) indicates the abstract proposition X whose free event variables are named y. We call X(y) a proposition and denote by X the set of all propositions. Definition 5 (syntax). The syntax of L∗⊗ hp over the sets of event variables Var , abstract propositions X a and labels Λ is defined as follows: ϕ ::= Z(y) | T | ϕ ∧ ϕ | h|x, y < a z|i ϕ | ϕ ∗ ϕ | h⊗i ϕ | (νZ(x).ϕ)(y) | F | ϕ ∨ ϕ | [[x, y < a z]] ϕ | ϕ ./ ϕ | [⊗] ϕ | (µZ(x).ϕ)(y) The free event variables of a formula ϕ are denoted fv (ϕ) and defined in the obvious way. Just note that the modalities act as binders for the variable representing the event executed, hence fv (h|x, y < a z|i ϕ) = fv ([[x, y < a z]] ϕ) = (fv (ϕ) r {z}) ∪ x ∪ y. The free propositions in ϕ, not bound by ν or µ, are denoted by fp(ϕ). Hereafter α ranges over {ν, µ}. For formulae (αZ(x).ϕ)(y) we require that fv (ϕ) = x. Intuitively, the fixpoint part αZ(x).ϕ defines a recursive formula Z(x) whose free variables are then instantiated with y. The formula (αZ(x).ϕ)(x) will be abbreviated as αZ(x).ϕ. When both fv (ϕ) and fp(ϕ) are empty we say that ϕ is closed. When x or y are empty they are omitted, e.g., we write h|a z|iϕ for h|∅, ∅ < a z|iϕ and αZ.ϕ for (αZ(∅).ϕ)(∅). For example, the formula ϕ1 = h|c x|i(h|x < a y|iT ∧ h|x < b z|iT) requires that, after the execution of a c-labelled event, one can choose between a causally dependent a-labelled event and a concurrent b-labelled event. This is satisfied by E3 in Fig. 1c. Instead, ϕ2 = h⊗i(F ./ F) requiring the existence of a maximal conflict-free set of enabled events which cannot be further separated, is false. Moving to infinite computations, consider ϕ3 = [[b x]] νZ(x).(h|c y|iT ∗ (h|x < b z|iT ∧ [[x < b w]]Z(w))), expressing that all non-empty causal chains of b- labelled events reach a state where the system can be separated into two parallel components, one continuing the chain of b events, while the other can execute a c-labelled event. Then, ϕ3 is satisfied by E3 . 3.2 Semantics Before defining the semantics of L∗⊗ hp , we need some notions, taken from [10], about conflict-free sets of enabled events, providing specific kinds of second- order quantification over them. The most general is the concept of support set. 5 Definition 6 (support set). Given a pes E and a configuration C ∈ C(E), a support set R for C is either the set of enabled events en(C) or a non-empty conflict-free set of enabled events, either way R ⊆ en(C). S We call R(C) the set of all support sets for a configuration C, and RE = C∈C(E) R(C) the set of all support sets for all possible configurations of a pes E. Support sets are used in the logic for local reasoning on executable events. According to the definition they can be conflict-free sets, where local reasoning becomes possible since they can be decomposed into smaller ones with the same property. Alternatively a support set can contain conflicts when it is the whole set of enabled events. In the latter case proper maximal conflict-free subsets can be isolated using so-called complete supsets. Definition 7 (complete supset). Let E be a pes and C ∈ C(E) be a configu- ration. Given a support set R ∈ R(C), a complete supset M of R, denoted by M v R, is a conflict-free support set M ∈ R(C) such that M ⊆ R and for all e ∈ R r M there exists e0 ∈ M s.t. e#e0 . We call M(R) the set of all complete supsets of a support set R. Intuitively, to decompose conflict-free sets into smaller ones means to separate different parallel components of systems, to allow local reasoning on them. This decomposition is captured by the notion of separation. Definition 8 (separation). Let E be a pes and C ∈ C(E) be a configuration. Given a support set R ∈ R(C), a separation (R1 , R2 ) of R is a pair of support sets R1 , R2 ∈ R(C) such that R1 ∩ R2 = ∅ and R1 ∪ R2 ∈ M(R). We call Sep(R) the set of all possible separations of a support set R. For instance, consider E3 in Fig. 1c. For the initial configuration ∅ we have three possible support sets R1 = {b0 , c0 }, R2 = {b0 }, and R3 = {c0 }. Among those only R1 admits a separation (just one), i.e., Sep(R1 ) = {(R2 , R3 )}. Since the logic L∗⊗ hp is interpreted over pess, the satisfaction of a formula ϕ is defined w.r.t. a configuration C, a support set R for C, and a (total) function η : Var → E, called an environment, that binds free variables in ϕ to events in C. Namely, if Env E denotes the set of environments, the se- mantics of a formula will be a set of triples in C(E) × RE × Env E . Given S ⊆ C(E) × RE × Env E and two tuples of variables x and y, with |x| = |y|, we define S[yx] = {(C, R, η 0 ) | ∃ (C, R, η) ∈ S ∧ η(x) = η 0 (y)}. The seman- tics of L∗⊗ hp also depends on a proposition environment π : X → 2 C(E)×RE ×Env E providing an interpretation for propositions. To ensure that the semantics of a formula depends only on the events associated with its free variables and is independent on the naming of the variables, it is required that for all tuples of variables x, y with |x| = |y| = ar (X) it holds π(X(y)) = π(X(x))[yx]. We denote by PEnv E the set of proposition environments, ranged over by π. With η[x 7→ e] we indicate the updated environment obtained from η where x is mapped to the event e. Similarly, for S ⊆ C(E)×RE ×Env E , we write π[Z(x) 7→ S] for the corresponding update of π. For a triple (C, R, η) ∈ C(E) × RE × Env E and variables x, y, z, we define the (x, y < az)-successors of (C, R, η), as 6 η(x),η(y) < e SuccEx,y