Computing maximal weak and other bisimulations

Formal Aspects of Computing - Tập 28 Số 3 - Trang 381-407 - 2016
Alexandre Boulgakov1, Thomas Gibson−Robinson1, A. W. Roscoe1
1Department of Computer Science, University of Oxford, Oxford, UK OX1 3QD#TAB#

Tóm tắt

Abstract We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.

Từ khóa


Tài liệu tham khảo

Armstrong P Goldsmith M Lowe G Ouaknine J Palikareva H Roscoe AW Worrell J (2012) Recent developments in FDR. In: Computer aided verification. Springer pp 699–704

Boulgakov A Gibson-Robinson T Roscoe AW (2014) Computing maximal bisimulations. In: Formal methods and software engineering. Springer pp 11–26

10.1016/S1571-0661(05)80390-1

10.1007/s10009-004-0185-2

Blom S van de Pol J (2009) Distributed branching bisimulation minimization by inductive signatures. arXiv preprint arXiv:0912.2550

10.1016/S0304-3975(03)00361-X

10.1016/0167-6423(90)90071-K

10.1145/367766.368168

10.1007/s10009-012-0244-z

Gibson-Robinson T Armstrong P Boulgakov A Roscoe AW (2015) FDR3: a parallel refinement checker for CSP. Int J Softw Tools Technol Transf 1–19

Groote JF, 1990, Automata, languages and programming, volume 443 of Lecture notes in computer science, 626

10.5555/3921

Kanellakis PC Smolka SA (1983) CCS expressions finite state processes and three problems of equivalence. In: Proceedings of the 2nd annual ACM symposium on principles of distributed computing PODC ’83 pp 228–240 New York NY USA ACM

Mateescu R (2005) On-the-fly state space reductions for weak equivalences. In: Proceedings of the 10th international workshop on formal methods for industrial critical systems pp 80–89 ACM

Milner R (1981) A modal characterisation of observable machine-behaviour. In: CAAP’81. Springer pp 25–34

10.5555/901178

10.1137/0216062

Phillips ICC Ulidowski I (1996) Ordered SOS rules and weak bisimulation. Theory Formal Methods

Roscoe AW Gardiner PHB Goldsmith MH Hulance JR Jackson DM Scattergood JB (1995) Hierarchical compression for model-checking CSP or how to check 10 20 dining philosophers for deadlock. In: Proceedings of TACAS 1995. BRICS

Roscoe AW (1994) Model-checking CSP. A classical mind: essays in honour of CAR Hoare

Roscoe AW (1998) The theory and practice of concurrency

10.1007/978-1-84882-258-0

10.1007/s002360050036

10.1137/0201010

10.1007/BF00268499

10.1145/233551.233556

Wimmer R Herbstritt M Hermanns H Strampp K Becker B (2006) Sigref—a symbolic bisimulation tool box. In: Automated technology for verification and analysis. Springer pp 477–492

Thông tin
Thông tin xuất bản

Formal Aspects of Computing

Tập 28 Số 3

381-407

Thông tin tác giả