Relating Apartness and Bisimulation

A bisimulation for a coalgebra of a functor on the category of sets can be described via a coalgebra in the category of relations, of a lifted functor. A final coalgebra then gives rise to the coinduction principle, which states that two bisimilar elements are equal. For polynomial functors, this leads to well-known descriptions. In the present paper we look at the dual notion of "apartness". Intuitively, two elements are apart if there is a positive way to distinguish them. Phrased differently: two elements are apart if and only if they are not bisimilar. Since apartness is an inductive notion, described by a least fixed point, we can give a proof system, to derive that two elements are apart. This proof system has derivation rules and two elements are apart if and only if there is a finite derivation (using the rules) of this fact. We study apartness versus bisimulation in two separate ways. First, for weak forms of bisimulation on labelled transition systems, where silent (tau) steps are included, we define an apartness notion that corresponds to weak bisimulation and another apartness that corresponds to branching bisimulation. The rules for apartness can be used to show that two states of a labelled transition system are not branching bismilar. To support the apartness view on labelled transition systems, we cast a number of well-known properties of branching bisimulation in terms of branching apartness and prove them. Next, we also study the more general categorical situation and show that indeed, apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle. In this analogy, we include the powerset functor, which gives a semantics to non-deterministic choice in process-theory.

Causal Semantics for BPP Nets with Silent Moves

BPP nets, a subclass of finite Place/Transition Petri nets, are equipped with some causal behavioral semantics, which are variations of fully-concurrent bisimilarity [3], inspired by weak [28] or branching bisimulation [12] on labeled transition systems. Then, we introduce novel, efficiently decidable, distributed semantics, inspired by team bisimulation [17] and h-team bisimulation [19], and show how they relate to these variants of fully-concurrent bisimulation.

An O(m log n) algorithm for branching bisimilarity on labelled transition systems

Branching bisimilarity is a behavioural equivalence relation on labelled transition systems (LTSs) that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than ones for other weak behavioural equivalences, especially weak bisimilarity. With m the number of transitions and n the number of states, the classic $${O\left( {m n}\right) }$$ algorithm was recently replaced by an $$O({m (\log \left| { Act }\right| + \log n)})$$ algorithm [9], which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari [20], resulting in a simpler $$O({m \log n})$$ algorithm. Benchmarks show that in practice this algorithm is also faster and often far more memory efficient than its predecessors, making it the best option for branching bisimulation minimisation and preprocessing for calculating other weak equivalences on LTSs.