Information Technology Reference
In-Depth Information
A Decision Procedure for Bisimilarity of
Generalized Regular Expressions
Marcello Bonsangue
1
, Georgiana Caltais
2
,
3
, Eugen-Ioan Goriac
2
,
3
,
Dorel Lucanu
3
, Jan Rutten
4
,
5
,
6
, and Alexandra Silva
4
1
LIACS - Leiden University, The Netherlands
marcello@liacs.nl
2
School of Computer Science - Reykjavik University, Iceland
{
gcaltais10,egoriac10
}
@ru.is
3
Faculty of Computer Science - Alexandru Ioan Cuza University, Romania
4
Centrum voor Wiskunde en Informatica, The Netherlands
dlucanu@info.uaic.ro
5
Radboud University Nijmegen, The Netherlands
{
janr,ams
}
@cwi.nl
6
Vrije Universiteit Amsterdam, The Netherlands
Abstract.
A notion of generalized regular expressions for a large class
of systems modeled as coalgebras, and an analogue of Kleene's theorem
and Kleene algebra, were recently proposed by a subset of the authors
of this paper. Examples of the systems covered include infinite streams,
deterministic automata and Mealy machines. In this paper, we present a
novel algorithm and a tool to decide whether two expressions are bisim-
ilar or not. The procedure is implemented in the automatic theorem
prover CIRC, by reducing coinduction to an entailment relation between
an algebraic specification and an appropriate set of equations.
1
Introduction
Regular expressions and deterministic automata (DFA's) constitute two of the
most basic structures in computer science. Kleene's theorem [8] gives a funda-
mental correspondence between these two structures: each regular expression
denotes a language that can be recognized by a DFA and, conversely, the lan-
guage accepted by a DFA can be specified by a regular expression. Languages
denoted by regular expressions are called regular. Two regular expressions are
(language) equivalent if they denote the same regular language. Salomaa [14] pre-
sented a sound and complete axiomatization (later refined by Kozen in [9,10])
for proving the equivalence of regular expressions.
Coalgebras arose in the last decade as a suitable mathematical framework
to study state-based systems, such as DFA's. For a functor
G
:
Set
→
Set
,a
G
-coalgebra or
G
-system is a pair (
S, g
), consisting of a set
S
of states and
a function
g
:
S
→
G
(
S
) defining the “transitions” of the states. We call the
functor
the type of the system. For instance, DFA's can be readily modeled
as finite coalgebras of the functor
G
S
A
.
G
(
S
)=2
×
Search WWH ::
Custom Search