Partition Refinement for Bisimilarity in CCP

Andrés Aristizábal; Filippo Bonchi; Luis Pino; Frank D. Valencia

hal-00641408, version 1

Partition Refinement for Bisimilarity in CCP

Andrés Aristizábal () ^1, 2, Filippo Bonchi () ³, Luis Pino () ¹, Frank D. Valencia () ^1, 2

27th ACM Symposium On Applied Computing (2012) 6 pages

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

1: COMETE (INRIA Saclay - Ile de France)
INRIA – Polytechnique - X – CNRS : UMR7161
2: Laboratoire d'informatique de l'école polytechnique (LIX)
CNRS : UMR7161 – Polytechnique - X
3: Laboratoire de l'Informatique du Parallélisme (LIP)
Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I

hal-00641408, version 1
http://hal.archives-ouvertes.fr/hal-00641408
oai:hal.archives-ouvertes.fr:hal-00641408
From: Frank D. Valencia <>
Submitted on: Tuesday, 15 November 2011 17:51:20
Updated on: Tuesday, 4 December 2012 17:03:29

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00641408"><analytic>
<author><persName><forename>Andrés</forename><surname>Aristizábal</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">COMETE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Polytechnique - X</orgName>
<orgName type="institution">CNRS : UMR7161</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LIX</orgName>
<orgName type="team">Laboratoire d'informatique de l'école polytechnique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7161</orgName>
<orgName type="institution">Polytechnique - X</orgName>
</affiliation>
</author>
<author><persName><forename>Filippo</forename><surname>Bonchi</surname></persName>
<affiliation>
<orgName type="laboratory">LIP</orgName>
<orgName type="team">Laboratoire de l'Informatique du Parallélisme</orgName>
<country>FR</country>
<orgName type="institution">Université de Lyon</orgName>
<orgName type="institution">CNRS : UMR5668</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École Normale Supérieure - Lyon</orgName>
<orgName type="institution">Université Claude Bernard - Lyon I</orgName>
</affiliation>
</author>
<author><persName><forename>Luis</forename><surname>Pino</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">COMETE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Polytechnique - X</orgName>
<orgName type="institution">CNRS : UMR7161</orgName>
</affiliation>
</author>
<author><persName><forename>Frank D.</forename><surname>Valencia</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">COMETE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Polytechnique - X</orgName>
<orgName type="institution">CNRS : UMR7161</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LIX</orgName>
<orgName type="team">Laboratoire d'informatique de l'école polytechnique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7161</orgName>
<orgName type="institution">Polytechnique - X</orgName>
</affiliation>
</author>
<title type="main" level="a">Partition Refinement for Bisimilarity in CCP</title></analytic><monogr><title level="m" type="main">Proceedings of the 27th ACM Symposium On Applied Computing</title><meeting>27th ACM Symposium On Applied Computing</meeting><imprint><pubPlace><settlement>Trento</settlement><country>Italy</country></pubPlace><biblScope type="publicationDate">2012-00-00</biblScope><biblScope type="pp">6 pages</biblScope></imprint></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00641408</idno><idno type="HALFile">http://hal.archives-ouvertes.fr/hal-00641408/PDF/hal-sac2012_camera-ready_.pdf</idno></biblStruct>
</listBibl>
</listBibl>