Connexion

English version

PPS UMR 7126 – Laboratoire
Preuves, Programmes et Systèmes

Accueil · Présentation · Membres · Publications · Séminaire · Groupes de travail · Projets · πr²

Filippo Bonchi (CWI et LiX)

A Minimization Algorithm for Symbolic Bisimilarity

Abstract: The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics is defined in terms of bisimilarity that, in the finite case, can be computed via the well-known partition refinement algorithm. However, the behaviour of interactive systems is in many cases infinite and thus checking bisimilarity in this way is unfeasible. Symbolic semantics allows to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some sources of infiniteness. Unfortunately, the standard partition refinement algorithm does not work with symbolic bisimilarity. In a previous work, we have introduced an abstract theory of symbolic semantics encompassing different kinds of semantics, such as asynchronous and open bisimilarity for the pi-calculus. In this talk, we will show a partition refinement algorithm for symbolic bisimilarity by employing as running example open Petri nets.