=Paper=
{{Paper
|id=Vol-1847/paper06
|storemode=property
|title=On Synthesising Step Alphabets for Acyclic Invariant Structures
|pdfUrl=https://ceur-ws.org/Vol-1847/paper06.pdf
|volume=Vol-1847
|authors=Ryszard Janicki,Jetty Kleijn,Maciej Koutny,Łukasz Mikulski
|dblpUrl=https://dblp.org/rec/conf/apn/JanickiKKM17
}}
==On Synthesising Step Alphabets for Acyclic Invariant Structures==
https://ceur-ws.org/Vol-1847/paper06.pdf
On Synthesising Step Alphabets
for Acyclic Invariant Structures
Ryszard Janicki1 , Jetty Kleijn2 , Maciej Koutny3 , and Łukasz Mikulski4
1
Department of Computing and Software, McMaster University
Hamilton, ON, L8S 4K1, Canada
janicki@mcmaster.ca
2
LIACS, Leiden University, P.O.Box 9512
NL-2300 RA Leiden, The Netherlands
h.c.m.kleijn@liacs.leidenuniv.nll
3
School of Computing Science, Newcastle University
Newcastle upon Tyne NE1 7RU, United Kingdom
maciej.koutny@ncl.ac.uk
4
Faculty of Mathematics and Computer Science, Nicolaus Copernicus University
Toruń, Chopina 12/18, Poland
lukasz.mikulski@mat.umk.pl
Abstract. A step alphabet describes dependencies between the actions
of a concurrent system in the form of two relations expressing potential
simultaneity and sequentialisability. These form the basis for the identi-
fication of step sequences as observations of the same run of the system.
The resulting equivalence classes – step traces – can be represented by
(labelled) invariant structures with two relations, viz. mutex and weak
causality.
In this paper, we address the following synthesis problem for acyclic
invariant structures which are structures corresponding to step traces
with sequential realisations: given an acyclic invariant structure that can
represent a step trace, construct a suitable step alphabet, i.e., provide
suitable simultaneity and sequentialisability relations for its actions. The
main result is that the set of all suitable alphabets forms a complete
lattice with the ordering derived from the relative ‘strength’ of the de-
pendencies between individual actions.
Keywords: step alphabet, step trace, invariant structure, simultaneity,
sequentialisability, mutual exclusion, weak causality, acyclicity, synthesis
1 Introduction
An observational semantics of concurrent systems is usually defined either in
terms of sequences (total orders), or step sequences, (stratified orders). When
concurrent histories are fully described by causality relations, i.e., by a partial
order, Mazurkiewicz traces [14, 15] allow a representation of the entire partial
order by a single sequence (plus independency relation), which provides a simple
76
and elegant connection between observational and process semantics (i.e., the
semantics in terms of concurrent histories) of concurrent systems.
A trace is an equivalence class of sequences comprising all (sequential) ob-
servations of a single concurrent run. The dependencies between the events of a
trace are invariant among (common to) all elements of the trace. They define an
acyclic dependence graph which — through its transitive closure — determines
the underlying causality structure of the trace as a (labelled) partial order [18].
Then each trace is represented by a labelled partial order; see, e.g., [3, 6].
However, the concurrency paradigm of Mazurkiewicz traces with the corre-
sponding partial order interpretation of concurrency is rather restricted, as it
cannot, for example, handle the ‘no later than relationship’ [12].
In [9], a generalisation of the theory of Mazurkiewicz traces is presented for
the case that actions could occur and could be observed as occurring simulta-
neously (a common assumption made, e.g., by concurrency models inspired by
bio-chemical reactions as in [4]; see also [12] for other examples). This leads to
step sequences, i.e., sequences of steps rather than single actions where a step
is a set of one or more actions occurring simultaneously. To retain the philos-
ophy underlying Mazurkiewicz traces, the extended set-up is based on a few
explicit and simple design choices. Instead of the independence relation, step
alphabets use two basic relations between pairs of actions: simultaneity indicat-
ing actions that may occur together in a step, and sequentialisation indicating
equivalent orders of executing two different actions. The two relations are ap-
plied to identify step sequences as observations of the same concurrent run, and
the resulting equivalence classes of step sequences are called step traces. Step
traces can be represented by invariant structures with two relations: the mutual
exclusion and (possibly cyclic) weak causality. Step sequences have been used
to represent operational semantics of concurrent systems since a long time [5,
19, 1]. The fundamental difference between models like those in [5, 19, 1] and the
approach of this paper is that step sequences that are considered equivalent are
grouped into step traces. Moreover, each step trace uniquely defines a relational
structure, similar to how each trace defines a unique causal partial order.
A key algorithmic issue here is to decide whether an invariant structure
represents a step trace over a given step alphabet. This problem was considered
and solved for the general case in [7]. In [10], a companion paper to the present
paper, we seek further efficiency improvements by restricting the class of order
structures under consideration to those with an acyclic weak causality relation.
There it is shown that these invariant structures represent linearisable step traces,
i.e., step traces where each step A = {a1 , . . . , an } can be represented by some
equivalent sequence of singletons {ai1 }{ai2 } . . . {ain }. In other words, each step
has a linear representation. (Here it is worthwhile to remark that the requirement
that concurrent runs can be sequentialised, is not an uncommon assumption,
see e.g., [1, 2, 16, 20].) The acyclity property allows one to structurally reduce an
invariant structure to a structure which can then be used to solve the problem
in a purely local way, by considering pairs of events, rather than the whole
77
structures. Furthermore, a characterisation is given of those step alphabets that
can give rise to a given acyclic invariant structure.
In this paper, we show how one can check whether an acyclic invariant struc-
ture represents a step trace over any step alphabet. The main result here is that
the set of all step alphabets that would qualify, forms a complete lattice with
the ordering derived from relative ‘strength’ of the dependencies between pairs
of individual actions.
2 Background
In this section, we outline the main concepts of the extension of Mazurkiewicz
trace theory to step traces. Complete definitions and results, as well as illustra-
tive examples, can be found in, e.g., [7, 9, 10].
Step alphabets. A step alphabet is a triple θ = hΣ, sim, seqi, where Σ is a fi-
nite nonempty alphabet of actions, and sim (simultaneity) and seq (sequential-
isability) are irreflexive binary relations over Σ such that sim and seq \ sim are
symmetric relations.
A step over θ is a clique of the simultaneity relation sim, and step sequences
over θ are all finite sequences SSEQθ of steps. A step sequence is linear if it
consists of singleton sets.
Step traces. Two step sequences over θ, u and v, are equivalent if one can be
obtained from the other by (repeatedly): swapping two consecutive steps AB con-
sisting of actions which can be sequentialised in any order (A × B ⊆ seq ∩ seq−1 ),
splitting a step A into two consecutive steps BC provided that the resulting or-
dering of actions respects the sequentialisability given by seq (B × C ⊆ seq), and
joining adjacent steps BC into a single step B ∪ C if their order respects seq and
all actions can be simultaneous (B×C ⊆ sim∩seq). The equivalence classes STRθ
of the resulting equivalence relation on step sequences are step traces over θ.
Derived dependencies. Next to simultaneity and serialisability, it helps to use six
further (static) dependencies between actions which together partition Σ × Σ:
– rig = (Σ×Σ)\(sim∪(seq∩seq−1 )) is rigid order allowing neither simultaneity
nor changing of the order of actions.
– inl = (seq∩seq−1 )\sim is interleaving allowing to change the order of actions
that cannot occur (simultaneously) together in a step.
– ssi = sim \ (seq ∪ seq−1 ) is strong simultaneity allowing a pair of actions to
occur together in a step but disallowing serialisation and interleaving.
– sse = (seq\seq−1 )∩sim is semi-serialisability allowing a pair of simultaneous
occurrences of actions to be serialized in the order given, but not in the
reverse order.
– wdp = (seq−1 \ seq) ∩ sim is weak dependence which is the inverse of semi-
serialisability.
78
– con = sim ∩ seq ∩ seq−1 is concurrency identifying actions which can occur
simultaneously as well as in any order.
For example, let u = {{c}{ab}{a}{d} be a step sequence over the step alpha-
bet θ = hΣ, sim, seqi, where Σ = {a, b, c, d} and
sim = {hb, ci, hc, bi, hb, di, hd, bi, ha, bi, hb, ai, ha, di, hd, ai, ha, ci, hc, ai}
seq = {hb, ci, hc, bi, hb, di, hd, bi, hc, di, hd, ci, ha, di, hc, ai} .
Then τ = {{c}{ab}{a}{d}, {c}{ab}{ad}, {abc}{a}{d}, {abc}{ad}} is the trace
over θ comprising u. Moreover, the derived dependencies are as follows:
rig = id {a,b,c,d} inl = {hc, di, hd, ci} ssi = {ha, bi, hb, ai}
sse = {ha, di, hc, ai} wdp = {hd, ai, ha, ci} con = {hb, ci, hc, bi, hb, di, hd, bi} .
Events. An event is a pair a(i) = ha, ii representing the i-th occurrence of action
a ∈ Σ in some execution scenario. The default labelling of a(i) is `a(i) = a. An
event domain is a finite set of events ∆ such that if a(i) ∈ ∆ and i > 1 then also
a(i−1) ∈ ∆. If u is a step sequence, then occ(u) comprises all events a(i) such
that i does not exceed the number of occurrences of a within u, and the position
of a(i) within u is given by posu (a(i) ) = j if the i-th occurrence of a happens in
the j-th step of u.
Order structures. In Mazurkiewicz trace theory, a central role is played by acyclic
relations. In the treatment of step traces, a similar role is played by order struc-
tures or = h∆, , @i such that ∆ is an event domain, and the remaining two
components are irreflexive binary relations on ∆. An order structure or is sup-
posed to represent an execution scenario involving events in ∆. The notation
x y means that x cannot occur simultaneously with y, and x @ y that x can-
not occur later than y, i.e., only before or simultaneously with y. The relation
is called mutex and @ weak causality (or weak precedence). Moreover, ≺, defined
as the intersection of mutex and weak causality, is interpreted as causality (or
precedence). It is assumed that events on a weak causality cycle cannot be in
the mutex relation, and that all occurrences of a given action are totally ordered
by ≺+ .
Order structures with the same domain can be compared, T with or C or
0
denoting that or extends or , as well as intersected, with OS denoting the
0
intersection of a nonempty set of order structures OS .
There are three classes of order structures corresponding to the three main
classes of acyclic relations used in Mazurkiewicz trace theory.
Saturated order structures (corresponding to total orders). An order structure
or is saturated if there is no order structure or 0 6= or such that or C or 0 , and
or2sr(or ) denotes all saturated extensions of an order structure or . Each step
sequence u defines a saturated structure sseq2sr(u) = hocc(u), , @i such that,
for all x 6= y ∈ occ(u):
x y if posu (x) 6= posu (y)
x@y if posu (x) ≤ posu (y).
79
For a step alphabet θ, this establishes a one-to-one correspondence between
SSEQθ and sseq2sr(SSEQθ ), with the inverse mapping being denoted by sr2sseq.
Invariant structures (corresponding to causal partial orders).
T Each step trace
τ defines an invariant (order) structure str2ir(τ ) = sseq2sr(τ ). For a step
alphabet θ, this establishes a one-to-one correspondence between STRθ and
IRθ = str2ir(STRθ ), called the invariant structures over θ. The inverse map-
ping is ir2str(ir ) = sr2sseq(or2sr(ir )). The set of all step alphabets θ such that
ir ∈ IRθ is denoted by Θir .
Dependence structures (corresponding to dependence graphs). Deriving an in-
variant structure for a step trace following the definition of str2ir(τ ) is inefficient
as the number of step sequences in τ can be huge. Fortunately, by taking a single
step sequence in τ , one can extract all the essential causal relationships between
events in str2ir(τ ). For a step sequence u over a step alphabet θ, the resulting
dependence (order) structure is defined as sseq2orθ (u) = hocc(u), , @i, where,
for all x, y ∈ occ(u):
x y if h`x , `y i ∈ ssi ∪ rig ∪ inl ∪ wdp ∧ posu (x) < posu (y)
or h`x , `y i ∈ ssi ∪ rig ∪ inl ∪ sse ∧ posu (x) > posu (y)
(1)
x@y if h`x , `y i ∈ ssi ∪ sse ∪ wdp ∪ rig ∧ posu (x) < posu (y)
or h`x , `y i ∈ ssi ∪ sse ∧ posu (x) = posu (y).
The above definition determines if two events are weakly causally related and/or
in the mutex relationship or neither, by looking at their relative order in the step
sequence and their dependence as given in θ. For example, the first two lines of
(1) mean that if two events that are not in the same step and have labels that
cannot be sequentialised when in the same step, are in the mutex relationship.
All step sequences belonging to τ have the same dependence structure, de-
noted by sseq2orθ (τ ). The closure of the latter is the invariant structure induced
by τ , clo(sseq2orθ (τ )) = str2ir(τ ), where clo is an operation defined for order
structures generalising the transitive closure of acyclic relations. A unique depen-
dence graph underlying an invariant structure ir ∈ IRθ , is given by ir2orθ (ir ) =
sseq2orθ (ir2str(ir )).
Invariant and dependence structures can be used to develop effective repre-
sentations and algorithmic treatment for step traces.
Linearising alphabets and acyclic invariant structures. Assuming that a non-
sequential execution has an equivalent sequential representation amounts, in the
current setting, to requiring that a step trace contains a linear step sequence.
A step alphabet θ is linearising if every step trace over θ contains a linear
step sequence. (In particular, this means that ssiθ = ∅.) As the next result
demonstrates, linearising step alphabets can be characterised by acyclic invariant
structures defined as those which have acyclic weak causality relation.
Fact 1 [10] A step alphabet θ is linearising if and only if all invariant structures
in IRθ are acyclic.
80
Transitive reduction. A Hasse diagram is the most ‘efficient’ representation of a
partial order. The corresponding notion for an acyclic invariant structure ir =
h∆, , @i is the transitive reduction red(ir ) = h∆, \( r ∪ −1 r ), @ \(@ ◦ @
)i, where:
r = {hx, yi ∈ ∆ × ∆ | ∃hw, zi : w z ∧ ( (x v w @ y ∧ x v z @ y) ∨
(x @ w v y ∧ x @ z v y) ) }.
Then clo(red(ir )) = ir and one cannot remove any mutex or weak causality
relationship from red(ir ) without losing information about ir .
Alphabets of acyclic invariant structures. Transitive reduction can be used to ef-
ficiently check whether an invariant structure represents a step trace over a given
step alphabet. To formulate this result, we first introduce auxiliary notation.
For an order structure or = h∆, , @, `i, we introduce evidence relations that
capture all possible (seven) combinations of mutex and weak causality between
two distinct events:
or = {hx, yi | x @ y 6@ x y} or = {hx, yi | x 6@ y @ x y}
or = {hx, yi | x @ y 6@ x 6 y} or = {hx, yi | x 6@ y @ x 6 y}
or = {hx, yi | x 6@ y 6@ x y} or = {hx, yi | x @ y @ x 6 y}
or = {hx, yi | x 6@ y 6@ x 6 y 6= x}
In addition we use abstract symbols to represent these relationships between
events and for the relations between actions:
Evi = { , , , , , , }. and Dep = {rig, inl, ssi, sse, wdp, con}
Let x 6= y be events of an acyclic order structure or . Then the evidence of hx, yi is
defined as evior (x, y) = e, where e ∈ Evi if hx, yi ∈ eor . For a step alphabet θ and
two distinct actions, a and b, we define their dependency in θ as depθ (a, b) = d,
where d ∈ Dep if ha, bi ∈ dθ . Finally, we introduce the possible dependencies
PDir (x, y) which could relate pairs of events in an acyclic invariant structure ir .
eviir (x, y)
evired(ir ) (x, y)
PDir (x, y) wdp rig inl rig inl rig sse sse sse con con
wdp wdp con
eviir (x, y)
evired(ir ) (x, y)
PDir (x, y) sse rig inl rig inl rig wdp wdp wdp con inl
sse sse con
Table 1. Possible dependencies of hx, yi in an acyclic invariant structure.
We then obtain a characterisation of all step alphabets which match an
acyclic invariant structure.
81
Fact 2 [10] Let ir = (∆, , @) be an acyclic invariant structure, and θ be a
step alphabet such that `∆ is included in the action set of θ. Then ir ∈ IRθ if
and only if depθ (a, b) ∈ PDir (a, b), for all a 6= b ∈ `∆ , where:
\
PDir (a, b) = {PDir (x, y) | x, y ∈ ∆ ∧ `x = a ∧ `y = b} .
3 Synthesising alphabets for acyclic invariant structures
We now extend the characterisation of possible dependencies of events in acyclic
invariant structures provided for individual pairs of events in Table 1.
Proposition 1. Let ir = (∆, , @) be an acyclic invariant structure, and a 6=
b ∈ ∆. Then PDir (a, b) is one of the following 14 sets:
∅ {sse} {rig, inl} {wdp, con} {rig, inl, sse}
{rig} {wdp} {rig, sse} {sse, con} {rig, inl, sse, wdp, con}
{con} {inl} {rig, wdp} {rig, inl, wdp}
Proof. From Fact 2 it follows that, for all x 6= y ∈ ∆, we have PDir (x, y) ∈
{R1 , . . . , R11 }, where:
R1 = {inl} R2 = {sse} R3 = {wdp}
R4 = {con} R5 = {rig, wdp} R6 = {rig, sse}
R7 = {wdp, con} R8 = {con, sse} R9 = {inl, rig, wdp}
R10 = {inl, rig, sse} R11 = {inl, rig, sse, wdp, con}.
Since different pairs of events labelled in the same way may T generate different
Ri ’s, the set PDir (a, b) is, in general, be an intersection i∈K Ri , where K is
any nonempty subset of {1, 2, . . . , 11}. Thus, in principle, we have to consider
211 − 1 intersections. Fortunately, we can simplify this task greatly, as the result
follows from the straightforward observations made below:
1. The sets R1 , . . . , R11 are potential values for PDir (a, b).
2. The following are also are potential values for PDir (a, b):
– R12 = ∅ = R1 ∩ R2 .
– R13 = {rig} = R5 ∩ R6 .
– R14 = {rig, inl} = R9 ∩ R10 .
3. No new
T potential values for PDir (a, b) can be obtained through intersections
R = i∈K Ri , for nonempty K ⊆ {1, 2, . . . , 11}, since we have the following:
– If i ∈ K ∩ {1, . . . , 4} then R = Ri T or R = R12 .
– If 11 ∈ K and R 6= R11 then R = i∈K\{11} Ri .
– |R5 ∩ R6 | = |R5 ∩ R7 | = |R5 ∩ R10 | = |R6 ∩ R9 | = |R6 ∩ R8 | = |R7 ∩ R9 | =
|R8 ∩ R10 | = 1.
– R5 ∩ R8 = R6 ∩ R7 = R7 ∩ R10 = R8 ∩ R9 = ∅.
– R5 ∩ R9 = R5 , R6 ∩ R10 = R6 , and R9 ∩ R10 = R14 . t
u
82
Alphabet synthesis for a single structure. Suppose that we are given an acyclic
invariant structure ir = h∆, , @i and asked to find (or synthesise) a step
alphabet in Θir , or conclude that such an alphabet does not exist. We can
solve this problem by first computing PDir (a, b), for all pairs of distinct actions
ha, bi ∈ `∆ × `∆ . If any of the computed values is equal to ∅, we conclude
that Θir = ∅, and so the alphabet synthesis fails. Otherwise, we can find a
suitable step alphabet, in the following way. For any pair of distinct actions
ha, bi ∈ `∆ × `∆ we can arbitrarily choose a dependency d(a, b) ∈ PDir (a, b),
and then take θ = h`∆ , sim, seri, where sim = dep−1 ({con, sse, wdp}) and seq =
dep−1 ({con, sse, inl}). It is then easily seen that ir ∈ IRθ .
Alphabet synthesis for multiple structures. The solution presented above for a
single structure, can be readily generalised to sets of acyclic invariant structures.
Suppose now that IR = {ir j | j ∈ J} is a possibly infinite nonempty set of acyclic
invariant structures ir j , each such structure having the domain ∆j and using
actions Σj S = `∆j . We do not assume that the Σj ’s are the same, but assume
that
T Σ = j∈J Σj is finite. The problem is to synthesise a step alphabet in
j∈J Θ ir j , or to conclude that such an alphabet does not exist. We can solve
this problem by first computing, for all pairs of distinct actions ha, bi ∈ Σ × Σ:
PDIR (a, b) = T rig, sse, wdp, con} if J(a, b) = ∅
{inl,
j∈J(a,b) PDir j (a, b) otherwise,
where J(a, b) = {j ∈ J T | a, b ∈ Σj }. If any of the computed values is equal
to ∅, we conclude that j∈J Θir j = ∅, and so the alphabet synthesis fails.
Otherwise, we can find a suitable step alphabet, in the following way. For any pair
of distinct actions ha, bi ∈ Σ×Σ we can arbitrarily choose a dependency d(a, b) ∈
PDir (a, b), and then take θ = hΣ, sim, seri, where sim = dep−1 ({con, sse, wdp})
and seq = dep−1 ({con, sse, inl}). It is then easily seen that ir j ∈ IRθ , for every
j ∈ J.
4 A complete lattice of step alphabets
In this section, we assume that ir = h∆, , @, `i is a fixed acyclic invariant
structure such that Θir 6= ∅.
Fact 2 provides a complete characterisation of the step alphabets in Θir .
Since, in general, there may be several such alphabets, one might ask for a
method of assessing their relative ‘quality’. The results so far do not provide
us with a way of addressing this issue, and in what follows we will show that
the step alphabets in Θir can, in fact, be ordered in a manner reflecting their
potential for creating causal relationships.
We first introduce a weak partial order 4 on the dependence symbols in
Dep \ {ssi}. It is given by the (Hasse) diagram below, where 4 is directed from
lower to higher nodes, e.g., rig 4 con. Intuitively, d0 4 d means that d0 introduces
at least as much causal relationships as d.
83
con
inl
sse wdp
rig
The order on dependencies can then be used to order step alphabets.
Definition 1 (alphabet ordering). Let θ, θ0 ∈ Θir . Then θ 4 θ0 if, for all
a 6= b ∈ `∆ , depθ (a, b) 4 depθ0 (a, b).
The above definition is purely syntactical. However, it can be justified by
compelling semantical arguments as well.
Proposition 2. If θ0 , θ00 ∈ Θir , then there exists θ ∈ Θir such that:
ir2orθ (ir ) C ir2orθ0 (ir ) and ir2orθ (ir ) C ir2orθ00 (ir ).
Proof. For any a 6= b ∈ `∆ we can choose from PDir (a, b) a dependence which
is maximal from the point of view of 4. Then the result is straightforward
except for the case that wdp 4 inl (and, symmetrically, sse 4 inl) since wdp
can generate in a dependence graph. However, when both inl and wdp are
possible dependencies but con is not, then wdp can only generate , and so inl
generates strictly less causal relationships and can be chosen for θ. t
u
That is, for each pair of step alphabets in Θir , one can use 4 to find a step
alphabet which imposes fewer underlying causal relationships than the original
two alphabets. It is worth observing that a stronger result, like “θ 4 θ0 implies
ir2orθ0 (ir ) C ir2orθ (ir )”, does not in general hold. Consider, for example, an
acyclic invariant structure ir shown in Figure 1, and five step alphabets θi such
that:
depθ1 (a, b) = rig depθ2 (a, b) = wdp depθ3 (a, b) = con
depθ4 (a, b) = sse depθ5 (a, b) = inl.
In every set of possible dependencies there exist the most restrictive as well
as the most permissive choice (given by 4). However, this does not mean that
θ 4 θ0 implies that the underlying dependence structures corresponding to the
same invariant structure are comparable w.r.t. C (see ir2orθ4 (ir ) and ir2orθ5 (ir )
depicted in Figure 1).
We then obtain as the main result of this paper that there is always the
most restrictive as well as the most permissive step alphabet with which a given
acyclic invariant structure is consistent.
Theorem 1. hΘir , 4i is a complete lattice.
84
ir = ir2orθ1 (ir ) = ir2orθ2 (ir ) red(ir ) = ir2orθ3 (ir )
c c
a b a b
d d
ir2orθ4 (ir ) ir2orθ5 (ir )
c c
a b a b
d d
Fig. 1. An acyclic invariant structure ir together with its transitive reduction and
underlying dependence structures w.r.t. five different step alphabets.
Proof. Note that all 13 nonempty sets of dependence symbols from Proposition 1
form complete lattices with the relation 4.
Indeed, {sse}, {rig}, {wdp}, {con}, and {inl} are singletons (and so form
trivial lattices), and in {rig, inl}, {wdp, con}, {rig, sse}, {sse, con}, and {rig, wdp},
we have the first element in the relation 4 with the second one.
Only three larger sets remain to be considered: {rig, inl, sse}, where rig 4
inl 4 sse; {rig, inl, wdp}, where rig 4 inl 4 wdp; and {rig, inl, sse, wdp, con} which
is the whole Dep \ {ssi} used in the definition of 4.
Since, for a fixed finite set of actions Σ present in ir , the relation 4 on
step alphabets is defined component-wise (where every pair of actions is a single
component), we are dealing with a finite product of complete lattices. Such a
product obviously forms a complete lattice, which ends the proof. t
u
To conclude, as hΘir , 4i is a finite complete lattice, it has a maximal element
max
θir and a minimal element θir min
. They are given by respectively taking, for all
a 6= b ∈ `∆ :
depθirmax (a, b) = max PDir (a, b) and depθirmin (a, b) = min PDir (a, b) .
4 4
5 Mazurkiewicz traces
As noted in [8], Mazurkiewicz traces with their original sequential semantics and
partial orders as structural counterparts, may be seen as a special subclass of
step traces. The manner in which we obtain the corresponding step traces is
to consider a subclass of step alphabets Θsim . Each such step alphabet has an
empty relation sim (hence all steps are singletons). This implies that the only
two interesting dependence symbols are inl and rig. As a matter of fact, they
85
play the role of the independence relation and the dependence relation in the
setting of Mazurkiewicz traces.
Thus, in this case, we consider an acyclic invariant structure ir = h∆, , @, `i
such that is equal to (∆ × ∆) \ id ∆ , and obtain:
Theorem 2. θ ∈ Θir ∩ Θsim if and only if depθ (a, b) ∈ PDir (a, b) ∩ {rig, inl}, for
all a 6= b ∈ `∆ .
Proof. Follows from Fact 2 and the definition of Θsim . t
u
Recalling from [11] the relation ≤ defined on step alphabets (θ0 ≤ θ if at the
same time simθ0 ⊆ simθ and seqθ0 ⊆ seqθ ) we also get
Theorem 3. hΘir ∩ Θsim , ≤i is a complete lattice.
Proof. Since rig 4 inl and, in this case θ 4 θ0 iff θ ≤ θ0 , this is a direct conse-
quence of Theorems 1 and 2. t
u
6 Conclusions
In this paper we carried out a deeper discussion on the structure of step alphabets
suitable for a given labelled acyclic invariant structure. The main result proven
here states that one can always choose not only the most restrictive alphabet,
i.e., maximal in the sense of the extension relation C (proven to hold in the
general case in [11]), but also the most permissive one, i.e., minimal in the sense
of C (taking advantage of the acyclicity of an invariant structure in a significant
way).
Related work. The papers [13, 17] discuss relationships between individual events
related to causality and simultaneity (mutual exclusion). The main difference
between these works and that presented here is the assumed semantics (step
semantics, in our case, rather than a sequential semantics). There is also a dif-
ference of the meaning of some relationships. The observations discussed in [13,
17] are (complete or incomplete) sets of processes/sequences produced by a sys-
tem. On this basis, one attempts to classify causality and mutual exclusion in
all/some executions of the system. In our case, this concerns causality in a single
process (which is projected to the whole system), and mutual exclusion between
two events means that such events do not occur in the same step rather than
not in the same process as in the approach of [13, 17]. Moreover, in order to
determine relationships in [13] an idea similar to ours (comparison of arcs in
original/reduced order structure with those appearing in the closed one) is em-
ployed. Adding more concrete observations implies going up (in the direction of
more restrictive ones) in lattice of determined relationships. On the other hand,
[17] defines the strength of a relationship by quantifying its presence in the whole
history of the model processes. This corresponds to our procedure of determining
possible dependencies (using intersection, i.e., through universal quantification).
86
Future work. We plan to investigate efficient methods of step alphabet synthesis
for invariant structures without specified labelling. A possible solution is to use
the method from this paper after taking an injective labelling. However, such
an attempt does not really yield interesting results as it is clearly desirable to
ask for an optimal (from the point of view of the step alphabet size) solution,
and investigate whether assuming acyclicity of the initial structure makes any
difference.
Acknowledgement. We are grateful to the reviewers for their useful comments
and suggestions for improvement. This research was supported by Epsrc (grant
EP/K001698/1 Uncover), the Polish National Science Center (grant No.2013/-
09/D/ST6/03928), and Nserc of Canada (grant RGPIN6466-15).
References
1. Baldan, P., Busi, N., Corradini, A., Pinna, G.M.: Domain and event structure
semantics for Petri nets with read and inhibitor arcs. Theoretical Computer Science
323, 129–189 (2004)
2. Bergstra, J., Ponse, A., Smolka, S. (eds.): Handbook of Process Algebra. Elsevier,
Amsterdam (2001)
3. Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, River
Edge, NJ, USA (1995)
4. Ehrenfeucht, A., Rozenberg, G.: Reaction systems. Fundamenta Informaticae 75(1-
4), 263–280 (2007)
5. Grabowski, J.: On partial languages. Fundamenta Informaticae 4(2), 125–147
(1983)
6. Hoogeboom, H.J., Rozenberg, G.: Dependence graphs. In: The Book of Traces, pp.
43–67. World Scientific (1995)
7. Janicki, R., Kleijn, J., Koutny, M., Mikulski, Ł.: Characterising concurrent histo-
ries. Fundamenta Informaticae 139, 21–42 (2015)
8. Janicki, R., Kleijn, J., Koutny, M., Mikulski, Ł.: Order structures for subclasses of
generalised traces. In: Language and Automata Theory and Applications, Lecture
Notes in Computer Science, vol. 8977, pp. 689–700. Springer (2015)
9. Janicki, R., Kleijn, J., Koutny, M., Mikulski, Ł.: Step traces. Acta Informatica 53,
35–65 (2016)
10. Janicki, R., Kleijn, J., Koutny, M., Mikulski, Ł.: Alphabets of acyclic invari-
ant structures. Fundamenta Informaticae (accepted) pp. 1–12 (2017). See
http://folco.mat.umk.pl/papers/JKKM-2017.pdf
11. Janicki, R., Kleijn, J., Koutny, M., Mikulski, Ł.: Invariant structures and depen-
dence relations. Fundamenta Informaticae (accepted) pp. 1–27 (2017)
12. Janicki, R., Koutny, M.: Structure of concurrency. Theoretical Computer Science
112(1), 5–52 (1993)
13. Leemans, S.J.J., Fahland, D., van der Aalst, W.M.P.: Discovering block-structured
process models from incomplete event logs. In: Application and Theory of Petri
Nets and Concurrency, pp. 91–110 (2014)
14. Mazurkiewicz, A.: Concurrent program schemes and their interpretations. DAIMI
Rep. PB 78, Aarhus University (1977)
87
15. Mazurkiewicz, A.: Basic notions of trace theory. In: Linear Time, Branching Time
and Partial Order in Logics and Models for Concurrency, Lecture Notes in Com-
puter Science, vol. 354, pp. 285–363. Springer (1988)
16. Montanari, U., Rossi, F.: Contextual nets. Acta Informatica 32, 545–596 (1995)
17. Polyvyanyy, A., Weidlich, M., Conforti, R., Rosa, M.L., ter Hofstede, A.H.M.:
The 4c spectrum of fundamental behavioral relations for concurrent systems. In:
Application and Theory of Petri Nets and Concurrency, pp. 210–232 (2014)
18. Pratt, V.: Modeling concurrency with partial orders. International Journal of
Parallel Programming 15(1), 33–71 (1986)
19. Rozenberg, G., Verraedt, R.: Subset languages of Petri nets. Part I. Theoretical
Computer Science 26, 301–326 (1983)
20. Vogler, W.: Partial order semantics and read arcs. Theoretical Computer Science
286(1), 33–63 (2002)
88