We study some logics for true concurrency recently de ned by several authors to characterise a number of known or meaningful behavioural equivalences, with special interest in history-preserving bisimilarity. All the considered logics are event-based, naturally interpreted over event structures or any formalism which can be given a causal semantics, like Petri nets. Operators of incomparable expressiveness from di erent logics can be combined into a single logic, more powerful than the original ones. Since the event structure associated with a system is typically in nite (even if the system is nite state), already the known decidability 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.
Introduction
In the analysis and veri cation of concurrent and distributed systems partial
order 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
concurrency and it is opposed to the so-called interleaving approach, where concurrency
of actions is reduced to the non-deterministic choice among their possible
sequentializations. In the true concurrent world, a widely used foundational model is
given by Winskel's event structures [
Several true concurrent behavioural equivalences have been de ned which allow to abstract operational models taking into account di erent concurrency features of computations (see, e.g., [2]). On the logical side, various behavioural logics have been proposed capable of expressing causal properties of computations (see, e.g., [3,4,5,6,7,8]) and some veri cation techniques have been considered (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 concurrent spectrum. Some of these logics, together with those in [10,11], are among the most expressive true concurrent logics for which veri cation 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 di erent 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). Formulae include variables which can be bound to events in computations. The logic includes two modalities, diamond and box, which allows to explicitly assert the dependency relations between the computational steps. The formula hjx; y < a zji' 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 xpoint operators, in mu-calculus style, allows one to express properties of in nite 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 xpoint logic (SFL) and trace xpoint logic (L ). Both are based on a core logic with modalities that allow to express properties about causality and concurrency. The di erence w.r.t. Lhp is that such modalities can only express causality and concurrency between consecutive steps. For example, the formula hainc ' declares the possibility to execute an a-labelled event, which is concurrent with (not caused by) the one executed before. The logics SFL and L di er for the way in which they capture the duality between concurrency and con ict, relying on operators on con ict-free sets of events. SFL uses a separating operator (dual ./) that behaves as a structural conjunction, allowing for local reasoning on con ictfree 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 rst (resp. second) subset. L instead has a second-order modality h i (dual [ ]) that recognises maximal concurrent subsets of the executable 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 identi er 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, 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 su cient to provide a logical characterisation of hhp-bisimilarity, intuitively because the possibility of performing backward steps can be a mean of exploring alternative di erent futures. Moreover, a fragment of the logic, referred to as EILh, where forward modalities are no longer allowed after backward modalities, corresponds to hpbisimilarity. 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, Lhp , which combines the operators of Lhp, SFL, and L . The logic EILh will be shown to be encodable in Lhp . Hence, Lhp is more powerful than all the considered logics (Lhp, SFL, L , EILh). Still, we conjecture that the logical equivalence for Lhp 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 Lhp , providing a local model-checking procedure for strongly regular event structures. The problem is not obvious since event structure models are in nite even for nite 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 combined together in Lhp 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 satis es 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 [
( pes) is a tuple E = hE; ; #i, where E E is the set of events and , # are binary relations on E, called causality and con ict respectively, such that: 1. is a partial order and dee = fe0 2 E j e0 eg is nite for all e 2 E; 2. # is irre exive, symmetric and hereditary with respect to , i.e., for all e; e0; e00 2 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 de nition above, possibly with subscripts. The concept of (concurrent) computation for event structures is captured by the notion of con guration.
events C E consistent (i.e., :(e#e0) for all e; e0 2 C) and causally closed (i.e., dee C for all e 2 C). The set of con gurations of E is denoted by C(E ).
The evolution of a system can be represented by a transition system where con gurations are states.
e 2 E r C such that C [ feg 2 C(E ) and X; Y C with X dee, Y \ dee = ;, we write C X;Y < !e (e) C [ feg. The set of enabled events at a con guration C is de ned as en(C) = fe 2 E r C j C [ feg 2 C(E )g. The pes is called k-bounded for some k 2 N (or simply bounded) if jen(C)j k for all C 2 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 con guration it is possible to identify the substructure of the pes corresponding to the transition system rooted in such con guration. De nition 4 (residual). Let E be a pes. For a con guration C 2 C(E ), the residual of E after C, is de ned as E [C] = fe j e 2 E r C ^ C [ feg consistentg.
The residual of E can be seen as a pes, endowed with the restrictions of causality and con ict 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 con icts 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 con ict. 3
True Concurrent Logics In this section we introduce the syntax and the semantics of the logic Lhp 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 computations and their dependency relations (causality, concurrency), and provide second order power on con ict-free sets of events in two di erent avours. 3.1
As already mentioned, formulae of Lhp include event variables, and so do formulae of Lhp . They belong to a xed 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 propositions belong to a xed 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 jyj = 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.
De nition 5 (syntax). The syntax of Lhp over the sets of event variables Var , abstract propositions X a and labels is de ned as follows: ' ::= Z(y) j T j ' ^ ' j hjx; y < a zji ' j ' ' j h i ' j ( Z(x):')(y) j F j ' _ ' j [[x; y < a z]] ' j ' ./ ' j [ ] ' j ( Z(x):')(y) The free event variables of a formula ' are denoted fv (') and de ned in the obvious way. Just note that the modalities act as binders for the variable representing the event executed, hence fv (hjx; y < a zji ') = fv ([[x; y < a z]] ') = (fv (') r fzg) [ x [ y. The free propositions in ', not bound by or , are denoted by fp('). Hereafter ranges over f ; g. For formulae ( Z(x):')(y) we require that fv (') = x. Intuitively, the xpoint part Z(x):' de nes 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 hja zji' for hj;; ; < a zji' and Z:' for ( Z(;):')(;).
For example, the formula '1 = hjc xji(hjx < a yjiT ^ hjx < b zjiT) 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 satis ed by E3 in Fig. 1c. Instead, '2 = h i(F ./ F) requiring the existence of a maximal con ict-free set of enabled events which cannot be further separated, is false. Moving to in nite computations, consider '3 = [[b x]] Z(x):(hjc yjiT (hjx < b zjiT ^ [[x < b w]]Z(w))), expressing that all non-empty causal chains of blabelled 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 satis ed by E3. 3.2
Before de ning the semantics of Lhp , we need some notions, taken from [10], about con ict-free sets of enabled events, providing speci c kinds of secondorder quanti cation over them. The most general is the concept of support set. De nition 6 (support set). Given a pes E and a con guration C 2 C(E ), a support set R for C is either the set of enabled events en(C) or a non-empty con ict-free set of enabled events, either way R en(C). We call R(C) the set of all support sets for a con guration C, and RE = SC2C(E) R(C) the set of all support sets for all possible con gurations of a pes E .
Support sets are used in the logic for local reasoning on executable events. According to the de nition they can be con ict-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 con icts when it is the whole set of enabled events. In the latter case proper maximal con ict-free subsets can be isolated using so-called complete supsets.
ration. Given a support set R 2 R(C), a complete supset M of R, denoted by M v R, is a con ict-free support set M 2 R(C) such that M R and for all e 2 R r M there exists e0 2 M s.t. e#e0. We call M(R) the set of all complete supsets of a support set R.
Intuitively, to decompose con ict-free sets into smaller ones means to separate di erent parallel components of systems, to allow local reasoning on them. This decomposition is captured by the notion of separation.
De nition 8 (separation). Let E be a pes and C 2 C(E ) be a con guration. Given a support set R 2 R(C), a separation (R1; R2) of R is a pair of support sets R1; R2 2 R(C) such that R1 \ R2 = ; and R1 [ R2 2 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 con guration ; we have three possible support sets R1 = fb0; c0g, R2 = fb0g, and R3 = fc0g. Among those only R1 admits a separation (just one), i.e., Sep(R1) = f(R2; R3)g.
Since the logic Lhp is interpreted over pess, the satisfaction of a formula ' is de ned w.r.t. a con guration 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 semantics 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 jxj = jyj, we de ne S[y x] = f(C; R; 0) j 9 (C; R; ) 2 S ^ (x) = 0(y)g. The semantics of Lhp also depends on a proposition environment : X ! 2C(E) RE EnvE 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 jxj = jyj = ar (X) it holds (X(y)) = (X(x))[y x]. 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; ) 2 C(E ) RE Env E and variables x, y, z, we de ne the (x; y < az)-successors of (C; R; ), as Succx;y<az(C; R; ) = f(C0; en(C0); [z 7! e]) j e 2 R ^ C
E (x); (y) < e !a C0g.
De nition 9 (semantics). Let E be a pes. The denotation of a formula ' in Lhp is given by the function fj jgE : Lhp ! PEnv E ! 2C(E) RE EnvE de ned inductively as follows, where we write fj'jgE instead of fj'jgE ( ): fjTjgE = C(E)
RE
Env E fjFjgE = ; fjZ(y)jgE = (Z(y)) fj'1 ^ '2jgE = fj'1jgE \ fj'2jgE fj'1 _ '2jgE = fj'1jgE [ fj'2jgE fjhjx; y < a zji 'jgE = f(C; R; ) j Succx;y<az(C; R; ) \ fj'jgE 6= ;g fj[[x; y < a z]] 'jgE = f(C; R; ) j SuccEEx;y<az(C; R; ) fj'jgE g fj'1 '2jgE = f(C; R; ) j 9 (R1; R2) 2 Sep(R): V i2f1;2g fj'1 ./ '2jgE = f(C; R; ) j 8 (R1; R2) 2 Sep(R): W i2f1;2g fjh i 'jgE = f(C; R; ) j 9 M 2 M(R): (C; M; ) 2 fj'jgE g fj[ ] 'jgE = f(C; R; ) j 8 M 2 M(R): (C; M; ) 2 fj'jgE g (C; Ri; ) 2 fj'ijgE g (C; Ri; ) 2 fj'ijgE g fj( Z(x):')(y)jgE = (f';Z(x); )[y x] fj( Z(x):')(y)jgE = (f';Z(x); )[y x] where f';Z(x); : 2C(E) RE EnvE ! 2C(E) RE EnvE is the semantic function of ', Z(x), de ned by f';Z(x); (S) = fj'jgE[Z(x)7!S] and (f';Z(x); ) (resp.
(f';Z(x); )) denotes the corresponding greatest (resp. least) xpoint. We say that a pes E satis es ' if (;; en(;); ) 2 fj'jgE for all environments and .
The semantics of boolean operators is as usual. The formula hjx; y < a zji' holds in (C; R; ) when an a-labelled event e included in the set R (hence enabled in con guration C), that causally depends on (at least) the events bound to the variables in x and is concurrent with (at least) those bound to the variables in y, can be executed producing a new con guration C0 = C [ feg which, together with the events enabled in C0 and the environment 0 = [z 7! e], satis es the formula '. Dually, [[x; y < a z]]' holds when all a-labelled events in R, caused by x and concurrent with y bring to a con guration where ' is satis ed.
The formula '1 '2 is satis ed by (C; R; ) if there is a separation (R1; R2) of R such that each formula 'i holds in the corresponding Ri with the same con guration C and environment . Dually, '1 ./ '2 holds if in all the possible separations of R at least one component satis es the corresponding subformula.
The operator h i' is satis ed by (C; R; ) simply when the formula ' holds after restricting R to one of its complete supsets M . Similarly, the dual [ ]' requires that ' holds for all possible restrictions of R to complete supsets.
The xpoints corresponding to the formulae ( Z(x):')(y) are guaranteed to exist by Knaster-Tarski theorem, since the set 2C(E) RE EnvE ordered by subset inclusion is a complete lattice and the functions f';Z(x); are monotonic.
Hereafter we assume that in every formula di erent bound propositions have di erent names, so that we can refer to the xpoint subformula quantifying an abstract proposition. This requirement can always be ful lled by alpha-renaming.
Fragments of Lhp can be easily identi ed which correspond to the three original logics. Hence Lhp is indeed more powerful than all of them. 3.3
Here we prove that EILh [13] can be encoded in Lhp which is thus more expressive than such logic. More precisely, we show that EILh can be encoded in Lhp. This also implies that the model-checking in EILh is decidable by reduction to Lhp.
The encoding uses functions to remember the variables bound by forward modalities, their causal dependency with past variables, and their labels. Function : Var ! 2Var associates variables with the set of past variables causing them. Function l : Var ! associates variables with their labels. and l are actually partial functions de ned only on a subset of variables, denoted by their dominion. Then, the procedure is as follows: [T]( ; l) = T [F]( ; l) = F [hx : aii ']( ; l) = where V c = dom( ) r V , for a set of variables V , and '[z x] is the formula ' where all free occurrences of the variable x are substituted with variable z.
We assume that in every formula of EILh di erent bound variables have di erent names. This requirement can always be ful lled by alpha-renaming.
The procedure allows for the encoding of any closed formula ' of EILh by computing ['](;; ;). The correctness of the encoding can be proved by induction on the formula ', observing that the necessary properties are preserved at each step and they vacuously hold when = l = ;. Thus, we obtain the following. Proposition 1 (encoding EILh). Let E be a pes and let ' be a closed formula of EILh, E satis es ' i it satis es ['](;; ;). 4
Model Checking Lhp In this section we provide a model-checking procedure for Lhp , showing that it is sound and complete over a class of pes satisfying a suitable regularity condition.
In many model-checking algorithms (e.g., [22,21]) the niteness of the model is an essential ingredient that concurs to termination or correctness of the method. We will work on a subclass of pess identi ed by nitarity requirements on the possible substructures. Given a con guration C 2 C(E ) and a subset X C, we denote by E [C] [ X the pes obtained from the residual E [C] by adding the events in X with the causal dependencies they had in the original pes E .
C; R; ;
C; R; ; j=E '1 _ '2 i 2 f1; 2g j=E 'i ( ) C; R; ; j=E hjx; y < a zji '
C0; en(C0); [z 7! e]; j=E ' e 2 R and C (x); (y) < !ea C0 ( )
C; R; ; j=E [[x; y < a z]] ' C1; en(C1); 1; j=E ' : : : Cn; en(Cn); n; j=E ' where f(C1; en(C1); 1); : : : ; (Cn; en(Cn); n)g = SuccEx;y<az(C; R; ) ( )
C; R0; ; (./)
C; R; ; j=E ' j=E ' C; R00; ; j=E
(R0; R00) 2 Sep(R) C; R1p1 ; ;
C; R; ; j=E '1 ./ '2 j=E 'p1 : : : C; Rnpn ; ; j=E 'pn where f(R11; R12); : : : ; (Rn1; Rn2)g = Sep(R) and 8 i 2 [1; n]: pi 2 f1; 2g (h i)
C; R; ;
C; M; ; j=E h i ' j=E '
M 2 M(R) ([ ])
C; M1; ;
C; R; ; j=E [ ] ' j=E ' : : : C; Mn; ; j=E '
where fM1; : : : ; Mng = M(R) (Int) C; R; ; j=E ( Z(x):')(y)
C; R; ; 0 j=E Z(y) (Unf )
C; R; ; j=E Z(y) C; R; [x 7! (y)]; j=E ' 0 = [Z(x) 7!
Z(x):'] : and (Z(x)) = Z(x):'
it is bounded and for each k 2 N the set fE[C] [ fe1; : : : ; ekg j C 2 C(E) ^ e1; : : : ; ek 2 Cg is nite up to isomorphism of pess.
Strong regularity [17] is obtained from the notion of regularity in [19], by replacing residuals with residuals extended with a bounded number of events from the past. Intuitively, this is important since we are interested in history dependent properties. Clearly, each strongly regular pes is regular. In [18] it is shown that the pess associated with nite safe Petri nets are strongly regular.
The model-checking procedure is given in the form of a tableau system. It follows closely the lines of [17]. The tableau rules are reported in Table 1.
Sequents contain a context C; R; ; and a formula ' of Lhp which they assert to be satis ed by such context. C; R; are the usual elements from the semantics, while is a nite set of de nitions Z(x) = . In such case (Z(x)) denotes the formula . In a tableau built starting from a closed formula, associates a free proposition with the xpoint subformula where it is quanti ed. Intuitively, is like a proposition environment at syntax level. [Z(x) 7! ] denotes the updated de nition set obtained from by removing the previous de nition of Z, if any, and adding Z(x) = . is updated every time a xpoint formula is encountered, i.e., when rule (Int) is applied. In such case we say that the sequent introduces the corresponding proposition. Then, given a sequent, if Z(x) = is in , we denote by "(Z) the closest ancestor introducing Z.
We next clarify when a fully constructed tableau is considered successful.
where no more rules can be applied and every leaf is labelled by a sequent C; R; ; j=E ' such that one of the following holds: 1. ' = T 3. ' = 1 ./ 2 2. ' = [[x; y < a z]] 4. ' = Z(y) and (Z(x)) = Z(x): .
Note the absence of the case ' = [ ] because every support set R has at least one complete supset, i.e., M(R) 6= ;, hence the sequent could not be a leaf.
For checking whether a closed formula ' of Lhp is satis ed by a strongly regular pes E , one must build a tableau for the formula, i.e., a successful tableau rooted in the sequent ;; en(;); ; ; j=E ' (where is irrelevant since ' is closed). Theorem 1 (tableau system). Given a strongly regular pes E and a closed formula ' of Lhp , E satis es ' i ' admits a successful tableau for E .
Here we just sketch the main ingredients of the proof.
Tableaux are guaranteed to be nitely branching by nitarity of the formulae of the logic and the fact that strongly regular pess are bounded. However, tableaux could contain in nite paths because of repeated applications of the rule (Unf ), which unfolds propositions according to their de nition in . To avoid this, rule (Unf ) has a side condition involving an unspeci ed part , the so-called stop condition. It is intended to prevent the unfolding of a proposition when a context is reached that is equivalent, in a suitable sense to be de ned, to a context occurring in an ancestor sharing the same formula.
Intuitively, two contexts are equivalent for a formula if they share the satisfaction of the formula. Recall that properties of Lhp predicate over executability of events and their dependency relations while imposing some second-order constraints. The notion below captures exactly the properties that two contexts must meet to be deemed equivalent.
pes E , and two contexts C; R; ; and C0; R0; 0; 0 for a formula ', we say that they have isomorphic pointed supported residuals, written E [hC; R; jfv(')i] E [hC0; R0; 0jfv(')i], if there is an isomorphism of pess : E [C] ! E [C0] such that R0 = (R) and for all x 2 fv ('), e 2 E [C] we have (x) e i 0(x) (e).
It can be shown that two contexts with isomorphic pointed supported residuals for a formula either both satisfy it or none of them does. These results motivate the de nition of the stop condition.
Table 1 is as follows: there is an ancestor of the premise C; R; ; j=E Z(z) labelled C0; R0; 0; 0 j=E Z(y), such that "(Z) = 0"(Z) and E [hC; R; [x 7! (z)]jxi] E [hC0; R0; 0[x 7! 0(y)]jxi].
Informally, the stop condition holds when in a previous step of the construction of the tableau an instance of the same abstract proposition has been unfolded in an equivalent context, without being reintroduced. Then we can safely avoid to continue along this path because it would not add new information.
Now, a crucial observation is that, for strongly regular pess, the number of pointed supported residuals is nite up to isomorphism. From this and the previous facts it can be shown that all tableaux are nite and the number of possible tableaux for a sequent is also nite. Moreover, we can prove the correctness of the tableau system, relying on the reduction of the semantics of xpoint formulae to that of nite approximants and the backwards soundness of the rules. 5
Conclusions We studied some expressive logics for true concurrency, proposed by several authors in the literature and we showed how they can be combined into a single, more powerful logic Lhp . We showed also that EILh can be encoded in Lhp. Except for xpoint operators, we conjecture that also Lhp is encodable in EILh.
We proved the decidability of the model-checking problem for Lhp over strongly regular pess, providing a decision procedure in the form of a tableau system, which is correct and terminating. A concrete procedure requires the effectiveness of the transition relation over con gurations and of the equivalence of pointed supported residuals, that we have if we focus on regular trace pess, which are known to be included in (but possibly equal to) strongly regular pess.
In [11] another logic for concurrency, called monadic trace logic (Mtl), is proposed as a fragment of monadic second-order logic (Msol), where second-order quanti cation is allowed only on con ict-free sets of events. Still, the possibility of directly observing con icts and thus of distinguishing behaviourally equivalent pess (e.g., those consisting of a single or two con icting copies of an event), and the presence in Lhp of propositions which are non-monadic with respect to event variables, make these logics not immediate to compare. Nevertheless, some investigations point us to conjecture that they are in fact incomparable.
The intimate relation between Lhp and Lhp, one of the logics combined into Lhp , suggests that the model-checking procedure based on automata proposed for Lhp in [18] could be adapted for the model-checking in Lhp . Furthermore, also the tool implementing such technique, presented in the same work, could be adjusted to allow the veri cation of Lhp properties. However, some considerations on the equivalence of pointed supported residuals lead us to think that a naive implementation would have a too high complexity to be useful in practice. Acknowledgements. I am grateful to Paolo Baldan for insightful discussions and inspiring suggestions and to the anonymous reviewers for their comments.