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

By applying the definition in [2], the coalgebra structure on expressions δ R
would be given by:

δ R : Exp R → B × Exp R
δ R ( ∅ ) = 0 , ∅

b 2 ,ε 1 ⊕ ε 2 )where δ R ( ε 1 ⊕ ε 2 )= b 1 ∨ b i ,ε i = δ R ( ε i ) ,i =1 , 2

δ R ( μx.ε ) δ R ( ε [ μx.ε/x ])

δ R ( l ε 1 ) = δ BR ( ε 1 ) , ∅

δ R ( r ε ) = ⊥ B ,ε

δ BR ( ∅ ) = ⊥ B

δ BR ( b ) b

δ BR ( ε 1 )
The proof of Kleene's theorem provides algorithms to go from expressions to
streams and vice-versa. We illustrate it by means of examples.
Consider the following stream:

ε 1 )= δ BR ( ε 1 )

δ BR ( ε 1 ⊕ ∨

s 1 s 2 s 3

1 0 1

We draw the stream with an automata-like flavor. The transitions indicate the
tail of the stream represented by a state and the output value the head. In a
more traditional notation, the above automata represents the infinite stream
(1 , 0 , 1 , 0 , 1 , 0 , 1 ,... ).
To compute expressions ε 1 , ε 2 and ε 3 equivalent to s 1 , s 2 and s 3 we associate
with each state s i avariable x i and we solve the following system of 3 equations
in 3 variables:

ε 1 = μx 1 .l 1 ⊕rx 2 ε 2 = μx 2 .l 0 ⊕rx 3 ε 3 = μx 3 .l 1 ⊕rx 2

which yields the following closed expressions:

ε 1 = μx 1 .l 1 ⊕ r ε 2 ε 2 = μx 2 .l 0 ⊕ r ε 3 ε 3 = μx 3 .l 1 ⊕ r μx 2 .l 0 ⊕ r x 3

satisfying, by construction, ε 1 ∼ s 3 .

For the converse construction, consider the expression ε =( μx.r

s 1 , ε 2 ∼ s 2 and ε 3 ∼

x ⊕ l

.
We construct an automaton by repeatedly applying the coalgebra structure on
expressions δ R , modulo ACI (associativity, commutativity and idempotency of
⊕

) 1

) in order to guarantee finiteness.
Applying the definition of δ R above, we have:

δ R ( ε )= 1 , ( μx.r x ) ⊕∅ and δ R (( μx.r x ) ⊕∅ )= 0 , ( μx.r x ) ⊕∅

which leads to the following stream (automaton):

ε

( μx.r x ) ⊕∅

1 0