Confluence of CHR Revisited

Invariants and Modulo Equivalence

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint HThe invariant is formalizedandling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.
Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation : 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers
EditorsFred Mesnard, Peter J. Stuckey
Volume11408
Place of PublicationCham
PublisherSpringer
Publication date2019
Pages94-111
ISBN (Print)978-3-030-13837-0
ISBN (Electronic)978-3-030-13838-7
DOIs
Publication statusPublished - 2019
EventLOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation - Göthe-University Frankfurt am Main, Frankfurt am Main, Germany
Duration: 4 Sep 20186 Sep 2018
Conference number: 28
http://ppdp-lopstr-18.cs.uni-frankfurt.de/lopstr18.html

Conference

ConferenceLOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation
Number28
LocationGöthe-University Frankfurt am Main
CountryGermany
CityFrankfurt am Main
Period04/09/201806/09/2018
Internet address
SeriesLecture Notes in Computer Science
Volume11408
ISSN0302-9743
SeriesTheoretical Computer Science and General Issues
Volume11408

Keywords

  • Constraint Handling Rules
  • Confluence
  • Confluence modulo equivalence
  • Invariants
  • Observable confluence

Cite this

Christiansen, H., & Kirkeby, M. H. (2019). Confluence of CHR Revisited: Invariants and Modulo Equivalence. In F. Mesnard, & P. J. Stuckey (Eds.), Logic-Based Program Synthesis and Transformation: 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers (Vol. 11408, pp. 94-111). Cham: Springer. Lecture Notes in Computer Science, Vol.. 11408, Theoretical Computer Science and General Issues, Vol.. 11408 https://doi.org/10.1007/978-3-030-13838-7_6
Christiansen, Henning ; Kirkeby, Maja Hanne. / Confluence of CHR Revisited : Invariants and Modulo Equivalence. Logic-Based Program Synthesis and Transformation: 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers. editor / Fred Mesnard ; Peter J. Stuckey. Vol. 11408 Cham : Springer, 2019. pp. 94-111 (Lecture Notes in Computer Science, Vol. 11408). (Theoretical Computer Science and General Issues, Vol. 11408).
@inproceedings{546f965d538e48168f3f2bd3fc355f0a,
title = "Confluence of CHR Revisited: Invariants and Modulo Equivalence",
abstract = "Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint HThe invariant is formalizedandling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.",
keywords = "Constraint Handling Rules, Confluence, Confluence modulo equivalence, Invariants, Observable confluence, Constraint Handling Rules, Confluence, Confluence modulo equivalence, Invariants, Observable confluence",
author = "Henning Christiansen and Kirkeby, {Maja Hanne}",
year = "2019",
doi = "10.1007/978-3-030-13838-7_6",
language = "English",
isbn = "978-3-030-13837-0",
volume = "11408",
pages = "94--111",
editor = "Fred Mesnard and Stuckey, {Peter J.}",
booktitle = "Logic-Based Program Synthesis and Transformation",
publisher = "Springer",

}

Christiansen, H & Kirkeby, MH 2019, Confluence of CHR Revisited: Invariants and Modulo Equivalence. in F Mesnard & PJ Stuckey (eds), Logic-Based Program Synthesis and Transformation: 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers. vol. 11408, Springer, Cham, Lecture Notes in Computer Science, vol. 11408, Theoretical Computer Science and General Issues, vol. 11408, pp. 94-111, Frankfurt am Main, Germany, 04/09/2018. https://doi.org/10.1007/978-3-030-13838-7_6

Confluence of CHR Revisited : Invariants and Modulo Equivalence. / Christiansen, Henning; Kirkeby, Maja Hanne.

Logic-Based Program Synthesis and Transformation: 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers. ed. / Fred Mesnard; Peter J. Stuckey. Vol. 11408 Cham : Springer, 2019. p. 94-111 (Lecture Notes in Computer Science, Vol. 11408). (Theoretical Computer Science and General Issues, Vol. 11408).

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Confluence of CHR Revisited

T2 - Invariants and Modulo Equivalence

AU - Christiansen, Henning

AU - Kirkeby, Maja Hanne

PY - 2019

Y1 - 2019

N2 - Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint HThe invariant is formalizedandling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.

AB - Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint HThe invariant is formalizedandling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.

KW - Constraint Handling Rules

KW - Confluence

KW - Confluence modulo equivalence

KW - Invariants

KW - Observable confluence

KW - Constraint Handling Rules

KW - Confluence

KW - Confluence modulo equivalence

KW - Invariants

KW - Observable confluence

U2 - 10.1007/978-3-030-13838-7_6

DO - 10.1007/978-3-030-13838-7_6

M3 - Article in proceedings

SN - 978-3-030-13837-0

VL - 11408

SP - 94

EP - 111

BT - Logic-Based Program Synthesis and Transformation

A2 - Mesnard, Fred

A2 - Stuckey, Peter J.

PB - Springer

CY - Cham

ER -

Christiansen H, Kirkeby MH. Confluence of CHR Revisited: Invariants and Modulo Equivalence. In Mesnard F, Stuckey PJ, editors, Logic-Based Program Synthesis and Transformation: 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers. Vol. 11408. Cham: Springer. 2019. p. 94-111. (Lecture Notes in Computer Science, Vol. 11408). (Theoretical Computer Science and General Issues, Vol. 11408). https://doi.org/10.1007/978-3-030-13838-7_6