research-article

Partition refinement for bisimilarity in CCP

Authors:

Andres Aristizabal,

Filippo Bonchi,

Frank D. Valencia,

Luis Fernando PinoAuthors Info & Claims

SAC '12: Proceedings of the 27th Annual ACM Symposium on Applied Computing

Pages 88 - 93

https://doi.org/10.1145/2245276.2245296

Published: 26 March 2012 Publication History

Abstract

Saraswat's concurrent constraint programming (ccp) is a mature formalism for modeling processes (or programs) that interact by telling and asking constraints in a global medium, called the store. Bisimilarity is a standard behavioural equivalence in concurrency theory, but a well-behaved notion of bisimilarity for ccp has been proposed only recently. When the state space of a system is finite, the ordinary notion of bisimilarity can be computed via the well-known partition refinement algorithm, but unfortunately, this algorithm does not work for ccp bisimilarity.

In this paper, we propose a variation of the partition refinement algorithm for verifying ccp bisimilarity. To the best of our knowledge this is the first work providing for the automatic verification of program equivalence for ccp.

References

[1]

A. Aristizabal, F. Bonchi, C. Palamidessi, L. Pino, and F. D. Valencia. Deriving labels and bisimilarity for concurrent constraint programming. In FOSSACS, pages 138--152, 2011.

Digital Library

[2]

A. Aristizabal, F. Bonchi, L. Pino, and F. Valencia. Partition refinement for bisimilarity in ccp (extended version). Technical report, INRIA-CNRS, 2012. Available at: http://www.lix.polytechnique.fr/~andresaristi/sac2012.pdf.

Digital Library

[3]

F. Bonchi, F. Gadducci, and G. V. Monreale. Reactive systems, barbed semantics, and the mobile ambients. In FOSSACS, pages 272--287, 2009.

Digital Library

[4]

F. Bonchi, B. König, and U. Montanari. Saturated semantics for reactive systems. In LICS, pages 69--80, 2006.

Digital Library

[5]

F. Bonchi and U. Montanari. Minimization algorithm for symbolic bisimilarity. In ESOP, pages 267--284, 2009.

Digital Library

[6]

T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms (3. ed.). MIT Press, 2009.

Digital Library

[7]

F. S. de Boer, A. D. Pierro, and C. Palamidessi. Nondeterminism and infinite computations in constraint programming. Theor. Comput. Sci., 151(1): 37--78, 1995.

Digital Library

[8]

J.-C. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Sci. Comput. Program., 13(1): 219--236, 1989.

Digital Library

[9]

G. Ferrari, S. Gnesi, U. Montanari, M. Pistore, and G. Ristori. Verifying mobile processes in the hal environment. In CAV, pages 511--515, 1998.

Digital Library

[10]

P. C. Kanellakis and S. A. Smolka. Ccs expressions, finite state processes, and three problems of equivalence. In PODC, pages 228--240, 1983.

Digital Library

[11]

R. Milner and D. Sangiorgi. Barbed bisimulation. In ICALP, pages 685--695, 1992.

Digital Library

[12]

U. Montanari and V. Sassone. Dynamic congruence vs. progressing bisimulation for ccs. FI, 16(1): 171--199, 1992.

Digital Library

[13]

V. A. Saraswat and M. C. Rinard. Concurrent constraint programming. In POPL, pages 232--245, 1990.

Digital Library

[14]

V. A. Saraswat, M. C. Rinard, and P. Panangaden. Semantic foundations of concurrent constraint programming. In POPL, pages 333--352, 1991.

Digital Library

[15]

B. Victor and F. Moller. The mobility workbench - a tool for the pi-calculus. In CAV, pages 428--440, 1994.

Digital Library

Cited By

Pino LAristizábal ABonchi FValencia F(2015)Weak CCP bisimilarity with strong proceduresScience of Computer Programming10.1016/j.scico.2014.09.007100:C(84-104)Online publication date: 15-Mar-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.09.007
Pino LBonchi FValencia F(2014)A Behavioral Congruence for Concurrent Constraint Programming with Nondeterministic ChoiceTheoretical Aspects of Computing – ICTAC 201410.1007/978-3-319-10882-7_21(351-368)Online publication date: 2014
https://doi.org/10.1007/978-3-319-10882-7_21
Pino LBonchi FValencia FPeña RSchrijvers T(2013)Efficient computation of program equivalence for confluent concurrent constraint programmingProceedings of the 15th Symposium on Principles and Practice of Declarative Programming10.1145/2505879.2505902(263-274)Online publication date: 16-Sep-2013
https://dl.acm.org/doi/10.1145/2505879.2505902
Show More Cited By

Recommendations

Weak CCP bisimilarity with strong procedures

We show that the standard saturation method for reducing weak bisimilarity to strong bisimilarity does not work for CCP.We provide a new saturation method for reducing weak bisimilarity to strong bisimilarity for CCP.We prove that due to distinctive ...
Quasi-Open Bisimilarity with Mismatch is Intuitionistic
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This minimal extension of quasi-open bisimilarity ...
Compositional Analysis of Protocol Equivalence in the Applied $π$ -Calculus Using Quasi-open Bisimilarity
Theoretical Aspects of Computing – ICTAC 2021
Abstract
This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied $π$ -calculus. Furthermore, we show that this equivalence is suited to security and privacy problems expressed as an equivalence problem in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '12: Proceedings of the 27th Annual ACM Symposium on Applied Computing

March 2012

2179 pages

ISBN:9781450308571

DOI:10.1145/2245276

Conference Chairs:
Sascha Ossowski
University Rey Juan Carlos, Spain
,
Paola Lecca
The Microsoft Research - University of Trento COSBI, Italy

Copyright © 2012 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

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 March 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAC 2012

Sponsor:

SIGAPP

SAC 2012: ACM Symposium on Applied Computing

March 26 - 30, 2012

Trento, Italy

Acceptance Rates

SAC '12 Paper Acceptance Rate 270 of 1,056 submissions, 26%;

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
91
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pino LAristizábal ABonchi FValencia F(2015)Weak CCP bisimilarity with strong proceduresScience of Computer Programming10.1016/j.scico.2014.09.007100:C(84-104)Online publication date: 15-Mar-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.09.007
Pino LBonchi FValencia F(2014)A Behavioral Congruence for Concurrent Constraint Programming with Nondeterministic ChoiceTheoretical Aspects of Computing – ICTAC 201410.1007/978-3-319-10882-7_21(351-368)Online publication date: 2014
https://doi.org/10.1007/978-3-319-10882-7_21
Pino LBonchi FValencia FPeña RSchrijvers T(2013)Efficient computation of program equivalence for confluent concurrent constraint programmingProceedings of the 15th Symposium on Principles and Practice of Declarative Programming10.1145/2505879.2505902(263-274)Online publication date: 16-Sep-2013
https://dl.acm.org/doi/10.1145/2505879.2505902
Olarte CRueda CValencia F(2013)Models and emerging trends of concurrent constraint programmingConstraints10.1007/s10601-013-9145-318:4(535-578)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10601-013-9145-3
Aristizábal ABonchi FPino LValencia F(2012)Reducing Weak to Strong Bisimilarity in CCPElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.104.2104(2-16)Online publication date: 14-Dec-2012
https://doi.org/10.4204/EPTCS.104.2

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