Next-preserving branching bisimulation

Yatapanage, Nisansala and Winter, Kirsten (2013) Next-preserving branching bisimulation. ITEE Technical Report 2013-02, School of Information Technology and Electrical Engineering, The University of Queensland.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
UQ312343.pdf Full text (open access) application/pdf 492.62KB 94
UQ312343_OA.pdf Full text (open access) application/pdf 1019.30KB 4
Author Yatapanage, Nisansala
Winter, Kirsten
Title Next-preserving branching bisimulation
School, Department or Centre School of Information Technology and Electrical Engineering
Institution The University of Queensland
Open Access Status Other
Report Number 2013-02
Series ITEE Technical Report
Publication date 2013-10-15
Start page 120
End page 142
Total pages 22
Publisher Elsevier
Language eng
Formatted Abstract/Summary
Bisimulations are equivalence relations between transition systems which assure that certain aspects of the behaviour of the systems are the same in a related pair. For many applications it is not possible to maintain such an equivalence unless non-observable (stuttering) behaviour is ignored. However, existing bisimulation relations which permit the removal of non-observable behaviour are unable to preserve temporal logic formulas referring to the next step operator. In this paper we propose a family of next-preserving branching bisimulations to overcome this limitation.

Next-preserving branching bisimulations are parameterised with a natural number, indicating the nesting depth of the X operators that the bisimulation preserves, while still allowing non-observable behaviour to be reduced. Based on van Glabbeek and Weijland’s notion of branching bisimulation with explicit divergence, we define the novel parameterised relation for which we prove the preservation of CTL formulas with an X operator-nesting depth that is not greater than the specified parameter. It can be shown that the family of next-preserving bisimulations constitutes a hierarchy that fills the gap between branching bisimulation and strong bisimulation.

As an example for its application we show how this definition gives rise to an advanced slicing procedure that creates a formula-specific slice, which constitutes a reduced model of the system that can be used as a substitute when verifying this formula. The result is a novel procedure for generating slices that are next-preserving branching bisimilar to the original model for any formula. We can assure that each slice preserves the formula it corresponds to, which renders the overall verification process sound.
Keyword Bisimulation
Temporal logic
Model checking
Transition system
Behavior trees
Q-Index Status Confirmed Code
Institutional Status UQ

Document type: Department Technical Report
Collection: School of Information Technology and Electrical Engineering Publications
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Thu, 17 Oct 2013, 10:13:26 EST by Ms Diana Cassidy on behalf of School of Information Technol and Elec Engineering