Confluence of CHR revisited: invariants and modulo equivalence

TL;DR

This paper introduces an abstract simulation approach to prove confluence under invariants and modulo equivalence in transition systems, extending classical results for Constraint Handling Rules (CHR) to more general cases.

Contribution

It develops a novel abstract simulation method that simplifies confluence proofs under invariants and modulo equivalence, broadening the applicability of CHR confluence results.

Findings

Extended confluence results to include invariants and modulo equivalence

Reduced proof complexity from infinite to finite cases

Validated approach with classical CHR confluence as a special case

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.