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.
  author  = {Hitoshi Furusawa and Georg Struth},
  title   = {Binary Multirelations},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2015,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Kleene_Algebra