ABSTRACT. We present an approach for identifying linear mixed logical dynamical systems from data. The dynamics is assumed to be a sum of $k$ linear dynamical modes, each activated based on a latent binary variable, called a flag. We term the discovery of the latent flag values and the corresponding linear dynamics as the ``flagged regression'' problem. This is extended to the ``guarded regression'' problem, wherein the activation of each mode is given by the sign of an affine ``guard'' function. {\new We show that the system identification problem is NP-hard 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 mixed logical dynamical models for mechanical systems with contact forces and a nonlinear robotic arm benchmark. In contrast, other approaches for piecewise affine system identification, including neural network learning, fail due to exponential complexity in terms of the data size, or lack of optimality guarantees for their solution.

ABSTRACT. 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, debugging, control synthesis, formula inference, and visualization. In the majority of cases this is done via search heuristics, especially for logics not always amenable to exhaustive methods, like Metric of Signal Temporal Logics. Search heuristics take a variable time to run and they 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 can solve the above tasks faster and/or obtain guarantees on the solution. For example, generating satisfying traces (to see whether the formula says what we think it says) reduces to random sampling in a union of polytopes. And model revision (to make it satisfy a given formula) is formulated as an optimization constrained by the set representation of the language. This paper focuses on the 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 an exact representation of the language, and that for a fixed formula, 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.

ABSTRACT. 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 specifications. 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 $n\log(n)$ dependence on the trace length $n$ for most traces arising in practice, and a $n^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.

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

ABSTRACT. 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 modeled as ordinary differential 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 SMT 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.

ABSTRACT. 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 is linear, the reachable set of states can be computed and combined with an encoding of the temporal logic specification using mixed-integer linear programming. In particular, the lowest robustness trajectory inside the reachable set is computed by the MILP solver, producing a witness initial point and vector of external inputs. 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 benchmarks from the most recent ARCH falsification competition demonstrates that we achieve superior performance over state-of-the-art tools on 16 out of 19 benchmarks based on the expected number of simulations metric. Further, on three benchmarks where no tool consistently reports a falsifying trace, our method reliably uncovers a counterexample.

ABSTRACT. Reachability analysis plays a central role in system design and verification. The reachability problem, denoted $\Diamond^J\,\Phi$, asks whether the system will meet the property $\Phi$ after some time in a given time interval $J$. 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 $\Box^I\,\Diamond^J\,\Phi$, which concerns whether the system starting from each absolute time in $I$ will meet the property $\Phi$ after some coming relative time in $J$. 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 successful 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 $\omega$-regular properties in a wide scope of real-time systems.

ABSTRACT. 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 the 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 comprehensive case study.

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

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

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

ABSTRACT. In this paper, we introduce the notion of recurrence entropy in the context of nonlinear control systems. A set is said to be ($\tau$-)recurrent if every trajectory that starts in the set returns to it (within at most $\tau$ units of time). Recurrence entropy quantifies the complexity of making a set $\tau$-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. Our results further offer insights into the minimum data rate required for achieving recurrence. We also present an algorithm for achieving recurrence asymptotically.