Hybrid dynamical systems exhibit a diverse array of stability phenomena, each currently addressed by separate Lyapunov-like results. We show that these results are all instances of a single theorem: a Lyapunov function is a morphism from a hybrid system into a simple stable target system $𝜎$, and different stability notions such as Lyapunov stability, asymptotic stability, exponential stability, and Zeno stability correspond to different choices of $𝜎$. This unification is achieved by expressing hybrid systems as coalgebras of an endofunctor $\mathrm{\mathscr{H}︀}$ on a category $\text{𝖢𝗁𝖺𝗋𝗍}$ that naturally blends continuous and discrete dynamics. Instantiating a general categorical Lyapunov theorem for coalgebras to this setting results in new Lypaunov-like conditions for the stability of Zeno equilibria and the existence of Zeno behavior in hybrid systems.

Assume-guarantee reasoning is a technique for compositional model checking in which system specifications are checked under certain assumptions on system parameters or inputs, and provide guarantees on observations of system state. We present a categorical framework for assume-guarantee reasoning for safety problems by viewing systems as lenses, following our earlier work on the compositionality of generalized Moore machines. Generalized Moore machines include ordinary Moore machines, partially observable Markov (decision) processes, and systems of parameterized ODEs (control systems); our framework gives assume-guarantee reasoning specially adapted to each of these cases. In particular, we give a novel formulation of assume-guarantee reasoning for (local) input-to-state stability ((L)ISS) Lyapunov functions on systems of parameterized ODEs. Our framework is categorically natural and straightforwardly compositional. A flavor of generalized Moore machine is determined by a tangency: a fibration with a section. We show that symmetric monoidal loose right modules of assume-guarantee certified generalized Moore machines over symmetric monoidal double categories of certified wiring diagrams can be constructed 2-functorially from fibrations internal to the 2-category of tangencies.

Quantitative semantics of Signal Temporal Logic (STL) play an important role in both the falsification and control synthesis for dynamical systems by assigning numerical quantities to truth values. Recently, several different quantitative semantics have been proposed, offering better performance in many cases. Yet a general, systematic understanding of the structure and properties of quantitative semantics is missing. In this paper, we develop a general framework to model quantitative semantics. We focus mainly on soundness, which requires that the quantitative semantics of a statement is positive when the statement is true, and negative when the statement is false. This ensures that counterexamples will not be missed during verification. We derive simple, necessary conditions in our framework for soundness. We show how several recently proposed quantitative semantics fit in our framework, and how others do not, typically because they do not strictly satisfy soundness. We implement various quantitative semantics, including existing semantics from literature, in our framework and compare their effectiveness as objective functions for optimization-based falsification on both novel and existing benchmarks.

Lyapunov’s theorem provides a foundational characterization of stable equilibrium points in dynamical systems. In this paper, we develop a framework for stability for F-coalgebras. We give two definitions for a categorical setting in which we can study the stability of a coalgebra for an endofunctor F. One is minimal and better suited for concrete settings, while the other is more intricate and provides a richer theory. We prove a Lyapunov theorem for both notions of setting for stability, and a converse Lyapunov theorem for the second.

Lyapunov’s theorem provides a fundamental characterization of the stability of dynamical systems. This paper presents a categorical framework for Lyapunov theory, generalizing stability analysis with Lyapunov functions categorically. Core to our approach is the set of axioms underlying a setting for stability, which give the necessary ingredients for “doing Lyapunov theory” in a category of interest. With these minimal assumptions, we define the stability of equilibria, formulate Lyapunov morphisms, and demonstrate that the existence of Lyapunov morphisms is necessary and sufficient for establishing the stability of flows. To illustrate these constructions, we show how classical notions of stability, e.g., for continuous and discrete time dynamical systems, are captured by this categorical framework for Lyapunov theory. Finally, to demonstrate the extensibility of our framework, we illustrate how enriched categories, e.g., Lawvere metric spaces, yield settings for stability enabling one to “do Lyapunov theory” in enriched categories.

The internal model principle, originally proposed in the theory of control of linear systems, nowadays represents a more general class of results in control theory and cybernetics. The central claim of these results is that, under suitable assumptions, if a system (a controller) can regulate against a class of external inputs (from the environment), it is because the system contains a model of the system causing these inputs, which can be used to generate signals counteracting them. Similar claims on the role of internal models appear also in cognitive science, especially in modern Bayesian treatments of cognitive agents, often suggesting that a system (a human subject, or some other agent) models its environment to adapt against disturbances and perform goal-directed behaviour. It is however unclear whether the Bayesian internal models discussed in cognitive science bear any formal relation to the internal models invoked in standard treatments of control theory. Here, we first review the internal model principle and present a precise formulation of it using concepts inspired by categorical systems theory. This leads to a formal definition of “model” generalising its use in the internal model principle. Although this notion of model is not a priori related to the notion of Bayesian reasoning, we show that it can be seen as a special case of possibilistic Bayesian filtering. This result is based on a recent line of work formalising, using Markov categories, a notion of “interpretation”, describing when a system can be interpreted as performing Bayesian filtering on an outside world in a consistent way.

Avoiding collisions between obstacles and vehicles such as cars, robots or aircraft is essential to the development of automation and autonomy. To simplify the problem, many collision avoidance algorithms and proofs consider vehicles to be a point mass, though the actual vehicles are not points. In this paper, we consider a convex polygonal vehicle with nonzero area traveling along a 2-dimensional trajectory. We derive an easily-checkable, quantifier-free formula to check whether a given obstacle will collide with the vehicle moving on the planned trajectory. We apply our method to two case studies of aircraft collision avoidance and study its performance.