We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Algebra of Non-deterministic Programs: Demonic Operations, Orders and Axioms.
- Authors
Hirsch, Robin; Mikulás, Szabolcs; Stokes, Tim
- Abstract
Demonic composition, demonic refinement and demonic union are alternatives to the usual 'angelic' composition, angelic refinement (inclusion) and angelic (usual) union defined on binary relations. We first motivate both the angelic and the demonic via an analysis of the behaviour of non-deterministic programs, with the angelic associated with partial correctness and demonic with total correctness, both cases emerging from a richer algebraic model of non-deterministic programs incorporating both aspects. Zareckiĭ has shown that the isomorphism class of algebras of binary relations under angelic composition and inclusion is finitely axiomatized as the class of ordered semigroups. The proof can be used to establish that the same axiomatization applies to binary relations under demonic composition and refinement, and a further modification of the proof can be used to incorporate a zero element representing the empty relation in the angelic case and the full relation in the demonic case. For the signature of angelic composition and union, it is known that no finite axiomatization exists, and we show the analogous result for demonic composition and demonic union by showing that the same axiomatization holds for both. We show that the isomorphism class of algebras of binary relations with the 'mixed' signature of demonic composition and angelic inclusion has no finite axiomatization. As a contrast, we show that the isomorphism class of partial algebras of binary relations with the partial operation of constellation product and inclusion (also a 'mixed' signature) is finitely axiomatizable.
- Subjects
RELATION algebras; ALGEBRA; BEHAVIORAL assessment
- Publication
Logic Journal of the IGPL, 2022, Vol 30, Issue 5, p886
- ISSN
1367-0751
- Publication type
Article
- DOI
10.1093/jigpal/jzab026