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.
Original language | English |
---|---|
Title of host publication | Logic-Based Program Synthesis and Transformation : 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers |
Editors | Fred Mesnard, Peter J. Stuckey |
Volume | 11408 |
Place of Publication | Cham |
Publisher | Springer |
Publication date | 2019 |
Pages | 94-111 |
ISBN (Print) | 978-3-030-13837-0 |
ISBN (Electronic) | 978-3-030-13838-7 |
DOIs | |
Publication status | Published - 2019 |
Event | LOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation - Göthe-University Frankfurt am Main, Frankfurt am Main, Germany Duration: 4 Sep 2018 → 6 Sep 2018 Conference number: 28 http://ppdp-lopstr-18.cs.uni-frankfurt.de/lopstr18.html |
Conference
Conference | LOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation |
---|---|
Number | 28 |
Location | Göthe-University Frankfurt am Main |
Country/Territory | Germany |
City | Frankfurt am Main |
Period | 04/09/2018 → 06/09/2018 |
Internet address |
Series | Lecture Notes in Computer Science |
---|---|
Volume | 11408 |
ISSN | 0302-9743 |
Series | Theoretical Computer Science and General Issues |
---|---|
Volume | 11408 |
Keywords
- Constraint Handling Rules
- Confluence
- Confluence modulo equivalence
- Invariants
- Observable confluence