Automatic equivalence proofs for non-deterministic coalgebras

Loading...
Thumbnail Image
Date
2013
Authors
Bonsangue, Marcello
Goriac, Eugen-Ioan
Lucanu, Dorel
Rutten, Jan
Silva, Alexandra
Editors
Contact
Journal ISSN
Electronic ISSN
ISBN
Bibliographical data
Publisher
Series
DOI (citable link)
ArXiv-ID
International patent number
Link to the license
EU project number
Project
Open Access publication
Restricted until
Title in another language
Research Projects
Organizational Units
Journal Issue
Publication type
Journal article
Publication status
Published
Published in
Science of Computer Programming ; 78 (2013), 9. - pp. 1324-1345. - ISSN 0167-6423. - eISSN 1872-7964
Abstract
A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analog 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, Mealy machines and labeled transition systems. In this paper, we present 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. We illustrate the generality of the tool with three examples: infinite streams of real numbers, Mealy machines and labeled transition systems.
Summary in another language
Subject (DDC)
004 Computer Science
Keywords
Coalgebra, Algebra, Bisimilarity, Automatic reasoning
Conference
Review
undefined / . - undefined, undefined. - (undefined; undefined)
Cite This
ISO 690BONSANGUE, Marcello, Georgiana CALTAIS, Eugen-Ioan GORIAC, Dorel LUCANU, Jan RUTTEN, Alexandra SILVA, 2013. Automatic equivalence proofs for non-deterministic coalgebras. In: Science of Computer Programming. 78(9), pp. 1324-1345. ISSN 0167-6423. eISSN 1872-7964. Available under: doi: 10.1016/j.scico.2012.07.001
BibTex
@article{Bonsangue2013-09Autom-44681,
  year={2013},
  doi={10.1016/j.scico.2012.07.001},
  title={Automatic equivalence proofs for non-deterministic coalgebras},
  number={9},
  volume={78},
  issn={0167-6423},
  journal={Science of Computer Programming},
  pages={1324--1345},
  author={Bonsangue, Marcello and Caltais, Georgiana and Goriac, Eugen-Ioan and Lucanu, Dorel and Rutten, Jan and Silva, Alexandra}
}
RDF
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/44681">
    <dcterms:issued>2013-09</dcterms:issued>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/44681"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-01-23T11:13:29Z</dc:date>
    <dcterms:abstract xml:lang="eng">A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analog 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, Mealy machines and labeled transition systems. In this paper, we present 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. We illustrate the generality of the tool with three examples: infinite streams of real numbers, Mealy machines and labeled transition systems.</dcterms:abstract>
    <dcterms:title>Automatic equivalence proofs for non-deterministic coalgebras</dcterms:title>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Caltais, Georgiana</dc:contributor>
    <dc:contributor>Bonsangue, Marcello</dc:contributor>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/44681/1/Bonsangue_2-c0deiwdbltt68.pdf"/>
    <dc:contributor>Rutten, Jan</dc:contributor>
    <dc:creator>Rutten, Jan</dc:creator>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:language>eng</dc:language>
    <dc:creator>Silva, Alexandra</dc:creator>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Goriac, Eugen-Ioan</dc:contributor>
    <dc:creator>Bonsangue, Marcello</dc:creator>
    <dc:rights>terms-of-use</dc:rights>
    <dc:creator>Goriac, Eugen-Ioan</dc:creator>
    <dc:creator>Lucanu, Dorel</dc:creator>
    <dc:contributor>Silva, Alexandra</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/44681/1/Bonsangue_2-c0deiwdbltt68.pdf"/>
    <dc:creator>Caltais, Georgiana</dc:creator>
    <dc:contributor>Lucanu, Dorel</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-01-23T11:13:29Z</dcterms:available>
  </rdf:Description>
</rdf:RDF>
Internal note
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Contact
URL of original publication
Test date of URL
Examination date of dissertation
Method of financing
Comment on publication
Alliance license
Corresponding Authors der Uni Konstanz vorhanden
International Co-Authors
Bibliography of Konstanz
No
Refereed
Unknown