Binary multirelations can model 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 that the classes of deterministic multirelations mentioned form categories with respect to Peleg composition from concurrent dynamic logic, and sometimes quantaloids. Some of these 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.
翻译:二元多关系可以模拟交替非确定性,例如在博弈或与环境交互的非确定性演化系统中。此类系统在交替的两个层级上可能表现出部分或完全的功能性行为,因此非确定性行为可能仅出现在一个层级、两个层级或完全不出现。我们基于关系代数和幂范畴(power allegories)的多关系语言,研究了内、外部分及完全功能多关系的类别。尽管已知一般多关系不构成范畴,但我们证明了上述确定性多关系类别在并发动态逻辑的Peleg复合下构成范畴,有时还构成量子态(quantaloids)。其中某些范畴与二元关系范畴同构。此外,我们引入了确定性映射,用于通过二元关系或确定性多关系近似多关系。此类映射对定义多关系上的模态算子具有实用价值。