A Decision Procedure for Bisimilarity of Generalized Regular Expressions - Formal Methods: Foundations and Applications - page 227

For coalgebras of a large class of functors, a language of regular expressions;
a corresponding generalization of Kleene's theorem; and a sound and complete
axiomatization for the associated notion of behavioral equivalence were intro-
duced in [2,1]. Both the language of expressions and their axiomatization were
derived, in a modular fashion, from the functor defining the type of the system.
Algebra and related tools can be successfully used for reasoning on properties
of systems. In this paper, we present a novel method for checking for the bisim-
ilarity of generalized regular expressions using the coinductive theorem prover
CIRC [4,12]. The main novelty of the method lies on the generality of the systems
it can handle. CIRC is a metalanguage application implemented in Maude [3],
and its target is to prove properties over infinite data structures. It has been
successfully used for checking the equivalence of programs, and trace equiva-
lence and strong bisimilarity of processes. The tool may be tested online and
downloaded from http://fsl.cs.uiuc.edu/index.php/Circ .
The main contributions of this paper can be summarized as follows. We
present the algebraic counterpart of the coalgebraic framework of the gener-
alized regular expressions mentioned above. This enables us to automatically
derive algebraic specifications that model the language of expressions, and to
define an appropriate equational entailment relation for checking for the be-
havioural equivalence of expressions. Furthermore, the implementation of both
the algebraic specification and the entailment relation in CIRC allows for auto-
matic reasoning on the equivalence of expressions.
Organization of the paper. Section 2 recalls the basic definitions of the language
associated to a polynomial functor. Section 3 formulates the aforementioned
language as an algebraic specification, which paves the way to implement in
CIRC a procedure to decide equivalence of expressions. The decision procedure
and the soundness of its implementation in CIRC are described in Section 4. In
Section 4.1 we show, by means of examples, how one can check for bisimilarity,
using CIRC . Section 5 contains concluding remarks and pointers for future work.

2 Regular Expressions for Polynomial Coalgebras

In this section, we briefly recall the basic definitions in [2,15].
Let Set denote the category of sets (represented by capital letters X,Y,... )
and functions (represented by lower case letters f,g,... ). The notation Y X repre-
sents the family of functions from X to Y . The product of two sets X, Y is written
as X × Y and has the projections functions π 1 and π 2 : X

π 1
←−

π 2
−→ X × Y Y .

We define X + Y = X Y {⊥ , } where is the disjoint union of sets, with

κ 1
−→

κ 2
←−

injections X

+ Y is different from the
classical coproduct of X and Y (which we shall denote by X + Y ), because of
the two extra elements ⊥ and . These extra elements will later be used to
represent, respectively, underspecification and inconsistency in the specification
of some systems.

X Y Y . Note that the set X