### 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.

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.

Original language | English |
---|

Place of Publication | Roskilde |
---|---|

Publisher | Roskilde Universitet |

Volume | 153 |

Number of pages | 20 |

ISBN (Print) | 0109-9779 |

Publication status | Published - 3 Oct 2018 |

Series | Roskilde Universitet. Computer Science. Computer Science Research Report |
---|---|

Volume | 153 |

ISSN | 0109-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 Universitet. Roskilde Universitet. Computer Science. Computer Science Research Report, Vol.. 153