<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Marcello Bonsangue</style></author><author><style face="normal" font="default" size="100%">Georgiana Caltais</style></author><author><style face="normal" font="default" size="100%">Eugen Goriac</style></author><author><style face="normal" font="default" size="100%">Dorel Lucanu</style></author><author><style face="normal" font="default" size="100%">Jan Rutten</style></author><author><style face="normal" font="default" size="100%">Alexandra Silva</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">A decision procedure for bisimilarity of generalized regular expressions</style></title><secondary-title><style face="normal" font="default" size="100%">Proceedings of the 13th Brazilian Symposium on Formal Methods (SBMF 2010)</style></secondary-title><tertiary-title><style face="normal" font="default" size="100%">Lecture Notes in Computer Science</style></tertiary-title></titles><dates><year><style  face="normal" font="default" size="100%">2010</style></year><pub-dates><date><style  face="normal" font="default" size="100%">November </style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/xana/files/sbmf10.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Springer</style></publisher><pub-location><style face="normal" font="default" size="100%">Natal, Brazil</style></pub-location><volume><style face="normal" font="default" size="100%">6527</style></volume><pages><style face="normal" font="default" size="100%">226–241</style></pages><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;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 tool where the aforementioned expressions can be derived automatically and a novel algorithm 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.&lt;/p&gt;
</style></abstract></record></records></xml>