Logics for Categorical Systems Theory [lcc-003J]

What sort of logic can we use for reasoning about open dynamical systems in the style of Categorical Systems Theory?

One idea would be to attempt to use some form of modal logic. It is tempting to try to see if we can draw on the connection between modal logic and coalgebra (Modal logics and coalgebra). However, while we can sometimes concoct a functor so that its coalgebras are precisely the open systems of a given signature, this is far from always the case.

Another question here is how this logic should interact with the change-of-interface functors, or with the compositional structure of categorical systems theory in general.

In terms of modal or temporal logic, the interpretation of a formula should be a subobject of the state space. In coalgebras there is a neat thing where a formula is a subset of a cofree coalgebra (this is perhaps easier to think about in the dual case - a system of equations for algebras of T in a set X of variables is the same thing as a quotient of T, namely the quotient obtained by imposing those equations). This seems like a promising starting point for building up a modal logic for categorical systems theory.

On the other hand, it may be interesting to apply the ideas of monoidal Hoare logic to the monoidal categories of controlled cybernetic processes. This may be of interest for control theory - we can reason about the control guarantees implied by a process. It may even be possible to combine the two approaches.