With the increasing ubiquity of safety-critical autonomous systems operating in uncertain environments, there is a need for mathematical methods for formal verification of stochastic models. Towards formally verifying properties of stochastic systems, methods based on discrete, finite Markov approximations - abstractions - thereof have surged in recent years. These are found in contexts where: either a) one only has partial, discrete observations of the underlying continuous stochastic process, or b) the original system is too complex to analyze, so one partitions the continuous state-space of the original system to construct a handleable, finite-state model thereof. In both cases, the abstraction is an approximation of the discrete stochastic process that arises precisely from the discretization of the underlying continuous process. The fact that the abstraction is Markov and the discrete process is not (even though the original one is) leads to approximation errors. Towards accounting for non-Markovianity, we introduce memory-dependent abstractions for stochastic systems, capturing dynamics with memory effects. Our contribution is twofold. First, we provide a formalism for memory-dependent abstractions based on transfer operators. Second, we quantify the approximation error by upper bounding the total variation distance between the true continuous state distribution and its discrete approximation.

Interval Markov Decision Processes (IMDPs) are finite-state uncertain Markov models, where the transition probabilities belong to intervals. Recently, there has been a surge of research on employing IMDPs as abstractions of stochastic systems for control synthesis. However, due to the absence of algorithms for synthesis over IMDPs with continuous action-spaces, the action-space is assumed discrete a-priori, which is a restrictive assumption for many applications. Motivated by this, we introduce continuous-action IMDPs (caIMDPs), where the bounds on transition probabilities are functions of the action variables, and study value iteration for maximizing expected cumulative rewards. Specifically, we decompose the max-min problem associated to value iteration to |𝒬| max problems, where |𝒬| is the number of states of the caIMDP. Then, exploiting the simple form of these max problems, we identify cases where value iteration over caIMDPs can be solved efficiently (e.g., with linear or convex programming). We also gain other interesting insights: e.g., in certain cases where the action set 𝒜 is a polytope, synthesis over a discrete-action IMDP, where the actions are the vertices of 𝒜, is sufficient for optimality. We demonstrate our results on a numerical example. Finally, we include a short discussion on employing caIMDPs as abstractions for control synthesis.

We present ETCetera, a Python library developed for the analysis and synthesis of the sampling behaviour of event triggered control (ETC) systems. In particular, the tool constructs abstractions of the sampling behaviour of given ETC systems, in the form of timed automata (TA) or finite-state transition systems (FSTSs). When the abstraction is an FSTS, ETCetera provides diverse manipulation tools for analysis of ETC’s sampling performance, synthesis of communication traffic schedulers (when networks shared by multiple ETC loops are considered), and optimization of sampling strategies. Additionally, the TA models may be exported to UPPAAL for analysis and synthesis of schedulers. Several examples of the tool’s application for analysis and synthesis problems with different types of dynamics and event-triggered implementations are provided.