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

Publikation: Bog/antologi/afhandling/rapportRapportForskning

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.
OriginalsprogEngelsk
Udgivelses stedRoskilde
ForlagRoskilde Universitet
Vol/bind153
Antal sider20
ISBN (Trykt)0109-9779
StatusUdgivet - 3 okt. 2018
NavnRoskilde Universitet. Computer Science. Computer Science Research Report
Vol/bind153
ISSN0109-9779

Emneord

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

Citer dette

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