Zero dynamics attacks (ZDAs) have received considerable attention in the control systems literature, as they can be disruptive while being almost virtually to detect from the measured output of the plant. However, as ZDAs require an unbounded input sequence, the effect of physical constraints on the actuators, in the form of saturation, must be taken into account. In this work, we show that conventional methods for constructing ZDAs, when subject to input saturation, can make these attacks no longer disruptive, stealthy, or both. While this might imply that some systems are safe from ZDAs, we introduced a new attack called a relaxed ZDA, which can be disruptive and practically stealthy even under input constraints. For the construction of relaxed ZDAs, we propose a method that involves solving an optimization problem offline. We demonstrate the versatility of the proposed method and show it succeeds where conventional ZDAs fall short by means of an illustrative example on a cyber-physical system (CPS).

We introduce a framework for the control of discrete-time switched stochastic systems with uncertain distributions. In particular, we consider stochastic dynamics with additive noise whose distribution lies in an ambiguity set of distributions that are epsilon - close, in the Wasserstein distance sense, to a nominal one. We propose algorithms for the efficient synthesis of distributionally robust control strategies that maximize the satisfaction probability of reach-avoid specifications with either a given or an arbitrary (not specified) time horizon, i.e., unbounded-time reachability. The framework consists of two main steps: finite abstraction and control synthesis. First, we construct a finite abstraction of the switched stochastic system as a robust Markov decision process (robust MDP) that encompasses both the stochasticity of the system and the uncertainty in the noise distribution. Then, we synthesize a strategy that is robust to the distributional uncertainty on the resulting robust MDP. We employ techniques from optimal transport and stochastic programming to reduce the strategy synthesis problem to a set of linear programs, and propose a tailored and efficient algorithm to solve them. The resulting strategies are correctly refined into switching strategies for the original stochastic system. We illustrate the efficacy of our framework on various case studies comprising both linear and non-linear switched stochastic systems.

Model-based fault detection identifies anomalies by comparing a system’s output with the prediction from a model. Although such a technique can be very powerful, it may suffer from the computational complexity of its underlying models, especially for large systems. An alternative approach that circumvents this cost increase uses barrier functions, which abstract the system’s behaviour into a single value. In this paper, we propose a fault detection mechanism via output-based barrier functions, that does not require to estimate the full state, copes with noisy processes, and is tailored to safety-critical faults as given by a user-defined safe region. We leverage such a mechanism by introducing so-called p-fault tolerant sets, which guarantee that a faulty system requires at least p time steps before reaching any unsafe state. Our approach is validated through numerical experiments on two systems with linear and nonlinear dynamics, along with the classic three-tank model.

In this paper we study the problem of designing event-triggering conditions for linear periodic discrete-time systems. Our design satisfies the so-called non-triviality property, a discrete-time version of the Zeno-free property, and enforces triggering events to be separated at least by two sampling periods. We propose a multirate event-based controller in which trigger checking and control update are performed at different rates, which serves to capture the intersampling behaviour. Two different architectures are proposed based on the lifting-based approach where the original periodic system is isomorphically lifted to a higher order LTI one. Finally, the efficiency of the proposed methods is illustrated through a numerical example.

In this paper, we present a novel framework to synthesize robust strategies for discrete-time nonlinear systems with random disturbances that are unknown, against temporal logic specifications. The proposed framework is data-driven and abstraction-based: leveraging observations of the system, our approach learns a high-confidence abstraction of the system in the form of an uncertain Markov decision process (UMDP). The uncertainty in the resulting UMDP is used to formally account for both the error in abstracting the system and for the uncertainty coming from the data. Critically, we show that for any given state-action pair in the resulting UMDP, the uncertainty in the transition probabilities can be represented as a convex polytope obtained by a two-layer state discretization and concentration inequalities. This allows us to obtain tighter uncertainty estimates compared to existing approaches, and guarantees efficiency, as we tailor a synthesis algorithm exploiting the structure of this UMDP. We empirically validate our approach on several case studies, showing substantially improved performance compared to the state-of-the-art.

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.

We propose a novel cyber-attack detection scheme for control schemes regulated via Stochastic Event-Triggered Control, to detect packets that are maliciously injected by an adversary. The diagnosis scheme relies on assessing whether the arrival time of the information packets received from the controller are compatible with the nominal probability distribution of triggering, or whether they are anomalous. To contrast the threat of an eavesdropping adversary capable of estimating the nominal triggering distribution, we propose a switching scheme, whereby the probability of triggering is drawn among a set of stochastic triggering mechanisms, which is such that the reconstruction of the communication pattern by an eavesdropper becomes computationally infeasible. We design the set of stochastic triggering mechanisms via the solution of an optimization problem, which embeds an explicit trade-off between the properties of the nominal Stochastic Event-Triggered Controller and the detection scheme. The results are illustrated through a numerical example.

We propose a novel watermarking scheme by modifying a self-triggered control (STC) policy, aimed at detecting replay attacks for linear time-invariant (LTI) systems. We show that by employing non-deterministic early triggering of the STC mechanism, replay attacks can be detected by a modified chi(2) detector which takes into account the aperiodic nature of the inter-sample times. Specifically, we consider the case where a periodic reference signal is tracked, which makes these systems vulnerable to replay attacks. The proposed approach is modular and can be retrofitted to legacy systems. An approach for designing an online optimal early triggering mechanism is provided. This is validated through an illustrative numerical example in which we compare our method to scenarios employing both additive and multiplicative watermarking.

Policy robustness in Reinforcement Learning may not be desirable at any cost: the alterations caused by robustness requirements from otherwise optimal policies should be explainable, quantifiable and formally verifiable. In this work we study how policies can be maximally robust to arbitrary observational noise by analysing how they are altered by this noise through a stochastic linear operator interpretation of the disturbances, and establish connections between robustness and properties of the noise kernel and of the underlying MDPs. Then, we construct sufficient conditions for policy robustness, and propose a robustness-inducing scheme, applicable to any policy gradient algorithm, that formally trades off expected policy utility for robustness through lexicographic optimisation, while preserving convergence and sub-optimality in the policy synthesis.

The abstraction of dynamical systems is a powerful tool that enables the design of feedback controllers using a correct-by-design framework. We investigate a novel scheme to obtain data-driven abstractions of discrete-time stochastic processes in terms of richer discrete stochastic models, whose actions lead to nondeterministic transitions over the space of probability measures. The data-driven component of the proposed methodology lies in the fact that we only assume samples from an unknown probability distribution. We also rely on the model of the underlying dynamics to build our abstraction through backward reachability computations. The nondeterminism in the probability space is captured by a collection of Markov Processes, and we identify how this model can improve upon existing abstraction techniques in terms of satisfying temporal properties, such as safety or reach-avoid. The connection between the discrete and the underlying dynamics is made formal through the use of the scenario approach theory. Numerical experiments illustrate the advantages and main limitations of the proposed techniques with respect to existing approaches.

The abstraction of dynamical systems is a powerful tool that enables the design of feedback controllers using a correct-by-design framework. We investigate a novel scheme to obtain data-driven abstractions of discrete-time stochastic processes in terms of richer discrete stochastic models, whose actions lead to nondeterministic transitions over the space of probability measures. The data-driven component of the proposed methodology lies in the fact that we only assume samples from an unknown probability distribution. We also rely on the model of the underlying dynamics to build our abstraction through backward reachability computations. The nondeterminism in the probability space is captured by a collection of Markov Processes, and we identify how this model can improve upon existing abstraction techniques in terms of satisfying temporal properties, such as safety or reach-avoid. The connection between the discrete and the underlying dynamics is made formal through the use of the scenario approach theory. Numerical experiments illustrate the advantages and main limitations of the proposed techniques with respect to existing approaches.

Verification of uncertain, complex dynamical systems is crucial in the modern day world. An increasingly common method to verify complex logic specifications for dynamical systems involves symbolic abstractions: simpler, finite-state models whose behaviour mimics the one of the systems of interest. By sampling trajectories of the concrete, unknown system and via robust analysis, we build a data-driven abstraction, related to the underlying model through a probabilistic behavioural inclusion relation. As the distribution from which the trajectories are drawn is unknown, we adopt two distinct distribution-free theories, namely scenario optimization and conformal prediction. We compare and discuss the differences between the two approaches in terms of the type of guarantees that they are able to provide. Furthermore, via experimental benchmarks we outline the efficiency of the two methods with respect to the number of samples available and the tightness of the guarantees.

At the intersection of dynamical systems, control theory, and formal methods lies the construction of symbolic abstractions: these typically represent simpler, finite-state models whose behavior mimics that of an underlying concrete system but are easier to analyse. Building an abstraction usually requires an accurate knowledge of the underlying model: this knowledge may be costly to gather, especially in real-life applications. We aim to bridge this gap by building abstractions based on sampling finite length trajectories. To refine a controller built for the abstraction to one for the concrete system, we newly define a notion of probabilistic alternating simulation, and provide Probably Approximately Correct (PAC) guarantees that the constructed abstraction includes all behaviors of the concrete system and that it is suitable for control design, for arbitrarily long time horizons, leveraging scenario theory. Our method is then tested on several numerical benchmarks.

We study the problem of identifying a linear time-varying output map from measurements and linear time-varying system states, which are perturbed with Gaussian observation noise and process uncertainty, respectively. Employing a stochastic model as prior knowledge for the parameters of the unknown output map, we reconstruct their estimates from input/output pairs via a Bayesian approach to optimize the posterior probability density of the output map parameters. The resulting problem is a non-convex optimization, for which we propose a tractable linear matrix inequalities approximation to warm-start a first-order subsequent method. The efficacy of our algorithm is shown experimentally against classical Expectation Maximization and Dual Kalman Smoother approaches.

Analyzing Event-Triggered Control's (ETC) sampling behaviour is of paramount importance, as it enables formal assessment of its sampling performance and prediction of its sampling patterns. In this work, we formally analyze the sampling behaviour of stochastic linear periodic ETC (PETC) systems by computing bounds on associated metrics. Specifically, we consider functions over sequences of state measurements and intersampling times that can be expressed as average, multiplicative or cumulative rewards, and introduce their expectations as metrics on PETC's sampling behaviour. We compute bounds on these expectations, by constructing appropriate Interval Markov Chains equipped with suitable reward structures, that abstract stochastic PETC's sampling behaviour. Our results are illustrated on a numerical example, for which we compute bounds on the expected average intersampling time and on the probability of triggering with the maximum possible intersampling time in a finite horizon.

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.

Scheduling communication traffic in networks of event-triggered control (ETC) systems is challenging, as their sampling times are unknown, hindering application of ETC in networks. In previous work, finite-state abstractions were created, capturing the sampling behavior of linear time-invariant (LTI) ETC systems with quadratic triggering functions. Offering an infinite-horizon look to ETC systems' sampling patterns, such abstractions can be used for scheduling of ETC traffic. Here, we significantly extend this framework, by abstracting perturbed uncertain nonlinear ETC systems with general triggering functions. To construct an ETC system's abstraction: 1) the state space is partitioned into regions; 2) for each region, an interval is determined, containing all intersampling times of points in the region; and 3) the abstraction's transitions are determined through reachability analysis. To determine intervals and transitions, we devise algorithms based on reachability analysis. For partitioning, we propose an approach based on isochronous manifolds, resulting into tighter intervals and providing control over them, thus containing the abstraction's nondeterminism. Simulations showcase our developments.

We introduce a novel approach for the construction of symbolic abstractions - simpler, finite-state models - which mimic the behaviour of a system of interest, and are commonly utilized to verify complex logic specifications. Such abstractions require an exhaustive knowledge of the concrete model, which can be difficult to obtain in real-world applications. To overcome this, we propose to sample finite length trajectories of an unknown system and build an abstraction based on the concept of $\ell $ -completeness. To this end, we introduce the notion of probabilistic behavioural inclusion. We provide probably approximately correct (PAC) guarantees that such an abstraction, constructed from experimental symbolic trajectories of finite length, includes all behaviours of the concrete system, for both finite and infinite time horizon. Finally, our method is displayed with numerical examples.

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future (Until, U) and the past (Since, S) modalities are used (denoted by MTL[U,S] and TPTL[U,S]). In a classical result, the satisfiability checking for Metric Interval Temporal Logic (MITL[ U,S]), a non-punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. A straightforward adoption of non-punctuality does not recover decidability in the case of TPTL[U,S]. Hence, we propose a more refined notion called non-adjacency for TPTL[U,S] and focus on its 1-variable fragment, 1-TPTL[U,S]. We show that non-adjacent 1-TPTL[U,S] is strictly more expressive than MITL. As one of our main results, we show that the satisfiability checking problem for non-adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity. Our decidability proof relies on a novel technique of anchored interval word abstraction and its reduction to a non-adjacent version of the newly proposed logic called PnEMTL. We further propose an extension of MSO [<] (Monadic Second Order Logic of Orders) with Guarded Metric Quantifiers (GQMSO) and show that it characterizes the expressiveness of PnEMTL. That apart, we introduce the notion of non-adjacency in the context of GQMSO (NA-GQMSO), which is a syntactic generalization of logic Q2MLO due to Hirshfeld and Rabinovich and show the decidability of satisfiability checking for NA-GQMSO.