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 HThe invariant is formalizedandling 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.
Originalsprog | Engelsk |
---|---|
Titel | Logic-Based Program Synthesis and Transformation : 28th International.Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers |
Redaktører | Fred Mesnard, Peter J. Stuckey |
Antal sider | 18 |
Vol/bind | 11408 |
Udgivelsessted | Cham |
Forlag | Springer |
Publikationsdato | 2019 |
Sider | 94-111 |
ISBN (Trykt) | 978-3-030-13837-0 |
ISBN (Elektronisk) | 978-3-030-13838-7 |
DOI | |
Status | Udgivet - 2019 |
Begivenhed | LOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation - Göthe-University Frankfurt am Main, Frankfurt am Main, Tyskland Varighed: 4 sep. 2018 → 6 sep. 2018 Konferencens nummer: 28 http://ppdp-lopstr-18.cs.uni-frankfurt.de/lopstr18.html |
Konference
Konference | LOPSTR 2018 -28th International Symposium on Logic-Based Program Synthesis and Transformation |
---|---|
Nummer | 28 |
Lokation | Göthe-University Frankfurt am Main |
Land/Område | Tyskland |
By | Frankfurt am Main |
Periode | 04/09/2018 → 06/09/2018 |
Internetadresse |
Navn | Lecture Notes in Computer Science |
---|---|
Vol/bind | 11408 |
ISSN | 0302-9743 |
Navn | Theoretical Computer Science and General Issues |
---|---|
Vol/bind | 11408 |
Emneord
- Constraint Handling Rules
- Confluence
- Confluence modulo equivalence
- Invariants
- Observable confluence