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

Theorem 2. Consider a polynomial functor G and F an ingredient of G .If R is

-expressions, and σ, σ : σ, σ ∈ a binary relation on the set of G F ( Exp G ) then

σ = σ . F ( cl ( R id )) iff E G ∪ R PF

Proof. The proof is by induction on the structure of F .Take,forexamplethe

direct implication “ ⇒ ”. The base case F = B holds by the reflexivity of PF .

The case = Id follows immediately according to an auxiliary result stating

that if ( ε, ε )

F

ε = ε . Inductive steps hold by ∈ cl ( R id )then E G ∪ R PF

the rules (5), (6) and (7), defining PF . A similar reasoning is used for proving

“ ⇐ ”.

Corollary 1. Let G be a polynomial functor. If R is a binary relation on the

set of G -expressions, then cl ( R id ) is a bisimulation iff E G ∪ R PF δ G G ( R ) .

Proof. The result follows immediately according to the equivalences:

( ε, ε ) δ G G ( ε ) ,δ G G ( ε ) cl ( R id )isabisimulation ⇔ (Definition 1) ( ∀ ∈ cl ( R id )) . ∈

G ( cl ( R id )) ⇔ (Theorem 2) E G ∪ R PF δ G G ( cl ( R id )) ⇔ (def. cl ( R id ) , PF ) E G ∪

R PF δ G G ( R ) .

4 A Decision Procedure for Bisimilarity

In this section we describe how the coinductive theorem prover CIRC [11] can
be used to implement a decision procedure for the bisimilarity of generalized
regular expressions.
CIRC can be seen as an extension of Maude with behavioral features and its
implementation is derived from that of Full-Maude. In order to use the prover,
one needs to provide a specification (a CIRC theory) and a set of goals. A CIRC
theory )) consists of an algebraic specification ( S, Σ, E ),

aset Δ of derivatives (= Σ -contexts), and a set

B =( S, ( Σ,Δ ) , ( E, I

I of equational interpolants,

which are expressions of the form e where e and e i are equations

(for more information on equational interpolants see [6]). A derivative δ

⇒{ e i | i ∈ I }

∈ Δ is

a Σ -term containing a special variable ∗ : s ,where s is the sort of the variable ∗ .

If e is an equation t = t with t and t of sort s ,then δ [ e ]is δ [ t/

∗

: s ]= δ [ t /

∗

: s ].

Let Δ [ e ]denotetheset

{ δ [ e ] | δ ∈ Δ appropriate for e }

.
CIRC implements the coinductive proof system given in [12] using a set of
reduction rules of the form ( F , G ), where

B , F , G ) ⇒ ( B , B represents a specifi-

cation, is the

current set of goals. The freezing operator is defined as described in Section 3.
Here is a brief description of these rules:

F is the coinductive hypothesis (a set of frozen equations) and G

[Done] :( ⇒·

Whenever the set of goals is empty, the system terminates with success.
[Reduce] :(

B , F , {} )

B , F , G∪{ e } ) ⇒ ( B , F , G ) if B∪F e

If the current goal is a -consequence of B∪F then e is removed from the

set of goals.