Majid Zamani

Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar et al.

Symbolic approaches to the control design over complex systems employ the construction of finite-state models that are related to the original control systems, then use techniques from finite-state synthesis to compute controllers satisfying specifications given in a temporal logic, and finally translate the synthesized schemes back as controllers for the concrete complex systems. Such approaches have been successfully developed and implemented for the synthesis of controllers over non-probabilistic control systems. In this paper, we extend the technique to probabilistic control systems modeled by controlled stochastic differential equations. We show that for every stochastic control system satisfying a probabilistic variant of incremental input-to-state stability, and for every given precision $\varepsilon>0$, a finite-state transition system can be constructed, which is $\varepsilon$-approximately bisimilar (in the sense of moments) to the original stochastic control system. Moreover, we provide results relating stochastic control systems to their corresponding finite-state transition systems in terms of probabilistic bisimulation relations known in the literature. We demonstrate the effectiveness of the construction by synthesizing controllers for stochastic control systems over rich specifications expressed in linear temporal logic. The discussed technique enables a new, automated, correct-by-construction controller synthesis approach for stochastic control systems, which are common mathematical models employed in many safety critical systems subject to structured uncertainty and are thus relevant for cyber-physical applications.

Majid Zamani, Murat Arcak

In this paper we propose a compositional scheme for the construction of abstractions for networks of control systems using the interconnection matrix and joint dissipativity-type properties of subsystems and their abstractions. In the proposed framework, the abstraction, itself a control system (possibly with a lower dimension), can be used as a substitution of the original system in the controller design process. Moreover, we provide a procedure for constructing abstractions of a class of nonlinear control systems by using the bounds on the slope of system nonlinearities. We illustrate the proposed results on a network of linear control systems by constructing its abstraction in a compositional way without requiring any condition on the number or gains of the subsystems. We use the abstraction as a substitute to synthesize a controller enforcing a certain linear temporal logic specification. This example particularly elucidates the effectiveness of dissipativity-type compositional reasoning for large-scale systems.

Abolfazl Lavaei, Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar et al.

This paper is concerned with a compositional approach for constructing abstractions of interconnected discrete-time stochastic control systems. The abstraction framework is based on new notions of so-called stochastic simulation functions, using which one can quantify the distance between original interconnected stochastic control systems and their abstractions in the probabilistic setting. Accordingly, one can leverage the proposed results to perform analysis and synthesis over abstract interconnected systems, and then carry the results over concrete ones. In the first part of the paper, we derive sufficient small-gain type conditions for the compositional quantification of the distance in probability between the interconnection of stochastic control subsystems and that of their abstractions. In the second part of the paper, we focus on the class of discrete-time linear stochastic control systems with independent noises in the abstract and concrete subsystems. For this class of systems, we propose a computational scheme to construct abstractions together with their corresponding stochastic simulation functions. We demonstrate the effectiveness of the proposed results by constructing an abstraction (totally 4 dimensions) of the interconnection of four discrete-time linear stochastic control subsystems (together 100 dimensions) in a compositional fashion.

Rupak Majumdar, Indranil Saha, Majid Zamani

Software implementations of controllers for physical systems are at the core of many embedded systems. The design of controllers uses the theory of dynamical systems to construct a mathematical control law that ensures that the controlled system has certain properties, such as asymptotic convergence to an equilibrium point, while optimizing some performance criteria. However, owing to quantization errors arising from the use of fixed-point arithmetic, the implementation of this control law can only guarantee practical stability: under the actions of the implementation, the trajectories of the controlled system converge to a bounded set around the equilibrium point, and the size of the bounded set is proportional to the error in the implementation. The problem of verifying whether a controller implementation achieves practical stability for a given bounded set has been studied before. In this paper, we change the emphasis from verification to automatic synthesis. Using synthesis, the need for formal verification can be considerably reduced thereby reducing the design time as well as design cost of embedded control software. We give a methodology and a tool to synthesize embedded control software that is Pareto optimal w.r.t. both performance criteria and practical stability regions. Our technique is a combination of static analysis to estimate quantization errors for specific controller implementations and stochastic local search over the space of possible controllers using particle swarm optimization. The effectiveness of our technique is illustrated using examples of various standard control systems: in most examples, we achieve controllers with close LQR-LQG performance but with implementation errors, hence regions of practical stability, several times as small.

Matthias Rungger, Majid Zamani

We consider a compositional construction of approximate abstractions of interconnected control systems. In our framework, an abstraction acts as a substitute in the controller design process and is itself a continuous control system. The abstraction is related to the concrete control system via a so-called simulation function: a Lyapunov-like function, which is used to establish a quantitative bound between the behavior of the approximate abstraction and the concrete system. In the first part of the paper, we provide a small gain type condition that facilitates the compositional construction of an abstraction of an interconnected control system together with a simulation function from the abstractions and simulation functions of the individual subsystems. In the second part of the paper, we restrict our attention to linear control system and characterize simulation functions in terms of controlled invariant, externally stabilizable subspaces. Based on those characterizations, we propose a particular scheme to construct abstractions for linear control systems. We illustrate the compositional construction of an abstraction on an interconnected system consisting of four linear subsystems. We use the abstraction as a substitute to synthesize a controller to enforce a certain linear temporal logic specification.

Xiang Yin, Majid Zamani

Opacity is an important information-flow security property in the analysis of cyber-physical systems. It captures the plausible deniability of the system's secret behavior in the presence of an intruder that may access the information flow. Existing works on opacity only consider non-metric systems by assuming that the intruder can always distinguish two different outputs precisely. In this paper, we extend the concept of opacity to systems whose output sets are equipped with metrics. Such systems are widely used in the modeling of many real-world systems whose measurements are physical signals. A new concept called approximate opacity is proposed in order to quantitatively evaluate the security guarantee level with respect to the measurement precision of the intruder. Then we propose a new simulation-type relation, called approximate opacity preserving simulation relation, which characterizes how close two systems are in terms of the satisfaction of approximate opacity. This allows us to verify approximate opacity for large-scale, or even infinite systems, using their abstractions. We also discuss how to construct approximate opacity preserving symbolic models for a class of discrete-time control systems. Our results extend the definitions and analysis techniques for opacity from non-metric systems to metric systems.

Saurabh Bagchi, Hyunseung Kim, Tarek Abdelzaher et al.

Resilience in cyber-physical systems (CPS) is the fundamental ability to maintain safety and critical functionality despite adverse "perturbations," which includes security attacks, environmental disruptions, and hardware or software failures. This survey provides a comprehensive review of CPS resilience, framing the field through five interconnected themes that are required in an integrated whole to achieve real-world resilience. The article first posits that resilience is a system-wide property emerging from interactions between hardware, software, and human users. Second, it addresses the challenges of learning-enabled CPS, which often operate in data-scarce environments characterized by imbalanced or noisy data, requiring innovative solutions like synthetic data generation and foundation model adaptation. Third, the survey examines proactive measures for resilience, which include distinctive aspects of verification, testing, and redundancy. Fourth, it explores recovery mechanisms, moving beyond traditional fault models to design "just good enough" recovery strategies that prioritize safety-critical functions during perturbations. Finally, it highlights the central role of the human, focusing on the different levels of human intervention, the necessity of trust calibration, and the requirement for explainable AI to support human-CPS teaming. These themes are illustrated through representative application domains, primarily Connected and Autonomous Transportation Systems (CATS) and Medical CPS (MCPS). By integrating the five interconnected themes, this survey provides a systematic roadmap for achieving the resilient CPS in increasingly complex and adversarial environments.

Abdalla Swikir, Antoine Girard, Majid Zamani

In this work, we introduce a compositional framework for the construction of finite abstractions (a.k.a. symbolic models) of interconnected discrete-time control systems. The compositional scheme is based on the joint dissipativity-type properties of discrete-time control subsystems and their finite abstractions. In the first part of the paper, we use a notion of so-called storage function as a relation between each subsystem and its finite abstraction to construct compositionally a notion of so-called simulation function as a relation between interconnected finite abstractions and that of control systems. The derived simulation function is used to quantify the error between the output behavior of the overall interconnected concrete system and that of its finite abstraction. In the second part of the paper, we propose a technique to construct finite abstractions together with their corresponding storage functions for a class of discrete-time control systems under some incremental passivity property. We show that if a discrete-time control system is so-called incrementally passivable, then one can construct its finite abstraction by a suitable quantization of the input and state sets together with the corresponding storage function. Finally, the proposed results are illustrated by constructing a finite abstraction of a network of linear discrete-time control systems and its corresponding simulation function in a compositional way. The compositional conditions in this example do not impose any restriction on the gains or the number of the subsystems which, in particular, elucidates the effectiveness of dissipativity-type compositional reasoning for networks of systems.

Majid Zamani, Ilya Tkachev, Alessandro Abate

Formal control synthesis approaches over stochastic systems have received significant attention in the past few years, in view of their ability to provide provably correct controllers for complex logical specifications in an automated fashion. Examples of complex specifications of interest include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. A general methodology to synthesize controllers for such properties resorts to symbolic abstractions of the given stochastic systems. Symbolic models are discrete abstractions of the given concrete systems with the property that a controller designed on the abstraction can be refined (or implemented) into a controller on the original system. Although the recent development of techniques for the construction of symbolic models has been quite encouraging, the general goal of formal synthesis over stochastic control systems is by no means solved. A fundamental issue with the existing techniques is the known "curse of dimensionality," which is due to the need to discretize state and input sets and that results in an exponential complexity over the number of state and input variables in the concrete system. In this work we propose a novel abstraction technique for incrementally stable stochastic control systems, which does not require state-space discretization but only input set discretization, and that can be potentially more efficient (and thus scalable) than existing approaches. We elucidate the effectiveness of the proposed approach by synthesizing a schedule for the coordination of two traffic lights under some safety and fairness requirements for a road traffic model. Further we argue that this 5-dimensional linear stochastic control system cannot be studied with existing approaches based on state-space discretization due to the very large number of generated discrete states.

Pushpak Jagtap, Sadegh Soudjani, Majid Zamani

This paper presents a methodology for temporal logic verification of discrete-time stochastic systems. Our goal is to find a lower bound on the probability that a complex temporal property is satisfied by finite traces of the system. Desired temporal properties of the system are expressed using a fragment of linear temporal logic, called safe LTL over finite traces. We propose to use barrier certificates for computations of such lower bounds, which is computationally much more efficient than the existing discretization-based approaches. The new approach is discretization-free and does not suffer from the curse of dimensionality caused by discretizing state sets. The proposed approach relies on decomposing the negation of the specification into a union of sequential reachabilities and then using barrier certificates to compute upper bounds for these reachability probabilities. We demonstrate the effectiveness of the proposed approach on case studies with linear and polynomial dynamics.

Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

This paper is concerned with a compositional approach for constructing both infinite (reduced-order models) and finite abstractions (a.k.a. finite Markov decision processes (MDPs)) of large-scale interconnected discrete-time stochastic systems. The proposed framework is based on the notion of stochastic simulation functions enabling us to employ an abstract system as a substitution of the original one in the controller design process with guaranteed error bounds. In the first part of the paper, we derive sufficient small-gain type conditions for the compositional quantification of the probabilistic distance between the interconnection of stochastic control subsystems and that of their infinite abstractions. We then construct infinite abstractions together with their corresponding stochastic simulation functions for a particular class of discrete-time nonlinear stochastic control systems. In the second part of the paper, we leverage small-gain type conditions for the compositional construction of finite abstractions. We propose an approach to construct finite MDPs as finite abstractions of concrete models or their reduced-order versions satisfying an incremental input-to-state stability property. We demonstrate the effectiveness of the proposed results by applying our approaches to a fully interconnected network of 20 nonlinear subsystems (totally 100 dimensions). We construct finite MDPs from their reduced-order versions (together 20 dimensions) with guaranteed error bounds on their output trajectories. We also apply the proposed results to a temperature regulation in a circular building and construct compositionally a finite abstraction of a network containing 1000 rooms. We employ the constructed finite abstractions as substitutes to compositionally synthesize policies regulating the temperature in each room for a bounded time horizon.

Majid Zamani, Matthias Rungger, Peyman Mohajerin Esfahani

In this paper we propose a compositional framework for the construction of approximations of the interconnection of a class of stochastic hybrid systems. As special cases, this class of systems includes both jump linear stochastic systems and linear stochastic hybrid automata. In the proposed framework, an approximation is itself a stochastic hybrid system, which can be used as a replacement of the original stochastic hybrid system in a controller design process. We employ a notion of so-called stochastic simulation function to quantify the error between the approximation and the original system. In the first part of the paper, we derive sufficient conditions which facilitate the compositional quantification of the error between the interconnection of stochastic hybrid subsystems and that of their approximations using the quantified error between the stochastic hybrid subsystems and their corresponding approximations. In particular, we show how to construct stochastic simulation functions for approximations of interconnected stochastic hybrid systems using the stochastic simulation function for the approximation of each component. In the second part of the paper, we focus on a specific class of stochastic hybrid systems, namely, jump linear stochastic systems, and propose a constructive scheme to determine approximations together with their stochastic simulation functions for this class of systems. Finally, we illustrate the effectiveness of the proposed results by constructing an approximation of the interconnection of four jump linear stochastic subsystems in a compositional way.

Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

This paper is concerned with a compositional approach for constructing finite Markov decision processes of interconnected discrete-time stochastic control systems. The proposed approach leverages the interconnection topology and a notion of so-called stochastic storage functions describing joint dissipativity-type properties of subsystems and their abstractions. In the first part of the paper, we derive dissipativity-type compositional conditions for quantifying the error between the interconnection of stochastic control subsystems and that of their abstractions. In the second part of the paper, we propose an approach to construct finite Markov decision processes together with their corresponding stochastic storage functions for classes of discrete-time control systems satisfying some incremental passivablity property. Under this property, one can construct finite Markov decision processes by a suitable discretization of the input and state sets. Moreover, we show that for linear stochastic control systems, the aforementioned property can be readily checked by some matrix inequality. We apply our proposed results to the temperature regulation in a circular building by constructing compositionally a finite Markov decision process of a network containing 200 rooms in which the compositionality condition does not require any constraint on the number or gains of the subsystems. We employ the constructed finite Markov decision process as a substitute to synthesize policies regulating the temperature in each room for a bounded time horizon.

Abdalla Swikir, Majid Zamani

In this paper, we introduce a compositional scheme for the construction of finite abstractions (a.k.a. symbolic models) of interconnected discrete-time control systems. The compositional scheme is based on small-gain type reasoning. In particular, we use a notion of so-called alternating simulation functions as a relation between each subsystem and its symbolic model. Assuming some small-gain type conditions, we construct compositionally an overall alternating simulation function as a relation between an interconnection of symbolic models and that of original control subsystems. In such compositionality reasoning, the gains associated with the alternating simulation functions of the subsystems satisfy a certain "small-gain" condition. In addition, we introduce a technique to construct symbolic models together with their corresponding alternating simulation functions for discrete-time control subsystems under some stability property. Finally, we apply our results to the temperature regulation in a circular building by constructing compositionally a finite abstraction of a network containing $N$ rooms for any $N\geq3$. We use the constructed symbolic models as substitutes to synthesize controllers compositionally maintaining room temperatures in a comfort zone. We choose $N=1000$ for the sake of illustrating the results. We also apply our proposed techniques to a nonlinear example of fully connected network in which the compositionality condition still holds for any number of components. In these case studies, we show the effectiveness of the proposed results in comparison with the existing compositionality technique in the literature using a dissipativity-type reasoning.

Pushpak Jagtap, Fardin Abdi, Matthias Rungger et al.

The paper addresses the issue of reliability of complex embedded control systems in the safety-critical environment. In this paper, we propose a novel approach to design controller that (i) guarantees the safety of nonlinear physical systems, (ii) enables safe system restart during runtime, and (iii) allows the use of complex, unverified controllers (e.g., neural networks) that drive the physical systems towards complex specifications. We use abstraction-based controller synthesis approach to design a formally verified controller that provides application and system-level fault tolerance along with safety guarantee. Moreover, our approach is implementable using commercial-off-the-shelf (COTS) processing unit. To demonstrate the efficacy of our solution and to verify the safety of the system under various types of faults injected in applications and in the underlying real-time operating system (RTOS), we implemented the proposed controller for the inverted pendulum and three degree-of-freedom (3-DOF) helicopter.

Pushpak Jagtap, Majid Zamani

Incremental stability is a property of dynamical systems ensuring the uniform asymptotic stability of each trajectory rather than a fixed equilibrium point or trajectory. Here, we introduce a notion of incremental stability for stochastic control systems and provide its description in terms of existence of a notion of so-called incremental Lyapunov functions. Moreover, we provide a backstepping controller design scheme providing controllers along with corresponding incremental Lyapunov functions rendering a class of stochastic control systems, namely, stochastic Hamiltonian systems with jumps, incrementally stable. To illustrate the effectiveness of the proposed approach, we design a controller making a spring pendulum system in a noisy environment incrementally stable.

Abdalla Swikir, Majid Zamani

In this paper, we provide a compositional methodology for constructing symbolic models for networks of discrete-time switched systems. We first define a notion of so-called augmented-storage functions to relate switched subsystems and their symbolic models. Then we show that if some dissipativity type conditions are satisfied, one can establish a notion of so-called alternating simulation function as a relation between a network of symbolic models and that of switched subsystems. The alternating simulation function provides an upper bound for the mismatch between the output behavior of the interconnection of switched subsystems and that of their symbolic models. Moreover, we provide an approach to construct symbolic models for discrete-time switched subsystems under some assumptions ensuring incremental passivity of each mode of switched subsystems. Finally, we illustrate the effectiveness of our results through two examples.

Asad Ullah Awan, Majid Zamani

In this work, we derive conditions under which compositional abstractions of networks of stochastic hybrid systems can be constructed using the interconnection topology and joint dissipativity-type properties of subsystems and their abstractions. In the proposed framework, the abstraction, itself a stochastic hybrid system (possibly with a lower dimension), can be used as a substitute of the original system in the controller design process. Moreover, we derive conditions for the construction of abstractions for a class of stochastic hybrid systems involving nonlinearities satisfying an incremental quadratic inequality. In this work, unlike existing results, the stochastic noises and jumps in the concrete subsystem and its abstraction need not to be the same. We provide examples with numerical simulations to illustrate the effectiveness of the proposed dissipativity-type compositional reasoning for interconnected stochastic hybrid systems.

Mahendra Singh Tomar, Matthias Rungger, Majid Zamani

We introduce a novel notion of invariance feedback entropy to quantify the state information that is required by any controller that enforces a given subset of the state space to be invariant. We establish a number of elementary properties, e.g. we provide conditions that ensure that the invariance feedback entropy is finite and show for the deterministic case that we recover the well-known notion of entropy for deterministic control systems. We prove the data rate theorem, which shows that the invariance entropy is a tight lower bound of the data rate of any coder-controller that achieves invariance in the closed loop. We analyze uncertain linear control systems and derive a universal lower bound of the invariance feedback entropy. The lower bound depends on the absolute value of the determinant of the system matrix and a ratio involving the volume of the invariant set and the set of uncertainties. Furthermore, we derive a lower bound of the data rate of any static, memoryless coder-controller. Both lower bounds are intimately related and for certain cases it is possible to bound the performance loss due to the restriction to static coder-controllers by $1$ bit/time unit. We provide various examples throughout the paper to illustrate and discuss different definitions and results.

Philipp J. Meyer, Matthias Rungger, Michael Luttenberger et al.

We consider the symbolic controller synthesis approach to enforce safety specifications on perturbed, nonlinear control systems. In general, in each state of the system several control values might be applicable to enforce the safety requirement and in the implementation one has the burden of picking a particular control value out of possibly many. We present a class of implementation strategies to obtain a controller with certain performance guarantees. This class includes two existing implementation strategies from the literature, based on discounted payoff and mean-payoff games. We unify both approaches by using games characterized by a single discount factor determining the implementation. We evaluate different implementations from our class experimentally on two case studies. We show that the choice of the discount factor has a significant influence on the average long-term costs, and the best performance guarantee for the symbolic model does not result in the best implementation. Comparing the optimal choice of the discount factor here with the previously proposed values, the costs differ by a factor of up to 50. Our approach therefore yields a method to choose systematically a good implementation for safety controllers with quantitative objectives.

Majid Zamani, Manuel Mazo, Mahmoud Khaled et al.

The last decade has witnessed significant attention on networked control systems (NCS) due to their ubiquitous presence in industrial applications, and, in the particular case of wireless NCS, because of their architectural flexibility and low installation and maintenance costs. In wireless NCS the communication between sensors, controllers, and actuators is supported by a communication channel that is likely to introduce variable communication delays, packet losses, limited bandwidth, and other practical non-idealities leading to numerous technical challenges. Although stability properties of NCS have been investigated extensively in the literature, results for NCS under more complex and general objectives, and in particular results dealing with verification or controller synthesis for logical specifications, are much more limited. This work investigates how to address such complex objectives by constructively deriving symbolic models of NCS, while encompassing the mentioned network non-idealities. The obtained abstracted (symbolic) models can then be employed to synthesize hybrid controllers enforcing rich logical specifications over the concrete NCS models. Examples of such general specifications include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. We thus provide a general synthesis framework that can be flexibly adapted to a number of NCS setups. We illustrate the effectiveness of the results over some case studies.

Majid Zamani, Rupak Majumdar

In this note, we propose coordinate-invariant notions of incremental Lyapunov function and provide characterizations of incremental stability in terms of existence of the proposed Lyapunov functions.

Asad Ullah Awan, Majid Zamani

In this work, we derive conditions under which abstractions of networks of stochastic hybrid systems can be constructed compositionally. Proposed conditions leverage the interconnection topology, switching randomly between P different interconnection topologies, and the joint dissipativity-type properties of subsystems and their abstractions. The random switching of the interconnection is modelled by a Markov chain. In the proposed framework, the abstraction, itself a stochastic hybrid system (possibly with a lower dimension), can be used as a substitute of the original system in the controller design process. Finally, we provide an example illustrating the effectiveness of the proposed results by designing a controller enforcing some logic properties over the interconnected abstraction and then refining it to the original interconnected system.

Paul Griffioen, Bingzhuo Zhong, Murat Arcak et al.

We compute probabilistic controlled invariant sets for nonlinear systems using Gaussian process state space models, which are data-driven models that account for unmodeled and unknown nonlinear dynamics. We propose a semidefinite programming scheme for designing state-feedback controllers that maximize the probability of the trajectories staying within a probabilistic controlled invariant set while satisfying input constraints. The results are validated on a quadrotor, both in simulation and on a physical platform.

Sara Taheri, Mahalakshmi Sabanayagam, Debarghya Ghoshdastidar et al.

The increasing use of machine learning in safety-critical domains amplifies the risk of adversarial threats, especially data poisoning attacks that corrupt training data to degrade performance or induce unsafe behavior. Most existing defenses lack formal guarantees or rely on restrictive assumptions about the model class, attack type, extent of poisoning, or point-wise certification, limiting their practical reliability. This paper introduces a principled formal robustness certification framework that models gradient-based training as a discrete-time dynamical system (dt-DS) and formulates poisoning robustness as a formal safety verification problem. By adapting the concept of barrier certificates (BCs) from control theory, we introduce sufficient conditions to certify a robust radius ensuring that the terminal model remains safe under worst-case ${\ell}_p$-norm based poisoning. To make this practical, we parameterize BCs as neural networks trained on finite sets of poisoned trajectories. We further derive probably approximately correct (PAC) bounds by solving a scenario convex program (SCP), which yields a confidence lower bound on the certified robustness radius generalizing beyond the training set. Importantly, our framework also extends to certification against test-time attacks, making it the first unified framework to provide formal guarantees in both training and test-time attack settings. Experiments on MNIST, SVHN, and CIFAR-10 show that our approach certifies non-trivial perturbation budgets while being model-agnostic and requiring no prior knowledge of the attack or contamination level.

Felipe Galarza-Jimenez, Majid Zamani, Saber Jafarpour

This paper presents a novel data-driven framework for the robust safety verification and safe control synthesis of unknown monotone discrete-time systems. While existing data-driven safety analysis approaches are often either heuristic in nature or require large amounts of data to provide rigorous guarantees, we leverage the structural property of monotonicity to significantly reduce data requirements while still ensuring formal safety guarantees. Our approach is built upon a new class of certificates called dominance functions, constructed directly from collected system trajectories, which themselves need not be safe. By exploiting the monotone structure of the dynamics, we show that dominance functions are (i) dissipative, meaning that they decrease monotonically along system trajectories, and (ii) sufficiently \expressive to characterize safety certificates for monotone systems. Together, these properties establish dominance functions as principled building blocks for the systematic construction of formal safety certificates directly from trajectory data. For both robust safety verification and safe control synthesis, we develop an efficient sampling-based optimization framework that searches for safety certificates represented as linear combinations of dominance functions constructed from collected trajectories. We validate our data-driven framework on two monotone systems by successfully deriving safety certificates from a small number of trajectories.

Vishnu Murali, Amin Falah, Ashutosh Trivedi et al.

We introduce a functional inductive framework to verify discrete-time dynamical systems against hyperproperties specified as Hyperlinear temporal logic formulae via a notion of HyperCertificates. Unlike linear temporal logic (LTL) formulae which are concerned with individual traces of a system, hyperproperties are properties that are concerned with how the traces of a system relate to one another. HyperLTL is an extension of LTL for hyperproperties, and is useful to describe specifications such as opacity, privacy as well as notions of robustness. Our notion of HyperCertificates consists of a pair of functions, where the first models the lookahead, and the second relies on a combination of barrier and ranking functions. We use closure certificates, to act as a model for this lookahead and then rely on barrier and ranking function arguments modulo this lookahead to provide guarantees against HyperLTL formulae. We demonstrate how our approach is automatable via existing techniques such as sum-of-squares optimization (SOS) and satisfiability modulo theories (SMT) solvers. Finally, we demonstrate our approach on some case studies.

Zhiyuan Huang, Shuo Li, Murat Arcak et al.

This paper introduces a general approximate alternating simulation relation (\emph{$\varepsilon$-gAAS relation}) for continuous-time systems, which relaxes existing simulation relations to tolerate larger mismatches between abstract and concrete models. The definition of gAAS for continuous-time systems is first proposed, and its properties are investigated. Then, a control refinement method is developed to enable hierarchical control for the gAAS relation. Finally, case studies demonstrate the effectiveness of the proposed approach, highlighting its advantages over existing methods.

Alireza Nadali, Bingzhuo Zhong, Ashutosh Trivedi et al.

Transfer learning is an umbrella term for machine learning approaches that leverage knowledge gained from solving one problem (the source domain) to improve speed, efficiency, and data requirements in solving a different but related problem (the target domain). The performance of the transferred model in the target domain is typically measured via some notion of loss function in the target domain. This paper focuses on effectively transferring control logic from a source control system to a target control system while providing approximately similar behavioral guarantees in both domains. However, in the absence of a complete characterization of behavioral specifications, this problem cannot be captured in terms of loss functions. To overcome this challenge, we use (approximate) simulation relations to characterize observational equivalence between the behaviors of two systems. Simulation relations ensure that the outputs of both systems, equipped with their corresponding controllers, remain close to each other over time, and their closeness can be quantified {\it a priori}. By parameterizing simulation relations with neural networks, we introduce the notion of \emph{neural simulation relations}, which provides a data-driven approach to transfer any synthesized controller, regardless of the specification of interest, along with its proof of correctness. Compared with prior approaches, our method eliminates the need for a closed-loop mathematical model and specific requirements for both the source and target systems. We also introduce validity conditions that, when satisfied, guarantee the closeness of the outputs of two systems equipped with their corresponding controllers, thus eliminating the need for post-facto verification. We demonstrate the effectiveness of our approach through case studies involving a vehicle and a double inverted pendulum.

Alireza Nadali, Ashutosh Trivedi, Majid Zamani

Control barrier certificates have proven effective in formally guaranteeing the safety of the control systems. However, designing a control barrier certificate is a time-consuming and computationally expensive endeavor that requires expert input in the form of domain knowledge and mathematical maturity. Additionally, when a system undergoes slight changes, the new controller and its correctness certificate need to be recomputed, incurring similar computational challenges as those faced during the design of the original controller. Prior approaches have utilized transfer learning to transfer safety guarantees in the form of a barrier certificate while maintaining the control invariant. Unfortunately, in practical settings, the source and the target environments often deviate substantially in their control inputs, rendering the aforementioned approach impractical. To address this challenge, we propose integrating \emph{inverse dynamics} -- a neural network that suggests required action given a desired successor state -- of the target system with the barrier certificate of the source system to provide formal proof of safety. In addition, we propose a validity condition that, when met, guarantees correctness of the controller. We demonstrate the effectiveness of our approach through three case studies.

Luca M. Meyer, Majid Zamani

Many previous works in spike sorting study spike classification and compression independently. In this paper, a novel algorithm is proposed called MetaSort to address these two problems. To deal with compression, a novel adaptive level crossing algorithm is proposed to approximate spike shapes with high fidelity. Meanwhile, the latent feature representation is used to handle the classification problem. Besides, to guarantee MetaSort is robust and discriminative, the geometric information of data is exploited simultaneously in the proposed framework by meta-transfer learning. Empirical experiments with in-vivo spike data demonstrate that MetaSort delivers promising performance, highlighting its potential and motivating continued development toward an ultra-low-power, on-chip implementation.

Daniel Ajeleye, Ashutosh Trivedi, Majid Zamani

Reward machines (RMs) provide a structured way to specify non-Markovian rewards in reinforcement learning (RL), thereby improving both expressiveness and programmability. Viewed more broadly, they separate what is known about the environment, captured by the reward mechanism, from what remains unknown and must be discovered through sampling. This separation supports techniques such as counterfactual experience generation and reward shaping, which reduce sample complexity and speed up learning. We introduce physics-informed reward machines (pRMs), a symbolic machine designed to express complex learning objectives and reward structures for RL agents, thereby enabling more programmable, expressive, and efficient learning. We present RL algorithms capable of exploiting pRMs via counterfactual experiences and reward shaping. Our experimental results show that these techniques accelerate reward acquisition during the training phases of RL. We demonstrate the expressiveness and effectiveness of pRMs through experiments in both finite and continuous physical environments, illustrating that incorporating pRMs significantly improves learning efficiency across several control tasks.

Mohammed Adib Oumer, Amr Alanwar, Majid Zamani

Ensuring safety in cyber-physical systems (CPSs) is a critical challenge, especially when system models are difficult to obtain or cannot be fully trusted due to uncertainty, modeling errors, or environmental disturbances. Traditional model-based approaches rely on precise system dynamics, which may not be available in real-world scenarios. To address this, we propose a data-driven safety verification framework that leverages matrix zonotopes and barrier certificates to verify system safety directly from noisy data. Instead of trusting a single unreliable model, we construct a set of models that capture all possible system dynamics that align with the observed data, ensuring that the true system model is always contained within this set. This model set is compactly represented using matrix zonotopes, enabling efficient computation and propagation of uncertainty. By integrating this representation into a barrier certificate framework, we establish rigorous safety guarantees without requiring an explicit system model. Numerical experiments demonstrate the effectiveness of our approach in verifying safety for dynamical systems with unknown models, showcasing its potential for real-world CPS applications.

Siyuan Liu, Ashutosh Trivedi, Xiang Yin et al.

Correct-by-construction synthesis is a cornerstone of the confluence of formal methods and control theory towards designing safety-critical systems. Instead of following the time-tested, albeit laborious (re)design-verify-validate loop, correct-by-construction methodology advocates the use of continual refinements of formal requirements -- connected by chains of formal proofs -- to build a system that assures the correctness by design. A remarkable progress has been made in scaling the scope of applicability of correct-by-construction synthesis -- with a focus on cyber-physical systems that tie discrete-event control with continuous environment -- to enlarge control systems by combining symbolic approaches with principled state-space reduction techniques. Unfortunately, in the security-critical control systems, the security properties are verified ex post facto the design process in a way that undermines the correct-by-construction paradigm. We posit that, to truly realize the dream of correct-by-construction synthesis for security-critical systems, security considerations must take center-stage with the safety considerations. Moreover, catalyzed by the recent progress on the opacity sub-classes of security properties and the notion of hyperproperties capable of combining security with safety properties, we believe that the time is ripe for the research community to holistically target the challenge of secure-by-construction synthesis. This paper details our vision by highlighting the recent progress and open challenges that may serve as bricks for providing a solid foundation for secure-by-construction synthesis of cyber-physical systems.

Pushpak Jagtap, George J. Pappas, Majid Zamani

This paper focuses on the controller synthesis for unknown, nonlinear systems while ensuring safety constraints. Our approach consists of two steps, a learning step that uses Gaussian processes and a controller synthesis step that is based on control barrier functions. In the learning step, we use a data-driven approach utilizing Gaussian processes to learn the unknown control affine nonlinear dynamics together with a statistical bound on the accuracy of the learned model. In the second controller synthesis steps, we develop a systematic approach to compute control barrier functions that explicitly take into consideration the uncertainty of the learned model. The control barrier function not only results in a safe controller by construction but also provides a rigorous lower bound on the probability of satisfaction of the safety specification. Finally, we illustrate the effectiveness of the proposed results by synthesizing a safety controller for a jet engine example.

Ali Salamati, Sadegh Soudjani, Majid Zamani

We consider systems under uncertainty whose dynamics are partially unknown. Our aim is to study satisfaction of temporal logic properties by trajectories of such systems. We express these properties as signal temporal logic formulas and check if the probability of satisfying the property is at least a given threshold. Since the dynamics are parameterized and partially unknown, we collect data from the system and employ Bayesian inference techniques to associate a confidence value to the satisfaction of the property. The main novelty of our approach is to combine both data-driven and model-based techniques in order to have a two-layer probabilistic reasoning over the behavior of the system: one layer is related to the stochastic noise inside the system and the next layer is related to the noisy data collected from the system. We provide approximate algorithms for computing the confidence for linear dynamical systems.

Abolfazl Lavaei, Fabio Somenzi, Sadegh Soudjani et al.

A novel reinforcement learning scheme to synthesize policies for continuous-space Markov decision processes (MDPs) is proposed. This scheme enables one to apply model-free, off-the-shelf reinforcement learning algorithms for finite MDPs to compute optimal strategies for the corresponding continuous-space MDPs without explicitly constructing the finite-state abstraction. The proposed approach is based on abstracting the system with a finite MDP (without constructing it explicitly) with unknown transition probabilities, synthesizing strategies over the abstract MDP, and then mapping the results back over the concrete continuous-space MDP with approximate optimality guarantees. The properties of interest for the system belong to a fragment of linear temporal logic, known as syntactically co-safe linear temporal logic (scLTL), and the synthesis requirement is to maximize the probability of satisfaction within a given bounded time horizon. A key contribution of the paper is to leverage the classical convergence results for reinforcement learning on finite MDPs and provide control strategies maximizing the probability of satisfaction over unknown, continuous-space MDPs while providing probabilistic closeness guarantees. Automata-based reward functions are often sparse; we present a novel potential-based reward shaping technique to produce dense rewards to speed up learning. The effectiveness of the proposed approach is demonstrated by applying it to three physical benchmarks concerning the regulation of a room's temperature, control of a road traffic cell, and of a 7-dimensional nonlinear model of a BMW 320i car.

Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap et al.

Decision tree learning is a popular classification technique most commonly used in machine learning applications. Recent work has shown that decision trees can be used to represent provably-correct controllers concisely. Compared to representations using lookup tables or binary decision diagrams, decision trees are smaller and more explainable. We present dtControl, an easily extensible tool for representing memoryless controllers as decision trees. We give a comprehensive evaluation of various decision tree learning algorithms applied to 10 case studies arising out of correct-by-construction controller synthesis. These algorithms include two new techniques, one for using arbitrary linear binary classifiers in the decision tree learning, and one novel approach for determinizing controllers during the decision tree construction. In particular the latter turns out to be extremely efficient, yielding decision trees with a single-digit number of decision nodes on 5 of the case studies.

Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

This paper is concerned with a compositional approach for constructing infinite abstractions of interconnected discrete-time stochastic control systems. The proposed approach uses the interconnection matrix and joint dissipativity-type properties of subsystems and their abstractions described by a new notion of so-called stochastic storage functions. The interconnected abstraction framework is based on new notions of so-called stochastic simulation functions, using which one can quantify the distance between original interconnected stochastic control systems and interconnected abstractions in the probabilistic setting. In the first part of the paper, we derive dissipativity-type compositional reasoning for the quantification of the distance in probability between the interconnection of stochastic control subsystems and that of their abstractions. Moreover, we focus on a class of discrete-time nonlinear stochastic control systems with independent noises in the abstract and concrete subsystems, and propose a computational scheme to construct abstractions together with their corresponding stochastic storage functions. In the second part of the paper, we consider specifications expressed as syntactically co-safe linear temporal logic formulae and show how a synthesized policy for the abstract system can be refined to a policy for the original system while providing guarantee on the probability of satisfaction. We demonstrate the effectiveness of the proposed results by constructing an abstraction (totally 3 dimensions) of the interconnection of three discrete-time nonlinear stochastic control subsystems (together 222 dimensions) in a compositional fashion. We also employ the abstraction as a substitute to synthesize a controller enforcing a syntactically co-safe linear temporal logic specification.

Mahmoud Khaled, Matthias Rungger, Majid Zamani

While many studies and tools target the basic stabilizability problem of networked control systems (NCS), nowadays modern systems require more sophisticated objectives such as those expressed as formulae in linear temporal logic or as automata on infinite strings. One general technique to achieve this is based on so-called symbolic models, where complex systems are approximated by finite abstractions, and then, correct-by-construction controllers are automatically synthesized for them. We present tool SENSE for the construction of finite abstractions for NCS and the automated synthesis of controllers. Constructed controllers enforce complex specifications over plants in NCS by taking into account several non-idealities of the communication channels. Given a symbolic model of the plant and network parameters, SENSE can efficiently construct a symbolic model of the NCS, by employing operations on binary decision diagrams (BDDs). Then, it synthesizes symbolic controllers satisfying a class of specifications. It has interfaces for the simulation and the visualization of the resulting closed-loop systems using OMNETPP and MATLAB. Additionally, SENSE can generate ready-to-implement VHDL/Verilog or C/C++ codes from the synthesized controllers.