Partition Refinement for Bisimilarity in CCP - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2012

Partition Refinement for Bisimilarity in CCP

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
Fichier principal
Vignette du fichier
hal-sac2012.pdf (184.25 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00641408 , version 1 (15-11-2011)
hal-00641408 , version 2 (04-12-2012)
hal-00641408 , version 3 (05-12-2012)

Identifiers

Cite

Andrés Aristizábal, Filippo Bonchi, Luis Pino, Frank D. Valencia. Partition Refinement for Bisimilarity in CCP. 27th ACM Symposium On Applied Computing, Mar 2012, Trento, Italy. pp.88-93. ⟨hal-00641408v3⟩
351 View
368 Download

Altmetric

Share

Gmail Facebook X LinkedIn More