Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]

Research output: Book/ReportReportResearch

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 Handling 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.
LanguageEnglish
Place of PublicationRoskilde
PublisherRoskilde Universitet
Volume153
Number of pages20
ISBN (Print)0109-9779
Publication statusPublished - 3 Oct 2018
SeriesRoskilde Universitet. Computer Science. Computer Science Research Report
Volume153
ISSN0109-9779

Keywords

  • confluence
  • constraint handling rules
  • observable confluence modulo equivalence; confluence modulo equivalence
  • invariants
  • equivalence

Cite this

Christiansen, H., & Kirkeby, M. H. (2018). Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]. Roskilde: Roskilde Universitet. Roskilde Universitet. Computer Science. Computer Science Research Report, Vol.. 153
Christiansen, Henning ; Kirkeby, Maja Hanne. / Confluence of CHR revisited : invariants and modulo equivalence [Extended version with proofs]. Roskilde : Roskilde Universitet, 2018. 20 p. (Roskilde Universitet. Computer Science. Computer Science Research Report, Vol. 153).
@book{3ebc1c4a5d4348beb79a5d6836e8f255,
title = "Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]",
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 Handling 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 = "confluence, constraint handling rules, observable confluence modulo equivalence; confluence modulo equivalence, invariants, equivalence, confluence, constraint handling rules, observable confluence modulo equivalence; confluence modulo equivalence, invariants, equivalence",
author = "Henning Christiansen and Kirkeby, {Maja Hanne}",
year = "2018",
month = "10",
day = "3",
language = "English",
isbn = "0109-9779",
volume = "153",
publisher = "Roskilde Universitet",

}

Christiansen, H & Kirkeby, MH 2018, Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]. Roskilde Universitet. Computer Science. Computer Science Research Report, vol. 153, vol. 153, Roskilde Universitet, Roskilde.

Confluence of CHR revisited : invariants and modulo equivalence [Extended version with proofs]. / Christiansen, Henning; Kirkeby, Maja Hanne.

Roskilde : Roskilde Universitet, 2018. 20 p.

Research output: Book/ReportReportResearch

TY - RPRT

T1 - Confluence of CHR revisited

T2 - invariants and modulo equivalence [Extended version with proofs]

AU - Christiansen, Henning

AU - Kirkeby, Maja Hanne

PY - 2018/10/3

Y1 - 2018/10/3

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 Handling 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 Handling 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 - confluence

KW - constraint handling rules

KW - observable confluence modulo equivalence; confluence modulo equivalence

KW - invariants

KW - equivalence

KW - confluence

KW - constraint handling rules

KW - observable confluence modulo equivalence; confluence modulo equivalence

KW - invariants

KW - equivalence

M3 - Report

SN - 0109-9779

VL - 153

BT - Confluence of CHR revisited

PB - Roskilde Universitet

CY - Roskilde

ER -

Christiansen H, Kirkeby MH. Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]. Roskilde: Roskilde Universitet, 2018. 20 p. (Roskilde Universitet. Computer Science. Computer Science Research Report, Vol. 153).