Confluence of CHR Revisited: Invariants and Modulo Equivalence

Henning Christiansen; Maja Hanne Kirkeby

doi:10.1007/978-3-030-13838-7_6

Confluence of CHR Revisited: Invariants and Modulo Equivalence

Henning Christiansen, Maja Hanne Kirkeby

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer 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.

Originalsprog	Engelsk
Titel	Logic-Based Program Synthesis and Transformation : 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers
Redaktører	Fred Mesnard, Peter J. Stuckey
Vol/bind	11408
Udgivelsessted	Cham
Forlag	Springer
Publikationsdato	2019
Sider	94-111
ISBN (Trykt)	978-3-030-13837-0
ISBN (Elektronisk)	978-3-030-13838-7
DOI	https://doi.org/10.1007/978-3-030-13838-7_6
Status	Udgivet - 2019
Begivenhed	LOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation - Göthe-University Frankfurt am Main, Frankfurt am Main, Tyskland Varighed: 4 sep. 2018 → 6 sep. 2018 Konferencens nummer: 28 http://ppdp-lopstr-18.cs.uni-frankfurt.de/lopstr18.html

Konference

Konference	LOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation
Nummer	28
Lokation	Göthe-University Frankfurt am Main
Land	Tyskland
By	Frankfurt am Main
Periode	04/09/2018 → 06/09/2018
Internetadresse	http://ppdp-lopstr-18.cs.uni-frankfurt.de/lopstr18.html

Navn	Lecture Notes in Computer Science
Vol/bind	11408
ISSN	0302-9743

Navn	Theoretical Computer Science and General Issues
Vol/bind	11408

Emneord

Constraint Handling Rules
Confluence
Confluence modulo equivalence
Invariants
Observable confluence

Link til dokument

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

https://link.springer.com/content/pdf/10.1007%2F978-3-030-13838-7_6.pdf

Citer dette

Christiansen, H., & Kirkeby, M. H. (2019). Confluence of CHR Revisited: Invariants and Modulo Equivalence. I F. Mesnard, & P. J. Stuckey (red.), Logic-Based Program Synthesis and Transformation: 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers (Bind 11408, s. 94-111). Springer. Lecture Notes in Computer Science Bind 11408 Theoretical Computer Science and General Issues Bind 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. red. / Fred Mesnard ; Peter J. Stuckey. Bind 11408 Cham : Springer, 2019. s. 94-111 (Lecture Notes in Computer Science, Bind 11408). (Theoretical Computer Science and General Issues, Bind 11408).

@inproceedings{fbbbcb9aafe745de8fadadaa7026456f,

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",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "94--111",

editor = "Fred Mesnard and Stuckey, {Peter J.}",

booktitle = "Logic-Based Program Synthesis and Transformation",

note = "null ; Conference date: 04-09-2018 Through 06-09-2018",

url = "http://ppdp-lopstr-18.cs.uni-frankfurt.de/lopstr18.html",

}

Christiansen, H & Kirkeby, MH 2019, Confluence of CHR Revisited: Invariants and Modulo Equivalence. i F Mesnard & PJ Stuckey (red), Logic-Based Program Synthesis and Transformation: 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers. bind 11408, Springer, Cham, Lecture Notes in Computer Science, bind 11408, Theoretical Computer Science and General Issues, bind 11408, s. 94-111, LOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation, Frankfurt am Main, Tyskland, 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. red. / Fred Mesnard; Peter J. Stuckey. Bind 11408 Cham : Springer, 2019. s. 94-111 (Lecture Notes in Computer Science, Bind 11408). (Theoretical Computer Science and General Issues, Bind 11408).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - Confluence of CHR Revisited

AU - Christiansen, Henning

AU - Kirkeby, Maja Hanne

N1 - Conference code: 28

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

T3 - Lecture Notes in Computer Science

SP - 94

EP - 111

BT - Logic-Based Program Synthesis and Transformation

A2 - Mesnard, Fred

A2 - Stuckey, Peter J.

PB - Springer

CY - Cham

Y2 - 4 September 2018 through 6 September 2018

ER -

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