A Decision Procedure for Bisimilarity of Generalized Regular Expressions | Zendy

Marcello Bonsangue | Zendy; Georgiana Caltais | Zendy; Eugen-Ioan Goriac | Zendy; Dorel Lucanu | Zendy; Jan Rutten | Zendy; Alexandra Silva | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Decision Procedure for Bisimilarity of Generalized Regular Expressions

Author(s) -

Marcello Bonsangue,

Georgiana Caltais,

Eugen-Ioan Goriac,

Dorel Lucanu,

Jan Rutten,

Alexandra Silva

Publication year - 2011

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

DOI - 10.1007/978-3-642-19829-8_15

Subject(s) - kleene's recursion theorem , kleene algebra , automaton , class (philosophy) , mathematics , regular expression , set (abstract data type) , coalgebra , algebra over a field , algebraic number , discrete mathematics , computer science , theoretical computer science , pure mathematics , programming language , artificial intelligence , mathematical analysis

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 bisimilar 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research