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

an experiment-based definition of bisimilarity. So, even though the mechanism
we use for proving ) is similar to the one described in

[12], the current soundness proof is conceived in terms of bisimulations (and not
experiments).
Remark 2. The entailment relation

B G ∪ F PF δ G G ( F

PF CIRC uses for checking for the equiv-
alence of generalized regular expressions is an instantiation of the parametric
entailment relation from the proof system in [12]. This approach extends CIRC

to automatically reason on a large class of systems that can be modeled as
coalgebras of polynomial functors.
As already stated, our final purpose is to use CIRC as a decision procedure for the
bisimilarity of generalized regular expressions. That is, whenever provided a set
of expressions, the prover stops with an yes/no answer w.r.t. their equivalence.
In this context, an important aspect is that the sub-coalgebra generated by an
expression ε

∈ Exp G by repeatedly applying δ G G is, in general, infinite. Take
for example the polynomial functor

G

= B × Id associated to infinite streams,

and consider the property μx. . In order to prove this, CIRC

builds an infinite proof sequence by repeatedly applying δ G G as follows:
δ G G ( μx.

∅ ⊕ r x = μx.r x

∅ ⊕ r x )= δ G G ( μx.r x )

↓

0 , ∅ ⊕ ( μx. ∅ ⊕ r x ) = 0 ,μx.r x

δ G G ( ∅ ⊕

( μx.

∅ ⊕ r x

)) = δ G G ( μx.r

x

)

↓

[...]
In this case, the prover would never stop. It is shown in [2,15] that the axioms for
associativity, commutativity and idempotency (ACI) guarantee finiteness of the
generated sub-coalgebra (note that these axioms have also been proven sound
w.r.t. bisimulation). ACI properties can easily be specified in CIRC as the prover
is an extension of Maude, which has a powerful matching modulo ACUI capabil-
ity. The idempotency is given by the equation ε

0 , ∅ ⊕∅⊕ ( μx. ∅ ⊕ r x ) = 0 ,μx.r x

⊕ ε = ε , and the commutativity

and associativity are specified as attributes of ⊕ .

Theorem 4. Let G be a set of proof obligations over generalized regular expres-

sions. CIRC can be used as a decision procedure for the equivalences in G , that

is, it can assert whenever a goal ( ε 1 ,ε 2 ) is a true or false equality.

Proof. The result is a consequence of the fact that by implementing the ACI ax-
ioms in CIRC , the set of new goals obtained by repeatedly applying the derivative
δ is finite. In these circumstances, whenever CIRC stops according to the reduc-
tion rule [Done] , the initial proof obligations are bisimilar. On the other hand,
whenever it terminates with [Fail] , the goals are not bisimilar.

∈G

4.1 A CIRC -Based Tool
We have implemented a tool that, when provided with a functor , automat-

ically generates a specification for CIRC which can then be used in order to

G