# Binary Multirelations

 Title: Binary Multirelations Authors: Hitoshi Furusawa and Georg Struth Submission date: 2015-06-11 Abstract: 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. BibTeX: @article{Multirelations-AFP, author = {Hitoshi Furusawa and Georg Struth}, title = {Binary Multirelations}, journal = {Archive of Formal Proofs}, month = jun, year = 2015, note = {\url{https://isa-afp.org/entries/Multirelations.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Kleene_Algebra Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.