Sibylle Fröschle

 

1 Theses (BibTeX Source)

@PHDTHESIS{Fr04:thesis,
  AUTHOR = {Sibylle Fr{\"o}schle},
  TITLE = {Decidability and Coincidence of Equivalences for Concurrency},
  SCHOOL = {University of Edinburgh},
  YEAR = {2004},
  URL = {http://homepages.inf.ed.ac.uk/sib/thesis.pdf},
  TASK = {4},
  ABSTRACT = {
There are two fundamental problems concerning equivalence relations in
concurrency. One is: for which system classes is a given equivalence
decidable? The second is: when do two equivalences coincide?
Two well-known equivalences are history preserving bisimilarity
(hpb) and hereditary history preserving bisimilarity (hhpb).
These are both `independence' equivalences: they reflect causal
dependencies between events. Hhpb is obtained from hpb by adding a
`backtracking' requirement. This seemingly small change makes hhpb
computationally far harder: hpb is well-known to be decidable for
finite-state systems, whereas the decidability of hhpb has been a
renowned open problem for many years; only recently it has been
shown undecidable. The main aim of this thesis is to gain insights
into the decidability problem for hhpb, and to analyse when it
coincides with hpb; less technically, we might say, to analyse the
power of the interplay between concurrency, causality, and conflict.

We first examine the backtracking condition, and see that it has
two dimensions: the number of transitions over which one may backtrack,
and the number of backtracking moves. These dimensions translate into
two hierarchies of bisimilarities; we find that both of them are strict,
and that each of their levels is decidable.

Our second approach is to analyse which behavioural properties of
concurrent systems are crucial to the increased power of hhpb.
After establishing a minimum of behavioural situations necessary
to keep hpb and hhpb distinct, we study two aspects of the
interplay of causality, concurrency, and conflict: three
synchronization witness (SW) situations, and the notion of confusion.
With the help of a composition and decomposition result we prove that
in their entirety the SW situations are essential for non-coincidence
(for bounded-degree systems). However, we show this is not so for
confusion, which disproves the long-standing conjecture that hpb and
hhpb coincide for confusion-free systems.

We continue by studying two structural system classes with promising
behavioural properties. First we consider basic parallel processes
(BPP), with a suitable partial order semantics. These systems are
infinite-state, but they restrict synchronization. Using the tableau
technique, we prove the decidability and coincidence of hpb and hhpb
for simple BPP (SBPP). The two bisimilarities do not coincide for the
complete BPP class, but we separately achieve decidability of both
(a known result for hpb, but not for hhpb).

The second structural class is (safe) free choice systems, an important
class in Petri net theory. These systems have a controlled interplay of
concurrency and conflict, and thereby exclude confusion. Having shown
that hpb and hhpb do not coincide here, we identify another interesting
candidate: live strictly state machine decomposable (SSMD) free choice
systems. For this class, we prove that an auxiliary bisimilarity
satisfies a restricted backtracking property. As a consequence we achieve
the coincidence of hpb and hhpb for a subclass of live SSMD free choice
systems: the only known positive result for a class with a reasonable
amount of interplay between concurrency, causality, and conflict while
still admitting considerable nondeterminism.}
}