Publikation:

A Decision Procedure for Bisimilarity of Generalized Regular Expressions

Vorschaubild

Dateien

Bonsangue_2-yi8hayl9n9430.pdf
Bonsangue_2-yi8hayl9n9430.pdfGröße: 246.36 KBDownloads: 190

Datum

2011

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

URI (zitierfähiger Link)
http://nbn-resolving.de/urn:nbn:de:bsz:352-2-yi8hayl9n9430
DOI (zitierfähiger Link)
https://doi.org/10.1007/978-3-642-19829-8_15
ArXiv-ID

Internationale Patentnummer

Link zur Lizenz
Urheberrechtlich geschützt

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Open Access Green

Sammlungen

Informatik und Informationswissenschaft: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

DAVIES, Jim, ed., Leila SILVA, ed., Adenilso SIMAO, ed.. Formal Methods: Foundations and Applications : 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, revised Selected Papers. Berlin: Springer, 2011, pp. 226-241. Lecture Notes in Computer Science. 6527. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-642-19828-1. Available under: doi: 10.1007/978-3-642-19829-8_15

Zusammenfassung

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.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Decision Procedure, Regular Expression, Proof System, Reduction Rule, Entailment Relation

Konferenz

13th Brazilian Symposium on Formal Methods, SBMF 2010, 8. Nov. 2010 - 11. Nov. 2010, Natal, Brazil
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, 2011. A Decision Procedure for Bisimilarity of Generalized Regular Expressions. 13th Brazilian Symposium on Formal Methods, SBMF 2010. Natal, Brazil, 8. Nov. 2010 - 11. Nov. 2010. In: DAVIES, Jim, ed., Leila SILVA, ed., Adenilso SIMAO, ed.. Formal Methods: Foundations and Applications : 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, revised Selected Papers. Berlin: Springer, 2011, pp. 226-241. Lecture Notes in Computer Science. 6527. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-642-19828-1. Available under: doi: 10.1007/978-3-642-19829-8_15
BibTex
@inproceedings{Bonsangue2011Decis-44688,
  year={2011},
  doi={10.1007/978-3-642-19829-8_15},
  title={A Decision Procedure for Bisimilarity of Generalized Regular Expressions},
  number={6527},
  isbn={978-3-642-19828-1},
  issn={0302-9743},
  publisher={Springer},
  address={Berlin},
  series={Lecture Notes in Computer Science},
  booktitle={Formal Methods: Foundations and Applications : 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, revised Selected Papers},
  pages={226--241},
  editor={Davies, Jim and Silva, Leila and Simao, Adenilso},
  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/44688">
    <dc:creator>Lucanu, Dorel</dc:creator>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:creator>Bonsangue, Marcello</dc:creator>
    <dc:creator>Caltais, Georgiana</dc:creator>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:title>A Decision Procedure for Bisimilarity of Generalized Regular Expressions</dcterms:title>
    <dc:contributor>Silva, Alexandra</dc:contributor>
    <dc:contributor>Lucanu, Dorel</dc:contributor>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/44688/1/Bonsangue_2-yi8hayl9n9430.pdf"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/44688/1/Bonsangue_2-yi8hayl9n9430.pdf"/>
    <dc:creator>Rutten, Jan</dc:creator>
    <dc:contributor>Rutten, Jan</dc:contributor>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-01-23T12:47:40Z</dc:date>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-01-23T12:47:40Z</dcterms:available>
    <dcterms:issued>2011</dcterms:issued>
    <dc:contributor>Goriac, Eugen-Ioan</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/44688"/>
    <dc:language>eng</dc:language>
    <dc:contributor>Caltais, Georgiana</dc:contributor>
    <dcterms:abstract xml:lang="eng">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.</dcterms:abstract>
    <dc:creator>Goriac, Eugen-Ioan</dc:creator>
    <dc:contributor>Bonsangue, Marcello</dc:contributor>
    <dc:creator>Silva, Alexandra</dc:creator>
  </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
Diese Publikation teilen