ABSTRACT. This paper studies exponential stability of linear systems with slow and fast time variation and switching. We use averaging to eliminate the fast dynamics and only retain the slow dynamics. We then use a recent stability criterion for slowly time-varying and switched systems, combined with perturbation analysis, to prove stability of the original system. The analysis involves working with an impulsive system in new coordinates, which enables us to treat a more general class of systems compared to previous work.

ABSTRACT. Digital filters, a subclass of linear time-invariant systems, are widely used in signal processing and control systems. A digital filter performs mathematical operations on a sampled, discrete-time signal to reduce or enhance certain aspects of that signal. Such a system is implemented by a loop that iterates over an infinite time horizon. At each iteration, a random value is generated as input, and a linear expression is evaluated as output. In control theory, bounded-input, bounded-output (BIBO) stability is a fundamental criterion, which requires that any bounded input to a digital filter yields a bounded output. Correspondingly, at the implementation level, we aim to determine if a specified interval bounds the output of a given filter. However, due to the complexity of digital filters, it is hard for state-of-the-art approaches to make a sound over-approximation of all the possible output values of a filter. In this work, considering the strong connection between poles of digital filters and BIBO stability, we propose a poles-based invariant to over-approximate the output ranges of filters. Initially, we design a decomposition of the iteration of a subclass of filters, based on which we derive a set of inequalities to provide bounds on the output. Subsequently, we generalize this approach to over-approximate the output ranges of general digital filters. Moreover, we split the output value at each iteration into two parts. One is computed precisely by bounded analysis. The other is a new filter that can be analyzed using our invariant. This optimization improves the precision of our approach. Leveraging this approach, we develop a prototype tool for verifying programs related to digital filters and compare it with the state-of-the-art. The results demonstrate that our approach delivers more precise over-approximations in less time for verifying BIBO stability.

ABSTRACT. In this paper, we propose an algorithm to design Lyapunov functions and upper bound the cost of solutions to a hybrid system via learning-based methods. Via enforcing conditions at finitely many sampled points of a set of interest, leveraging regularity properties of the maps defining the dynamics of the game and the stage costs associated to solutions, we can generalize the conditions to every point in the set of interest and thus, obtain an upper bound on the cost or guarantee practical asymptotic stability of a set for hybrid systems. The method uses neural networks to learn the parameters defining a Lyapunov function or the value function that satisfies sufficient point-wise conditions along continuous and discrete evolution. The approach is illustrated in a hybrid oscillator system.

ABSTRACT. Customizing autonomous vehicles to align with user preferences while ensuring safety may significantly impact their adoption. However, collecting user preference data by asking a large number of comparison questions can be demanding. In this work, we use active learning together with temporal logic descriptions of constraints to enable safe learning of preferences with a reduced number of questions. Particularly, we take a Bayesian inference approach combined with Weighted Signal Temporal Logic (WSTL), resulting in a WSTL formula that can rank signals based on user preferences and that can be used for correct-and-custom-by-construction control synthesis. Our method is practical for formulas and signals with various complexity and length since we compute STL-related values offline. We provide an upper bound for the number of answers in disagreement with user answers. We demonstrate the performance of our method both on synthetic data and by human subject experiments in an immersive driving simulator. We consider two driving scenarios, one involving a vehicle approaching a pedestrian crossing and the other with an overtake maneuver. Our results over synthetic data, where we have the ground truth weight valuation, show that our query selection algorithm converges to the ground truth weight valuation in our search set faster than random query selection. Human subject study results show that we can capture preferences with an average agreement of 94\% with user answers during training.

ABSTRACT. We present an algorithm for active learning of deterministic timed automata with multi-clock. The algorithm is within the querying framework of Angluin's $L^*$ algorithm and follows the idea proposed in existing work on the active learning of deterministic one-clock timed automata. We introduce an equivalence relation over the reset-logical-timed language of a timed automaton and then transform the learning problem into learning the corresponding reset-logical-timed language of the target automaton. Since a reset-logical-timed language includes the clocks reset information which is not observable, we first present the approach of learning from a powerful teacher who can provide reset information by answering reset information queries from the learner. Then we extend the algorithm in a normal teacher situation in which the learner can only ask standard membership query and equivalence query while the learner guesses the reset information. We prove that the learning algorithm terminates and returns a correct deterministic timed automaton. Due to the need of guessing whether the clocks reset at the transitions, the algorithm is of exponential complexity in the size of the target automaton.

ABSTRACT. In the domain of cyber-physical systems, there is an increasing relevance of data-driven approaches for the learning of hybrid system dynamics. In particular, accurate models have been successfully abstracted from continuous (real-valued) traces and applied for various goals. However, industrial applications involving online modeling or rapid prototyping have two additional requirements: 1) runtime efficiency and 2) the interpretability of the approach and results. This work adopts a common break down of this learning problem into four steps: 1) trace segmentation, 2) segment clustering, 3) characterization of the dynamics for each cluster (mode) and 4) learning of the overall model of mode transitions. Correspondingly, the bottlenecks in the state-of-the-art approaches are identified and discussed. Then, in a heuristic manner, interpretable and time-efficient algorithms for each of the steps are proposed giving a novel approach named FaMoS. The accuracy and runtime efficiency of the approach are evaluated for several system examples. FaMoS shows very short learning time, while the model’s predictions of system dynamics are close to the ground truth behavior.

ABSTRACT. This study focuses on synthesizing controllers for unknown dynamics control-affine nonlinear systems, aiming to satisfy reach-avoid-stay (RAS) specifications. The main objective is to derive a closed-form control law, incorporating a novel notion of spatiotemporal tubes, to guarantee that the system trajectories reach a designated target set while avoiding an unsafe set and adhering to state constraints. The efficacy of this approach is demonstrated through simulation.

ABSTRACT. In this work, we develop an open-source software tool, called IMPaCT, for the parallelized verification and controller synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs), respectively. The tool serves to (i) construct IMCs/IMDPs as finite abstractions of underlying original systems, and (ii) leverage interval iteration algorithms for formal verification and controller synthesis over infinite-horizon properties, including safety, reachability, and reach-avoid, while offering convergence guarantees. IMPaCT is developed in C++ and designed using AdaptiveCpp, an independent open-source implementation of SYCL, for adaptive parallelism over CPUs and GPUs of all hardware vendors, including Intel and NVIDIA. IMPaCT stands as the first software tool for the parallel construction of IMCs/IMDPs, empowered with the capability to leverage high-performance computing platforms and cloud computing services, while providing formal convergence guarantees. We benchmark IMPaCT on several physical case studies adopted from the ARCH tool competition for stochastic models.

ABSTRACT. We present our tool for the segmentation of temporal behavior trees (TBT), a novel formalism for monitoring specifications. TBTs can be easily retrofitted to behavior trees, commonly used to program robotic applications. Our tool supports the robustness semantics of TBT and generates trace segmentations. In other words, given a TBT specification and a trace, it determines the optimal assignment of TBT nodes to sub-traces. To illustrate its application, we use the example of an autonomous ship deck landing. We showcase the user inputs required and demonstrate how the outputs can be interpreted to identify challenging task aspects, contributing to a comprehensive system analysis.

ABSTRACT. In this paper, we present physics-informed neural networks (PINNs) for the analysis and control of nonlinear systems. PINNs are designed to solve partial differential equations (PDEs). We demonstrate their applications in various challenging computational tasks in systems and control, including computing Lyapunov functions, regions of attraction, and optimal value functions and controllers for nonlinear systems. Additionally, we introduce LyZNet, a tool that combines physics-informed learning with formal verification to ensure the solutions provided by PINNs meet formal guarantees. We provide theoretical results and demonstrate with numerical examples of both low- and high-dimensional nonlinear systems to showcase the effectiveness of the proposed framework.

ABSTRACT. We present MULTIGAIN 2.0, a major extension to the controller synthesis tool MULTIGAIN, built on top of the probabilistic model checker PRISM. This new version extends MULTIGAIN's multi-objective capabilities, by allowing for the formal verification and synthesis of controllers for probabilistic systems with multi-dimensional long-run average reward structures, steady-state constraints, and linear temporal logic properties. Additionally, MULTIGAIN 2.0 can modify the underlying linear program to prevent unbounded-memory and other unintuitive solutions and visualizes Pareto curves, in the two- and three-dimensional cases, to facilitate trade-off analysis in multi-objective scenarios.

ABSTRACT. In this work, we propose a formal framework for safety controller synthesis of stochastic control systems with both process and measurement noises while considering wireless communication networks between sensors, controllers, and actuators. The proposed scheme relies on the utilization of control barrier certificates (CBC), enabling us to offer probabilistic safety certifications for wirelessly connected stochastic systems. Despite the existing literature on designing control barrier certificates, wireless communication networks have not been taken into account to address potential packet losses and end-to-end delays, a critical consideration for safety-critical real-world applications. In our proposed scenario, the primary aim is to construct a control barrier certificate alongside a safety controller, ensuring a lower bound on the probability of satisfying the safety property within a finite time horizon. We showcase the efficacy of our approach through multiple physical case studies involving communication networks, including a permanent magnet synchronous motor, vehicle lane-keeping system, and Moore-Greitzer jet engine with nonlinear dynamics.