Publikation:

Automatic equivalence proofs for non-deterministic coalgebras

Lade...
Vorschaubild

Dateien

Bonsangue_2-c0deiwdbltt68.pdf
Bonsangue_2-c0deiwdbltt68.pdfGröße: 277.92 KBDownloads: 156

Datum

2013

Autor:innen

Bonsangue, Marcello
Goriac, Eugen-Ioan
Lucanu, Dorel
Rutten, Jan
Silva, Alexandra

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Zeitschriftenartikel
Publikationsstatus
Published

Erschienen in

Science of Computer Programming. 2013, 78(9), pp. 1324-1345. ISSN 0167-6423. eISSN 1872-7964. Available under: doi: 10.1016/j.scico.2012.07.001

Zusammenfassung

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.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Coalgebra, Algebra, Bisimilarity, Automatic reasoning

Konferenz

Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

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. 2013, 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>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Unbekannt
Diese Publikation teilen