=Paper=
{{Paper
|id=Vol-2243/paper24
|storemode=property
|title=Relating some Logics for True Concurrency
|pdfUrl=https://ceur-ws.org/Vol-2243/paper24.pdf
|volume=Vol-2243
|authors=Tommaso Padoan
|dblpUrl=https://dblp.org/rec/conf/ictcs/Padoan18
}}
==Relating some Logics for True Concurrency==
https://ceur-ws.org/Vol-2243/paper24.pdf
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[y x] = {(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))[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, η) ∈ 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