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.
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
PublisherComputer Science, Roskilde University
Volume153
Number of pages20
StatePublished - 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]. Computer Science, Roskilde University. 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]. Computer Science, Roskilde University, 2018. 20 p. (Roskilde Universitet. Computer Science. Computer Science Research Report, ???volume??? 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",
author = "Henning Christiansen and Kirkeby, {Maja Hanne}",
year = "2018",
month = "10",
day = "3",
language = "English",
volume = "153",
publisher = "Computer Science, Roskilde University",

}

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, Computer Science, Roskilde University.

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

Computer Science, Roskilde University, 2018. 20 p.

Research output: Book/ReportReportResearch

TY - RPRT

T1 - Confluence of CHR revisited: 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

M3 - Report

VL - 153

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

PB - Computer Science, Roskilde University

ER -

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