Information Technology Reference
In-Depth Information
As previously mentioned, CIRC is also able to detect when two expressions
are not equivalent. Take, for instance, the expressions μx.a ( r
a ( l
1
)
x
)and
a ( r
), characterizing the states s 1 and s 3 from the Mealy
machines in Fig. 4. After following some steps similar to the ones previously enu-
merated, the proof fails and the output message is Visible goal [...] failed
during coinduction .
a ( l
1
)
)
μx.a ( r
x
a| 0
a| 0
a| 1
s 1
s 2
s 3
s 4
s 5
a| 0
a| 1
Fig. 4. Mealy machines: s 1 ∼ s 3
5 Conclusions and Future Work
One of the major contributions of this paper is that we exploited an encoding
of coalgebra into algebra, and provided a decision procedure for the bisimilar-
ity of generalized regular expressions. In order to enable the implementation of
the decision procedure, we formalized the equivalence between the coalgebraic
concepts associated to polynomial coalgebras [2,1] and their algebraic correspon-
dents. This led to the definition of algebraic specifications (
E G )thatmodelboth
the language and the coalgebraic structure of expressions. Moreover, we defined
an equational deduction relation (
PF ), used on the algebraic side for reasoning
on the bisimilarity of expressions.
The most important result of the parallel between the coalgebraic and al-
gebraic approaches is given in Corollary 1, which formalizes the definition of
the bisimulation relations, in algebraic terms. Actually, this result is the key for
proving the soundness of the decision procedure implemented in the automated
prover CIRC [11]. As a coinductive prover, CIRC builds a relation
F
closed un-
der the application of δ G
) ), hence
automatically computing a bisimulation the initial proof obligations belong to.
The approach we present in this paper enables CIRC to perform a reasoning
based on bisimulations (instead of experiments [12]). This way, the prover is
extended to checking for the bisimilarity in a large class of systems that can be
modeled as
with respect to
PF
(
E G ∪ F PF
δ G (
F
-coalgebras. Note that the constructions above are all automated
- the (non-trivial) CIRC algebraic specification describing
G
E G , together with the
PF are generated with the Maude tool presented in
interpolants implementing
Section 4.1.
As future work, we intend to extend our proof system to Kripke polynomial
coalgebras and to exploit more of the axioms in [1] with the purpose of improving
the prover's time performance (our experience so far shows that by adding the
axiom for the distribution of the
expression through the constructors, the
prover works significantly faster).
 
Search WWH ::




Custom Search