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.
翻译:二元多关系可模拟交替非确定性,例如在博弈或与环境交互的非确定性演化系统中。此类系统在交替的两个层次上可能呈现部分或完全函数行为,使得非确定性行为可能仅出现在一个层次、两个层次或不出现。我们基于关系代数与幂拟范畴的多关系语言,研究内层与外层部分与完全函数多关系的类别。尽管已知一般多关系不能构成范畴,但我们证明所提及的决定性多关系类在并发动态逻辑的Peleg复合下构成范畴(有时构成量词范畴),其中部分范畴与二元关系范畴同构。我们还引入决定化映射,通过二元关系或决定性多关系近似多关系,此类映射对于在多关系上定义模态算子具有实用价值。