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