4 results
Daniel Hirschkoff ; Damien Pous.
We give an axiomatisation of strong bisimilarity on a small fragment of CCS that does not feature the sum operator. This axiomatisation is then used to derive congruence of strong bisimilarity in the finite pi-calculus in absence of sum. To our knowledge, this is the only nontrivial subcalculus of […]
Published on May 14, 2008
Paul Brunet ; Damien Pous.
Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations. We consider Kleene allegories, i.e., Kleene algebras […]
Published on September 26, 2017
Jean-Marie Madiot ; Damien Pous ; Davide Sangiorgi.
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible […]
Published on September 17, 2021
Damien Pous ; Jurriaan Rot.
In the context of abstract coinduction in complete lattices, the notion of compatible function makes it possible to introduce enhancements of the coinduction proof principle. The largest compatible function, called the companion, subsumes most enhancements and has been proved to enjoy many good […]
Published on August 8, 2019