Binary multirelations form a model of alternating nondeterminism useful for analysing games, interactions of computing systems with their environments or abstract interpretations of probabilistic programs. We investigate this alternating structure with inner or demonic and outer or angelic choices in a relation-algebraic language extended with specific operations on multirelations that relate to the inner layer of alternation.

Abstract We formalize the modal operators from the concurrent dynamic logics of Peleg, Nerode and Wijesekera in a multirelational algebraic language based on relation algebras and power allegories, using relational approximation operators on multirelations developed in a companion article. We relate Nerode and Wijesekera’s box operator with a relational approximation operator for multirelations and two related operators that approximate multirelations by different kinds of deterministic multirelations. We provide an algebraic soundness proof of Goldblatt’s axioms for concurrent dynamic logic and one for a multirelational Hoare logic based on Nerode and Wijesekera’s box as applications.

Previous work has axiomatised the cardinality operation in relation algebras, which counts the number of edges of an unweighted graph. We generalise the cardinality axioms to Stone relation algebras, which model weighted graphs, and study the relationships between various axioms for cardinality. This results in simpler cardinality axioms also for relation algebras. We give sufficient conditions for the representability of Stone relation algebras and for Stone relation algebras to be relation algebras. added explanations

This paper studies how to use relation algebras, which are useful for high-level specification and verification, for proving the correctness of lower-level array-based implementations of algorithms. We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in computation models supporting while-programs. As a result, relation algebras can be used for verifying programs with associative arrays. We verify the correctness of an array-based implementation of disjoint-set forests using the union-by-rank strategy and find operations with path compression, path splitting and path halving. All results are formally proved in Isabelle/HOL. This paper is an extended version of [1].

Abstract An equivalence relation can be constructed from a given (homogeneous, binary) relation in two steps: first, construct the smallest reflexive and transitive relation containing the given relation (the “star” of the relation) and, second, construct the largest symmetric relation that is included in the result of the first step. The fact that the final result is also reflexive and transitive (as well as symmetric), and thus an equivalence relation, is not immediately obvious, although straightforward to prove. Rather than prove that the defining properties of reflexivity and transitivity are satisfied, we establish reflexivity and transitivity constructively by exhibiting a starth root—in a way that emphasises the creative process in its construction. The resulting construction is fundamental to algorithms that determine the strongly connected components of a graph as well as the decomposition of a graph into its strongly connected components together with an acyclic graph connecting such components.

Binary multirelations allow modelling alternating nondeterminism, for instance, in games or nondeterministically evolving systems interacting with an environment. Such systems can show partial or total functional behaviour at both levels of alternation, so that nondeterministic behaviour may occur only at one level or both levels, or not at all. We study classes of inner and outer partial and total functional multirelations in a multirelational language based on relation algebra and power allegories. While it is known that general multirelations do not form a category, we show in the multirelational language that the classes of deterministic multirelations mentioned form categories with respect to Peleg composition from concurrent dynamic logic, and sometimes quantaloids. Some of these categories are isomorphic to the category of binary relations. We also introduce determinisation maps that approximate multirelations either by binary relations or by deterministic multirelations. Such maps are useful for defining modal operators on multirelations.