Nondeterministic Behaviours in Double Categorical Systems Theory
Paul Zhongpeng Wang
TL;DR
This work develops a double-categorical framework for nondeterministic systems using Markov categories with conditionals, aiming to faithfully model trajectories as joint time-indexed distributions rather than per-step marginals. The authors construct semimodules of systems, $T^{\mathrm{Moore}}(\mathcal{C}, \mathcal{G})$, for a Markov category $\mathcal{C}$ and a time graph $\mathcal{G}$, by building semi triple arenas $Arena^{\mathrm{Moore}}_{\mathcal{C}}$ and $ArenaSys^{\mathrm{Moore}}_{\mathcal{C}}(\mathcal{G})$ and proving a main existence theorem (Theorem) via a detailed construction. Trajectories are realized as compatible families of Markov morphisms, with time modeled through $\mathcal{G}$ and conditional products providing joint distributions for composed subsystems. The framework handles nondeterministic updates on states/inputs while keeping channels between interfaces deterministic, enforcing associativity via copy-composition and ensuring interchange through conditional products. This approach advances compositional modelling of nondeterministic systems and offers a path toward time-aware, modular system theories with potential extensions to continuous time and richer conditioning regimes.
Abstract
In this paper, we build double theories capturing the idea of nondeterministic behaviors and trajectories. Following Libkind and Myers' Double Operadic Theory of Systems, we construct monoidal semi double categories of interfaces, along with what we call semimodules of systems, in the case of Moore machines, working with Markov categories with conditionals to handle nondeterminism. We use conditional products in these Markov categories to define trajectories in a compositional way, and represent nondeterministic systems using Markov maps; channels between systems are assumed to be deterministic.