research-article

Analyzing divergence in bisimulation semantics

Authors:

Wenhui ZhangAuthors Info & Claims

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Pages 735 - 747

https://doi.org/10.1145/3009837.3009870

Published: 01 January 2017 Publication History

Abstract

Some bisimulation based abstract equivalence relations may equate divergent systems with non-divergent ones, examples including weak bisimulation equivalence and branching bisimulation equivalence. Thus extra efforts are needed to analyze divergence for the compared systems. In this paper we propose a new method for analyzing divergence in bisimulation semantics, which relies only on simple observations of individual transitions. We show that this method can verify several typical divergence preserving bisimulation equivalences including two well-known ones. As an application case study, we use the proposed method to verify the HSY collision stack to draw the conclusion that the stack implementation is correct in terms of linearizability with lock-free progress condition.

References

[1]

M. Hennessy and G. Plotkin. A term model for CCS, Lecture notes in computer science, Vol.88, Springer-Verlag, 1980.

Digital Library

[2]

David Park: Concurrency and automata on infinite sequences. Lecture Notes in Computer Science 104,1981. Proceedings of 5th GI Conference.

Digital Library

[3]

J. van Benthem. Modal Logic and Classic Logic. Bibliopolis, 1983.

[4]

R. Milner: A complete axiomatisation for observational congruence of finite-state behaviours. Inf. Comput. 81(1989)227-247.

Digital Library

[5]

D.J. Walker. Bisimulation and divergence, Information and Computation, vol. 85, pp. 212-241, 1990.

Digital Library

[6]

Rob J. van Glabbeek: The Linear Time - Branching Time Spectrum II. CONCUR 1993: 66-81.

Digital Library

[7]

Rob J. van Glabbeek, Peter Weijland: Branching time and abstraction in bisimulation semantics. J. ACM 43(3):555-600.1996

Digital Library

[8]

D. Hendler, N. Shavit, and L. Yerushalmi: A scalable lock-free stack algorithm. In SPAA 2004: Proceedings of the sixteenth annual ACM symposium on Parallel Algorithms, June 27-30, 2004, Barcelona, Spain, pages 206-215, 2004

Digital Library

[9]

R. Colvin, L. Groves. A Scalable lock-free stack algorithm and its verification. fifth IEEE International conference on software engineering and formal methods. 2007

Digital Library

[10]

Rob J. van Glabbeek, Bas Luttik, Nikola Trcka: Branching Bisimilarity with Explicit Divergence. Fundam. Inform. 93(4): 371-392. 2009

[11]

Rob J. van Glabbeek, Bas Luttik, Nikola Trcka: Computation tree logic with deadlock detection. Logical Methods in Computer Science. Vol.5(4:5) 2009, pages 1-24.

[12]

K. S. Namjoshi. A simple characterization of stuttering bisimulation. In 17th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1346 of Lecture Notes in Computer Science, pages 284-296.

Digital Library

[13]

M. Herlihy, J. Wing, H. Hermanns: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463-492(1990)

Digital Library

[14]

M. Lohrey, P. R. D’Argenio, H. Hermanns: Axiomatising divergence. Inf. Comput. 203(2005)115-144.

Digital Library

[15]

I. Filipovic, P. O’Hearn, N.Rinetzky, H. Yang: Abstraction for concurrent objects. Theor. Comput. Sci. (2010).

Digital Library

[16]

Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao: Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. CONCUR 2013: 227-241.

Digital Library

[17]

Hongjin Liang, Xinyu Feng, Zhong Shao: Compositional verification of termination-preserving refinement of concurrent programs. CSLLICS 2014: 65:1-10.

Digital Library

[18]

Alexey Gotsman, Hongseok Yang: Liveness-Preserving Atomicity Abstraction. ICALP (2) 2011: 453-465.

Digital Library

[19]

X. Yang, J. Katoen, H. Lin, H. Wu: Proving linearizability via branching bisimulation. CoRR abs/1609.07546(2016)

Cited By

Liu XYu TGorla D(2021)A complete axiomatisation for divergence preserving branching congruence of finite-state behavioursProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470647(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470647
Jain MManolios P(2019)Local and Compositional Reasoning for Optimized Reactive SystemsComputer Aided Verification10.1007/978-3-030-25540-4_32(553-571)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25540-4_32
Liu XYu TZhang W(2018)Logics for Bisimulation and DivergenceFoundations of Software Science and Computation Structures10.1007/978-3-319-89366-2_12(221-237)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89366-2_12
Show More Cited By

Index Terms

Analyzing divergence in bisimulation semantics

Recommendations

Analyzing divergence in bisimulation semantics
POPL '17

Some bisimulation based abstract equivalence relations may equate divergent systems with non-divergent ones, examples including weak bisimulation equivalence and branching bisimulation equivalence. Thus extra efforts are needed to analyze divergence ...
Branching time and abstraction in bisimulation semantics

In comparative concurrency semantics, one usually distinguishes between linear time and branching time semantic equivalences. Milner's notion of observatin equivalence is often mentioned as the standard example of a branching time equivalence. In this ...
Bisimulation on speed: a unified approach

Two process-algebraic approaches have been developed for comparing two bisimulation-equivalent processes with respect to speed: the one of Moller/Tofts equips actions with lower time bounds, while the other by Lüttgen/Vogler considers upper time bounds ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

January 2017

901 pages

ISBN:9781450346603

DOI:10.1145/3009837

General Chair:
Giuseppe Castagna
Paris Diderot University, France / CNRS, France
,
Program Chair:
Andrew D. Gordon
Microsoft Research, UK / University of Edinburgh, UK

ACM SIGPLAN Notices Volume 52, Issue 1
POPL '17
January 2017
901 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3093333
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '17

Sponsor:

SIGPLAN

POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 15 - 21, 2017

Paris, France

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
344
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)2

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liu XYu TGorla D(2021)A complete axiomatisation for divergence preserving branching congruence of finite-state behavioursProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470647(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470647
Jain MManolios P(2019)Local and Compositional Reasoning for Optimized Reactive SystemsComputer Aided Verification10.1007/978-3-030-25540-4_32(553-571)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25540-4_32
Liu XYu TZhang W(2018)Logics for Bisimulation and DivergenceFoundations of Software Science and Computation Structures10.1007/978-3-319-89366-2_12(221-237)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89366-2_12
Liu XZhang W(2018)Characterization and Verification of Stuttering EquivalenceSymposium on Real-Time and Hybrid Systems10.1007/978-3-030-01461-2_7(116-132)Online publication date: 29-Sep-2018
https://doi.org/10.1007/978-3-030-01461-2_7
He KWu HChen Y(2023)On divergence-sensitive weak probabilistic bisimilarityInformation and Computation10.1016/j.ic.2023.105033292(105033)Online publication date: Jun-2023
https://doi.org/10.1016/j.ic.2023.105033
Liu XYu TGorla D(2021)A complete axiomatisation for divergence preserving branching congruence of finite-state behavioursProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470647(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470647
Li LGunter E(2020)Per-Location SimulationNASA Formal Methods10.1007/978-3-030-55754-6_16(267-287)Online publication date: 11-May-2020
https://dl.acm.org/doi/10.1007/978-3-030-55754-6_16

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents