Binary Multirelations

Hitoshi Furusawa 🌐 and Georg Struth 🌐

June 11, 2015

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Binary multirelations associate elements of a set with its subsets; hence they are binary relations from a set to its power set. Applications include alternating automata, models and logics for games, program semantics with dual demonic and angelic nondeterministic choices and concurrent dynamic logics. This proof document supports an arXiv article that formalises the basic algebra of multirelations and proposes axiom systems for them, ranging from weak bi-monoids to weak bi-quantales.


BSD License


Session Multirelations

Depends on