How to Stay Locally Safe in a Global World (Part I: Introduction)

Suppose your name is $ x$ and you have a very important state machine $ N_x : S_x \times \Sigma \to \mathcal{P}(S_x)$ that you cherish with all your heart. Because you love this state machine so much, you don't want it to malfunction and you have a subset $ P \subseteq S_x$ which you consider to be safe. If your state machine ever leaves this safe space you are in big trouble so you ask the following question. If you start in some subset $ I \subseteq P$ will your state machine $ N_x$ ever leave $ P$? In math, you ask if

$ \mu (\blacksquare(-) \cup I) \subseteq P$

where $ \mu$ is the least fixed point and $ \blacksquare(-)$ indicates the next-time operator of the cherished state machine. What is the next-time operator?

Definition: For a function $ N : X \times \Sigma \to \mathcal{P}(Y)$ there is a monotone function $ \blacksquare_N : \mathcal{P}(X) \to \mathcal{P}(Y)$ given by

$ \blacksquare_N(A) = \bigcup_{a \in A} \bigcup_{s \in \Sigma} N(a,s)$

In layspeak the next-time operator sends a set of states the set of all possible successors of those states.

In a perfect world you could use these definitions to ensure safety using the formula

$ \mu (\blacksquare(-) \cup I) = \bigcup_{n=0}^{\infty} (\blacksquare ( - ) \cup I)^n$

or at least check safety up to an arbitrary time-step $ n$ by computing this infinite union one step at a time.

Unfortunately there is a big problem with this method! Your state machine does not exist in isolation. You have a friend whose name is $ y$ with their own state machine $ N_y : S_y \times \Sigma \to \mathcal{P} (S_y)$. $ y$ has the personal freedom to run their state machine how they like but there are functions

$ N_{xy} : S_x \times \Sigma \to \mathcal{P}(S_y)$ and $ N_{yx} : S_y \times \Sigma \to \mathcal{P}(S_x)$

which allow states of your friend's machine to change the states of your own and vice-versa. Making matters worse, there is a whole graph $ G$ whose vertices are your friends and whose edges indicate that the corresponding state machines may effect each other. How can you be expected to ensure safety under these conditions?

But don't worry, category theory comes to the rescue. In the next two posts I will:

1. State my model of the world and the local-to-global safety problem for this model (Part II)
2. Propose a solution to the local-to-global safety problem based on an enriched version of the Grothendieck construction (Part III)

I won't have time to explain exactly which enriched Grothendieck construction this is or even prove that my solution is correct. This will be left to future work so stay tuned.