Hirsch, R;
Semrl, J;
(2021)
Demonic Lattices and Semilattices in Relational Semigroups with Ordinary Composition.
In:
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
IEEE: Rome, Italy.
Preview |
Text
2105.06787v1.pdf - Accepted Version Download (212kB) | Preview |
Abstract
Relation algebra and its reducts provide us with a strong tool for reasoning about nondeterministic programs and their partial correctness. Demonic calculus, introduced to model the behaviour of a machine where the demon is in control of nondeterminism, has also provided us with an extension of that reasoning to total correctness.We formalise the framework for relational reasoning about total correctness in nondeterministic programs using semigroups with ordinary composition and demonic lattice operations. We show that the class of representable demonic join semigroups is not finitely axiomatisable and that the representation class of demonic meet semigroups does not have the finite representation property for its finite members.For lattice semigroups (with composition, demonic join and demonic meet) we show that the representation problem for finite algebras is undecidable, moreover the finite representation problem is also undecidable. It follows that the representation class is not finitely axiomatisable, furthermore the finite representation property fails.
| Type: | Proceedings paper |
|---|---|
| Title: | Demonic Lattices and Semilattices in Relational Semigroups with Ordinary Composition |
| Event: | 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
| ISBN-13: | 9781665448956 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1109/LICS52264.2021.9470509 |
| Publisher version: | http://dx.doi.org/10.1109/LICS52264.2021.9470509 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Computer science, Algebra, Lattices, Tools, Cognition, Calculus |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10134909 |
Archive Staff Only
 |
View Item |
