PREG Axiomatizer : A Ground Bisimilarity Checker for GSOS with Predicates

Aceto, Luca; Caltais, Georgiana; Goriac, Eugen-Ioan; Ingolfsdottir, Anna

PREG Axiomatizer : A Ground Bisimilarity Checker for GSOS with Predicates

Dateien

Aceto_2-1ujbbwdk8rj2i6.pdfGröße: 141.27 KBDownloads: 234

Datum

2011

Autor:innen

Aceto, Luca

Caltais, Georgiana

Goriac, Eugen-Ioan

Ingolfsdottir, Anna

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Beitrag zu einem Konferenzband

Publikationsstatus

Published

Erschienen in

CORRADINI, Andrea, ed., Bartek KLIN, ed., Corina CÎRSTEA, ed.. Algebra and Coalgebra in Computer Science : 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011, proceedings. Berlin: Springer, 2011, pp. 378-385. Lecture Notes in Computer Science. 6859. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-642-22943-5. Available under: doi: 10.1007/978-3-642-22944-2_27

Zusammenfassung

PREG Axiomatizer is a tool used for proving strong bisimilarity between ground terms consisting of operations in the GSOS format extended with predicates. It automatically derives sound and ground-complete axiomatizations using a technique proposed by the authors of this paper. These axiomatizations are provided as input to the Maude system, which, in turn, is used as a reduction engine for provided ground terms. These terms are bisimilar if and only if their normal forms obtained in this fashion are equal. The motivation of this tool is the optimized handling of equivalence checking between complex ground terms within automated provers and checkers.

Fachgebiet (DDC)

004 Informatik

Schlagwörter

Structural operational semantics, GSOS rule format, bisimilarity, equational axiomatizations, Maude

Konferenz

4th International Conference, CALCO 2011, 30. Aug. 2011 - 2. Sep. 2011, Winchester, UK

Zitieren

ISO 690

ACETO, Luca, Georgiana CALTAIS, Eugen-Ioan GORIAC, Anna INGOLFSDOTTIR, 2011. PREG Axiomatizer : A Ground Bisimilarity Checker for GSOS with Predicates. 4th International Conference, CALCO 2011. Winchester, UK, 30. Aug. 2011 - 2. Sep. 2011. In: CORRADINI, Andrea, ed., Bartek KLIN, ed., Corina CÎRSTEA, ed.. Algebra and Coalgebra in Computer Science : 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011, proceedings. Berlin: Springer, 2011, pp. 378-385. Lecture Notes in Computer Science. 6859. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-642-22943-5. Available under: doi: 10.1007/978-3-642-22944-2_27

BibTex

@inproceedings{Aceto2011Axiom-44687,
  year={2011},
  doi={10.1007/978-3-642-22944-2_27},
  title={PREG Axiomatizer : A Ground Bisimilarity Checker for GSOS with Predicates},
  number={6859},
  isbn={978-3-642-22943-5},
  issn={0302-9743},
  publisher={Springer},
  address={Berlin},
  series={Lecture Notes in Computer Science},
  booktitle={Algebra and Coalgebra in Computer Science : 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011, proceedings},
  pages={378--385},
  editor={Corradini, Andrea and Klin, Bartek and Cîrstea, Corina},
  author={Aceto, Luca and Caltais, Georgiana and Goriac, Eugen-Ioan and Ingolfsdottir, Anna}
}

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/44687">
    <dcterms:title>PREG Axiomatizer : A Ground Bisimilarity Checker for GSOS with Predicates</dcterms:title>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:issued>2011</dcterms:issued>
    <dc:rights>terms-of-use</dc:rights>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/44687/1/Aceto_2-1ujbbwdk8rj2i6.pdf"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-01-23T12:44:14Z</dc:date>
    <dc:creator>Ingolfsdottir, Anna</dc:creator>
    <dc:creator>Aceto, Luca</dc:creator>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-01-23T12:44:14Z</dcterms:available>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/44687/1/Aceto_2-1ujbbwdk8rj2i6.pdf"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/44687"/>
    <dc:contributor>Goriac, Eugen-Ioan</dc:contributor>
    <dc:contributor>Aceto, Luca</dc:contributor>
    <dc:creator>Goriac, Eugen-Ioan</dc:creator>
    <dc:contributor>Caltais, Georgiana</dc:contributor>
    <dcterms:abstract xml:lang="eng">PREG Axiomatizer is a tool used for proving strong bisimilarity between ground terms consisting of operations in the GSOS format extended with predicates. It automatically derives sound and ground-complete axiomatizations using a technique proposed by the authors of this paper. These axiomatizations are provided as input to the Maude system, which, in turn, is used as a reduction engine for provided ground terms. These terms are bisimilar if and only if their normal forms obtained in this fashion are equal. The motivation of this tool is the optimized handling of equivalence checking between complex ground terms within automated provers and checkers.</dcterms:abstract>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Ingolfsdottir, Anna</dc:contributor>
    <dc:language>eng</dc:language>
    <dc:creator>Caltais, Georgiana</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Nein