HSCC '24: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control

Engineering safe and trustworthy autonomous systems demand formal methodologies that accommodate statistical models and assumptions. In the first part of this talk, I will present safety verification methods that use reachability analysis. This research explores a spectrum of model assumptions and the corresponding guarantees and utilities. The methods combine simulation data with sensitivity analysis. At one end, complete dynamical models offer strong guarantees, but their utility can be limited. Learning sensitivity from data comes with statistical guarantees, and the algorithms are applicable to real-world scenarios, and still confer the benefits of formal reasoning via composition and abstraction. This flexible approach informs our current work on the Verse framework which aims to make code-level analysis for autonomous multi-agent scenarios accessible to undergraduates in engineering design courses.

In the second part, I will discuss a safety analysis method for learning-enabled autonomous systems using abstraction and substitutivity. The method derives the conditions when a hypothetical ideal observer can be substituted with a practical observer implemented by a machine learning model. This leads to the notion of a perception contract which approximates the machine learning model, and it can substitute a perfect observer while preserving the safety proof. I will discuss applications of this method in the analysis for vision-based lane keeping and automated landing systems.

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.

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.

In this paper, we propose a learning-based algorithm for hybrid systems with a twofold purpose: first, to design Lyapunov functions and, second, to upper bound the cost of solutions to the system. Via enforcing conditions at finitely many points of a set of interest and leveraging regularity properties of the maps defining the dynamics of the system and the stage costs associated to solutions, we extend the conditions to the entire set of interest. The method employs neural networks to learn a Lyapunov function and a value-like function to guarantee the extended pointwise conditions at all points in the set of interest and thus, guarantee practical asymptotic stability of a set or provide an upper bound on the cost of solutions, respectively. The approach is illustrated in a hybrid oscillator system.

Customizing autonomous vehicles to align with user preferences while ensuring safety may significantly impact their adoption. Collecting user preference data by asking a large number of comparison questions can be demanding. In this work, we use active learning along with temporal logic descriptions of constraints to enable safe learning of preferences with a reduced number of questions. 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 be used for correct-and-custom-by-construction control synthesis. Our method is practical for formulas and signals with various complexity 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 experiments with ground truth weight valuation show that our query selection algorithm converges faster than random query selection. Human subject study results show an average agreement of 94% with user answers during training, and 79% during validation (which increases to 86% when restricted to high confidence results).

We present an algorithm for active learning of deterministic timed automata with multiple clocks. 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-clocked language of a timed automaton and then transform the learning problem into learning the corresponding reset-clocked language of the target automaton. Since a reset-clocked 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.

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.

We propose an approach to compute inner and outer-approximations of the sets of values satisfying constraints expressed as arbitrarily quantified formulas. Such formulas arise for instance when specifying important problems in control such as robustness, motion planning or controllers comparison. We propose an interval-based method which allows for tractable but tight approximations. We demonstrate its applicability through a series of examples and benchmarks using a prototype implementation.

This paper presents temporal behavior trees (TBT), a specification formalism inspired by behavior trees that are commonly used to program robotic applications. We then introduce the concept of trace segmentation, wherein given a TBT specification and a trace, we split the trace optimally into sub-traces that are associated with various portions of the TBT specification. Segmentation of a trace then serves to explain precisely how a trace satisfies or violates a specification, and which portions of a specification are actually violated. We introduce the syntax and semantics of TBT and compare their expressiveness in relation to temporal logic. Next, we define robustness semantics for TBT specification with respect to a trace. Rather than a Boolean interpretation, the robustness provides a real-valued numerical outcome that quantifies how close or far away a trace is from satisfying or violating a TBT specification. We show that computing the robustness of a trace also segments it into subtraces.Finally, we provide efficient approximations for computing robustness and segmentation for long traces with guarantees on the result.We demonstrate how segmentations are useful through applications such as understanding how novice users pilot an aerial vehicle through a sequence of waypoints in desktop experiments and the offline monitoring of automated lander for a drone on a ship. Our case studies demonstrate how TBT specification and segmentation can be used to understand and interpret complex behaviors of humans and automation in cyber-physical systems.

A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures—such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT)—barrier certificates enable an automated deductive verification approach to safety. The barrier certificate approach has been extended to refute LTL and ω -regular specifications by separating consecutive transitions of corresponding ω -automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We augment these definitions with SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness over some case studies.

We consider the problem of computing distributed logical controllers for two interacting system components via a novel sound and complete contract-based synthesis framework. Based on a discrete abstraction of component interactions as a two-player game over a finite graph and specifications for both components given as ω -regular (e.g. LTL) properties over this graph, we co-synthesize contract and controller candidates locally for each component and propose a negotiation mechanism which iteratively refines these candidates until a solution to the given distributed synthesis problem is found. Our framework relies on the recently introduced concept of permissive templates which collect an infinite number of controller candidates in a concise data structure. We utilize the efficient computability, adaptability and compositionality of such templates to obtain an efficient, yet sound and complete negotiation framework for contract-based distributed logical control. We showcase the superior performance of our approach by comparing our prototype tool CoSMo to the state-of-the-art tool on a robot motion planning benchmark suite.

We present an abstract interpretation approach for synthesizing nonlinear (semi-algebraic) positive invariants for systems of polynomial ordinary differential equations (ODEs) and switched systems. The key behind our approach is to connect the system under study to a positive nonlinear system through a “change of variables”. The positive invariance of the first orthant (Math 1) for a positive system guarantees, in turn, that the functions involved in the change of variables define a positive invariant for the original system. The challenge lies in discovering such functions for a given system. To this end, we characterize positive invariants as fixed points under an operator that is defined using the Lie derivative. Next, we use abstract-interpretation approaches to systematically compute this fixed point. Whereas abstract interpretation has been applied to the static analysis of programs, and invariant synthesis for hybrid systems to a limited extent, we show how these approaches can compute fixed points over cones generated by polynomials using sum-of-squares optimization and its relaxations. Our approach is shown to be promising over a set of small but hard-to-analyze nonlinear models, wherein it is able to generate positive invariants to place useful bounds on their reachable sets.

Formal synthesis of safe controllers is essential for safety-critical cyber-physical systems. In this paper, we propose a novel counterexample guided approach for synthesizing safe controllers of nonlinear systems using Bayesian optimization enhanced reinforcement learning, to improve the efficiency of the training process while ensuring safety property. First, we utilize the control barrier function technique to establish a constrained Markov decision process, which enables us to learn an initial controller with minimal safety violations. We then design a counterexample guided policy refinement using Bayesian optimization, to fine-tune the initial controller based on the failure trajectories. Finally, we suggest a compensatory mechanism to correct the tuned controller to guarantee the safety property. We implement the CEGRLPR tool and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our approach.

We introduce the concept of memoryless concretization relation (Math 1) to describe abstraction within the context of controller synthesis. This relation is a specific instance of alternating simulation relation (Math 2), where it is possible to simplify the controller architecture. In the case of Math 3, the concretized controller needs to simulate the concurrent evolution of two systems, the original and abstract systems, while for Math 4, the designed controllers only need knowledge of the current concrete state. We demonstrate that the distinction between Math 5 and Math 6 becomes significant only when a non-deterministic quantizer is involved, such as in cases where the state space discretization consists of overlapping cells. We also show that any abstraction of a system that alternatingly simulates a system can be completed to satisfy Math 7 at the expense of increasing the non-determinism in the abstraction. We clarify the difference between the Math 8 and the feedback refinement relation (Math 9), showing in particular that the former allows for non-constant controllers within cells. This provides greater flexibility in constructing a practical abstraction, for instance, by reducing non-determinism in the abstraction. Finally, we prove that this relation is not only sufficient, but also necessary, for ensuring the above properties.

We present an approach for identifying two subclasses of piecewise affine (PWA) systems that we call flagged and guarded linear systems. Flagged linear system dynamics are given by a sum of k linear dynamical modes, each activated based on a latent binary variable, called a flag. Additionally, guarded linear systems define each flag as the sign of an affine “guard” function. We term the discovery of the latent flag values and the corresponding linear dynamics as the “flagged regression” and “guarded regression” problems, respectively. We show that the system identification problem is NP-hard even for these models, making the identification problem computationally challenging. For both problems, we provide approximation algorithms that identify a model whose error is within some user-defined constant away from the optimum. The time complexity of these algorithms is linear in the number of data points but exponential in the state-space dimension and the number of flags. The linear complexity in data size allows our approach to potentially scale to large data sets. We evaluate our algorithms on benchmark problems in order to learn models for mechanical systems with contact forces and a nonlinear robotic arm benchmark. Our approach compares favorably against neural network learning and the PARC algorithm for identifying PWA models proposed by Bemporad.

We present an algorithm for approximating the language of a temporal logic formula, that is, the set of all signals that satisfy the formula. Most tasks involving temporal logic require determining whether a signal satisfies the formula, or finding such satisfying signals: example tasks include monitoring, testing, control synthesis, formula inference, and example generation. In the majority of cases this is done via search heuristics, especially for logics not always amenable to exhaustive methods. Search heuristics take a variable time to run and might not converge to the desired signals. There is a wide variety of heuristics and, apart from falsification, no solid guidelines for choosing between them. We take a different approach: we directly approximate the entire language of the formula. With such an approximation, we might solve the above tasks faster and/or obtain guarantees on the solution. For example, generating satisfying signals reduces to random sampling in a union of polytopes. This paper focuses on the language approximation process. We do this approximation in the special case of discrete-time Signal Temporal Logic. We show the language in this case is a union of polytopes, and upper bound the number of polytopes. We then present an algorithm for approximating this language. We evaluate the algorithm empirically and observe that it is often able to compute a highly accurate representation of the language, and that for a fixed language, the algorithm requires fewer iterations as the length of the signal increases. These results suggest that working with the language is a viable way to solving many temporal logic tasks, and raise interesting theoretical questions for investigation.

Signal Temporal Logic (STL) is a timed temporal logic formalism that has found widespread adoption for rigorous specification of properties in Cyber-Physical Systems. However, STL is unable to specify oscillatory properties commonly required in engineering design. This limitation can be overcome by the addition of additional operators, for example, signal-value freeze operators, or with first order quantification. Previous work on augmenting STL with such operators has resulted in intractable monitoring algorithms. We present the first efficient and scalable offline monitoring algorithms for STL augmented with independent freeze quantifiers. Our final optimized algorithm has a |ρ|log (|ρ|) dependence on the trace length |ρ| for most traces ρ arising in practice, and a |ρ|2 dependence in the worst case. We also provide experimental validation of our algorithms – we show the algorithms scale to traces having 100k time samples.

Reachability analysis plays a central role in system design and verification. The reachability problem, denoted Math 1, asks whether the system will meet the property Φ after some time in a given time interval Math 2. Recently, it has been considered on a novel kind of real-time systems — quantum continuous-time Markov chains (QCTMCs), and embedded into the model-checking algorithm. In this paper, we further study the repeated reachability problem in QCTMCs, denoted Math 3, which concerns whether the system starting from each absolute time in Math 4 will meet the property Φ after some coming relative time in Math 5. First of all, we reduce it to the real root isolation of a class of real-valued functions (exponential polynomials), whose solvability is conditional to Schanuel’s conjecture being true. To speed up the procedure, we employ the strategy of sampling. The original problem is shown to be equivalent to the existence of a finite collection of satisfying samples. We then present a sample-driven procedure, which can effectively refine the sample space after each time of sampling, no matter whether the sample itself is satisfying or conflicting. The improvement on efficiency is validated by randomly generated instances. Hence the proposed method would be promising to attack the repeated reachability problems together with checking other ω -regular properties in a wide scope of real-time systems.

In this work, we develop a framework for formally constructing finite abstractions, also known as finite Markov decision processes (MDPs), for continuous-space stochastic hybrid systems. These complex systems encompass both continuous dynamics, described by stochastic differential equations involving Brownian motions and Poisson processes, as well as instantaneous jumps governed by stochastic difference equations with additive noise components. Our approach is grounded in the concept of stochastic simulation functions, enabling us to employ finite MDPs as suitable substitutes for original hybrid systems in the controller design process. Our construction methodology offers an augmented framework capable of characterizing stochastic hybrid systems with both continuous evolutions and instantaneous jumps. This unified framework ensures that state trajectories of augmented systems exactly match those of original hybrid systems. Subsequently, we outline a systematic procedure for constructing finite MDPs from the general class of nonlinear stochastic hybrid systems exhibiting an incremental input-to-state stability property. Additionally, we focus on a linear class of stochastic hybrid systems and propose a construction scheme based on the satisfaction of certain matrix inequalities. We validate the efficacy of our proposed approaches through a case study.

This work studies computation tree logic (CTL) model checking for finite-state Markov decision processes (MDPs) over the space of their distributions. Instead of investigating properties over states of the MDP, as encoded by formulae in standard probabilistic CTL (PCTL), the focus of this work is on the associated transition system, which is induced by the MDP, and on its dynamics over the (transient) MDP distributions. CTL is thus used to specify properties over the space of distributions, and is shown to provide an alternative way to express probabilistic specifications or requirements over the given MDP. We discuss the distinctive semantics of CTL formulae over distribution spaces, compare them to existing non-branching logics that reason on probability distributions, and juxtapose them to traditional PCTL specifications. We then propose reachability-based CTL model checking algorithms over distribution spaces, as well as computationally tractable, sampling-based procedures for computing the relevant reachable sets: it is in particular shown that the satisfaction set of the CTL specification can be soundly under-approximated by the union of convex polytopes. Case studies display the scalability of these procedures to large MDPs.

In this paper, we offer a formal framework to automatically synthesize a hybrid controller for continuous-time nonlinear stochastic control systems while addressing control challenges closely integrated with logical decision-making processes. The primary goal is to enforce complex logic specifications that encompass context switches initiated by either the external environment or the system itself. The proposed game-solving framework adopts a two-layer strategy synthesis approach: (i) in the lower layer, it employs control barrier certificates to synthesize controllers that guarantee reach-while-avoid specifications over complex stochastic systems, and (ii) these controllers are subsequently utilized in a higher logical layer during a game-based logical control synthesis process. This approach enables the utilization of computational capabilities derived from state space control techniques and taps into the problem-solving intelligence inherent in finite games to handle complex logic specifications. We demonstrate the efficacy of our proposed approach over a robotic case study.

In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions and polynomial weight functions as a special case. Besides general LDSs, the special cases of stochastic LDSs and of LDSs with bounded orbits are considered. Furthermore, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.

In this paper, we introduce the notion of recurrence entropy in the context of nonlinear control systems. A set is said to be (τ -)recurrent if every trajectory that starts in the set returns to it (within at most τ units of time). Recurrence entropy of a control system quantifies the complexity of making a set τ -recurrent measured by the average rate of growth, as time increases, of the number of control signals required to achieve this goal. Our analysis reveals that, compared to invariance, recurrence is quantitatively less complex, meaning that the recurrence entropy of a set is no larger than, and often strictly smaller than, the invariance entropy. We provide upper and lower bounds on recurrence entropy and show that they converge to the bounds on invariance entropy as τ decreases to zero. Further, our results show that recurrence entropy lower bounds the minimum data rate between the sensor and controller required for achieving recurrence. Finally, we present an algorithm according to which the sensor can send state estimates to the controller over a limited-bandwidth channel for achieving recurrence asymptotically at an exponential rate. We relate the data rate of the algorithm with the upper bound on entropy that we derive.

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.

In this paper, we describe a lightweight Python framework that provides integrated learning and verification of neural Lyapunov functions for stability analysis. The proposed tool, named LyZNet, learns neural Lyapunov functions using physics-informed neural networks (PINNs) to solve Zubov’s equation and verifies them using satisfiability modulo theories (SMT) solvers. What distinguishes this tool from others in the literature is its ability to provide verified regions of attraction close to the domain of attraction. This is achieved by encoding Zubov’s partial differential equation (PDE) into the PINN approach. By embracing the non-convex nature of the underlying optimization problems, we demonstrate that in cases where convex optimization, such as semidefinite programming, fails to capture the domain of attraction, our neural network framework proves more successful. The tool also offers automatic decomposition of coupled nonlinear systems into a network of low-dimensional subsystems for compositional verification. We illustrate the tool’s usage and effectiveness with several numerical examples, including both non-trivial low-dimensional nonlinear systems and high-dimensional systems.

This paper presents Fossil 2.0, a new major release of a software tool for the synthesis of certificates (e.g., Lyapunov and barrier functions) for dynamical systems modelled as ordinary differential and difference equations. Fossil 2.0 is much improved from its original release, including new interfaces, a significantly expanded certificate portfolio, controller synthesis and enhanced extensibility. We present these new features as part of this tool paper. Fossil implements a counterexample-guided inductive synthesis (CEGIS) loop ensuring the soundness of the method. Our tool uses neural networks as templates to generate candidate functions, which are then formally proven by an satisfiability modulo theories solver acting as an assertion verifier. Improvements with respect to the first release include a wider range of certificates, synthesis of control laws, and support for discrete-time models.

Black-box falsification problems are most often solved by numerical optimization algorithms. In this work, we propose an alternative approach, where simulations are used to construct a surrogate model for the system dynamics using data-driven Koopman operator linearization. Since the dynamics of the Koopman model are linear, the reachable set of states can be computed and combined with an encoding of the signal temporal logic specification in a mixed-integer linear program (MILP). To determine the next sample, an MILP solver computes the least robust trajectory inside the reachable set of the surrogate model. The trajectory’s initial state and input signal are then executed on the original black-box system, where the specification is either falsified or additional simulation data is generated that we use to retrain the surrogate Koopman model and repeat the process.

The proposed method is highly effective. Evaluation on the complete set of benchmarks taken from the 2022 ARCH falsification competition demonstrates superior performance—fewer expected simulations—over all participating tools on 16 out of 19 benchmarks. Further, on three benchmarks where no tool consistently reports a falsifying trace, our method reliably uncovers a counterexample.

This study focuses on synthesizing controllers for unknown dynamics control-affine nonlinear systems, aiming to satisfy reach-avoid-stay (RAS) specifications within prescribed-time. 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.

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.

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.

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.

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.

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.