Information Technology Reference
In-Depth Information
automatically check whether two
-expressions are bisimilar. The tool is imple-
mented as a metalanguage application in Maude. It can be downloaded from
http://circidei.info.uaic.ro/functorizer/functorizer.maude
.
Let us now show another example: Mealy machines, which are coalgebras
for the functor (
B
×
Id
)
A
. In what follows we show how
CIRC
canbeusedin
conjunction with our tool in order to act as a decision procedure when checking
for the equivalence of two expressions.
Formally, a Mealy machine is a pair (
S, α
) consisting of a set
S
of states and
a transition function
α
:
S
G
S
)
A
, which for each state
s
→
(
B
×
∈
S
and input
A
associates an output value
b
and a next state
s
. Typically, we write
a
∈
a
|
b
α
(
s
)(
a
)=
b, s
⇔
s
s
. As an example, consider the Mealy machine
depicted in Fig. 3, where all the states are bisimilar.
We first show how to check for the
equivalence of two expressions characteriz-
ing the states
s
1
and
s
2
from the Mealy
machine in Fig. 3. These expressions, which
could be computed, using the algorithm in
Kleene's theorem, are
ε
1
=
a
(
rμx.a
(
rx
)
⊕
b
(
s
1
a
|
0
a|
0
b
|
0
b
|
0
s
2
a
|
0
b
|
0
a
|
0
b
|
0
∅
)
)
⊕
b
(
r
μy.a
(
r
y
)
⊕
b
(
r
y
)
)and
ε
2
=
Fig. 3.
Mealy machine:
s
1
∼ s
2
μx.a
(
r
), respectively.
In order to check for the bisimilarity of
ε
1
and
ε
2
we load the tool and define
the semilattice
B
=
x
)
⊕
b
(
r
x
{
0
}
and the alphabet
A
=
{
a, b
}
:
(jslt B is 0 bottom 0 . 0 v 0 = 0 . endjslt)
(alph A is a b endalph)
We provide the functor
using the command
(functor (B x Id)
^
A.)
.Thecom-
mand
(set goal ... .)
specifies the goal we want to prove:
(set goal a(r<
G
μ
X:FixpVar . a(r< X:FixpVar >) (+) b(
∅
)>) (+)
μ
b(r<
Y:FixpVar . a(r< Y:FixpVar >) (+) b(r< Y:FixpVar >) >) =
μ
X:FixpVar . a(r< X:FixpVar >) (+) b(r< X:FixpVar >) .)
In order to generate the
CIRC
specification we use the command
(generate
coalgebra .)
. Next we need to load
CIRC
along with the resulting specification
and start the proving engine using the command
(coinduction .)
.
As already shown, behind the scenes,
CIRC
builds a bisimulation relation that
includes the initial goal. The proof succeeds and the output consists of (a subset
of) this bisimulation:
Proof succeeded.
Number of derived goals: 3
Number of proving steps performed: 82
[...]
Proved properties:
[...]
a(r<
μ
X . a(r< X >) (+) b(
∅
) >) (+)
μ
b(r<
Y . a(r< Y >) (+) b(r< Y >) >)) =
μ
X . a(r< X >) (+) b(r< X >)
Search WWH ::
Custom Search