We employ the scenario optimisation theory to compute a traffic abstraction, with probability guarantees of correctness, of a PETC system with unknown dynamics from a finite number of samples. To this end, we extend the scenario optimisation approach to multiclass SVM in order to compute a map between the concrete state space and the intersample times of the PETC. This map allows the construction of a traffic abstraction, through an <inline-formula><tex-math notation="LaTeX">$\ell$</tex-math></inline-formula>-complete relation, that provides upper and lower bounds on the sampling performance of the concrete system. We further propose an alternative path to build such abstraction, first we identify the model and then apply a model-based procedure. Numerical benchmarks show the practical applicability of our methods for noiseless and noisy samples.

We describe a new variant of zero dynamics attack (ZDA), what we call a switched ZDA, targeting linear time-invariant (LTI) sampled-data systems with non-uniform sampling. Specifically, we consider continuous-time systems and construct attacks that exploit the unstable sampling zeros resulting from a zero-order hold (ZOH) mechanism. These attacks can be constructed by strong adversaries who have knowledge of the plant dynamics, with the additional requirement that they can determine the next sampling instant. We provide sufficient conditions when cyber-physical systems are vulnerable to switched ZDAs, and prove that these attacks can be disruptive while remaining stealthy. We also provide two possible countermeasures that make switched ZDAs ineffective. The first countermeasure revolves around creating a mismatch between the next sampling instant as predicted by the adversary and the true one, which makes the switched ZDAs no longer stealthy. The second countermeasure relies on increasing the inter-sample times such that the system no longer contains unstable sampling zeros, making the switched ZDA no longer disruptive. We demonstrate the vulnerability of sampled-data systems with non-uniform sampling to switched ZDAs in several illustrative examples, and exemplify the effectiveness of the proposed countermeasures.

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.

Estimating the expectation of a Bernoulli random variable based on N independent trials is a classical problem in statistics, typically addressed using Binomial Proportion Confidence Intervals (BPCI). In the control systems community, many critical tasks—such as certifying the statistical safety of dynamical systems—can be formulated as BPCI problems. Conformal Prediction (CP), a distribution-free technique for uncertainty quantification, has gained significant attention in recent years and has been applied to various control systems problems, particularly to address uncertainties in learned dynamics or controllers. A variant known as training-conditional CP was recently employed to tackle the problem of safety certification. In this note, we highlight that the use of training-conditional CP in this context does not provide valid safety guarantees. We demonstrate why CP is unsuitable for BPCI problems and argue that traditional BPCI methods are better suited for statistical safety certification.

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.

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 behavior 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 behavior 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 behavior. We compute bounds on these expectations, by constructing Interval Markov Chains equipped with suitable reward functions, that abstract stochastic PETC's sampling behavior. 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.

We present a novel framework for formal control of uncertain discrete-time switched stochastic systems against probabilistic reach-avoid specifications. In particular, we consider stochastic systems with additive noise, whose distribution lies in an ambiguity set of distributions that are ε−close to a nominal one according to the Wasserstein distance. For this class of systems we derive control synthesis algorithms that are robust against all these distributions and maximize the probability of satisfying a reach-avoid specification, defined as the probability of reaching a goal region while being safe. The framework we present first learns an abstraction of a switched stochastic system as a robust Markov decision process (robust MDP) by accounting for both the stochasticity of the system and the uncertainty in the noise distribution. Then, it synthesizes a strategy on the resulting robust MDP that maximizes the probability of satisfying the property and is robust to all uncertainty in the system. This strategy is then refined into a switching strategy for the original stochastic system. By exploiting tools from optimal transport and stochastic programming, we show that synthesizing such a strategy reduces to solving a set of linear programs, thus guaranteeing efficiency. We experimentally validate the efficacy of our framework on various case studies, including both linear and non-linear switched stochastic systems. Our results represent the first formal approach for control synthesis of stochastic systems with uncertain noise distribution.

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.

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 ℓ -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.

We present a biologically inspired design for swarm foraging based on ant’s pheromone deployment, where the swarm is assumed to have very restricted capabilities. The robots do not require global or relative position measurements and the swarm is fully decentralized and needs no infrastructure in place. Additionally, the system only requires one-hop communication over the robot network, we do not make any assumptions about the connectivity of the communication graph and the transmission of information and computation is scalable versus the number of agents. This is done by letting the agents in the swarm act as foragers or as guiding agents (beacons). We present experimental results computed for a swarm of Elisa-3 robots on a simulator, and show how the swarm self-organizes to solve a foraging problem over an unknown environment, converging to trajectories around the shortest path, and test the approach on a real swarm of Elisa-3 robots. At last, we discuss the limitations of such a system and propose how the foraging efficiency can be increased.

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.