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 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. © 2011 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Bonsangue, M., Caltais, G., Goriac, E. I., Lucanu, D., Rutten, J., & Silva, A. (2011). A decision procedure for bisimilarity of generalized regular expressions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6527 LNCS, pp. 226–241). https://doi.org/10.1007/978-3-642-19829-8_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
