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

2020 ◽  
pp. 3-20 ◽  
Author(s):  
David N. Jansen ◽  
Jan Friso Groote ◽  
Jeroen J. A. Keiren ◽  
Anton Wijs
Keyword(s):  
Equivalence Relation ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Branching Bisimulation ◽  
Memory Efficient

Abstract 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.

scholarly journals Relating Apartness and Bisimulation

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Herman Geuvers ◽  
Bart Jacobs
Keyword(s):  
Transition System ◽  
Proof System ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Induction Principle ◽  
Weak Bisimulation ◽  
Initial Algebra ◽  
Branching Bisimulation ◽  
Dual Notion ◽  
Labelled Transition System

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.

scholarly journals Natural Quantum Operational Semantics with Predicates

2008 ◽  
Vol 18 (3) ◽  
pp. 341-359 ◽  
Author(s):  
Marek Sawerwain ◽  
Roman Gielerak
Keyword(s):  
Positive Operator ◽  
Operational Semantics ◽  
General Definition ◽  
Completely Positive Maps ◽  
Transition Systems ◽  
Positive Operator Valued Measures ◽  
Labelled Transition Systems ◽  
Positive Maps ◽  
Definition Of ◽  
Positive Operator Valued Measure

Natural Quantum Operational Semantics with PredicatesA general definition of a quantum predicate and quantum labelled transition systems for finite quantum computation systems is presented. The notion of a quantum predicate as a positive operator-valued measure is developed. The main results of this paper are a theorem about the existence of generalised predicates for quantum programs defined as completely positive maps and a theorem about the existence of a GSOS format for quantum labelled transition systems. The first theorem is a slight generalisation of D'Hondt and Panagaden's theorem about the quantum weakest precondition in terms of discrete support positive operator-valued measures.

Sign in / Sign up

Export Citation Format

Share Document