We present an algorithmic framework for abstraction-based verification and controller synthesis of continuous-time systems under Linear Temporal Logic (LTL) specifications. It is designed to address a key challenge in abstraction-based verification and control under complex specifications such as LTL: abstract models retain significantly less information than their original systems. This issue is especially true for continuous-time systems, where the system state trajectories are split into intervals of discrete actions, and satisfaction of atomic propositions is abstracted to a whole time interval. We propose a translation of LTL formulas into AP-observation automata, a novel type of Büchi automata specifically designed for abstraction-based verification and control. We reduce verification and controller synthesis problems to solving games built as a product between a discrete abstraction of the system and an AP-observation automaton. In addition, we incorporate a constraint on the average control signal length inspired by self-triggered control, enabling the synthesis of controllers that satisfy LTL specifications while reducing unnecessary control updates. We also present illustrative examples to demonstrate the applicability of the proposed algorithms.

A key challenge in abstraction-based verification and control under complex specifications such as Linear Temporal Logic (LTL) is that abstract models retain significantly less information than their original systems. This issue is especially true for continuous-time systems, where the system state trajectories are split into intervals of discrete actions, and satisfaction of atomic propositions is abstracted to a whole time interval. To tackle this challenge, this work introduces a novel translation from LTL specifications to AP-observation automata, a particular type of Büchi automata specifically designed for abstraction-based verification. Based on this automaton, we present a game-based verification algorithm played between the system and the environment, and an illustrative example for abstraction-based system verification under several LTL specifications.

We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas—control-data separation and logical condition propagation—in a nontrivial manner so that the two ideas boost the benefits of each other. We implemented our algorithm on top of Anglican. The experimental results demonstrate our algorithm's efficiency, especially for programs with while loops and rare observations.

We develop a method to approximate the moments of a discrete-time stochastic polynomial system. Our method is built upon Carleman linearization with truncation. Specifically, we take a stochastic polynomial system with finitely many states and transform it into an infinite-dimensional system with linear deterministic dynamics, which describe the exact evolution of the moments of the original polynomial system. We then truncate this deterministic system to obtain a finite-dimensional linear system, and use it for moment approximation by iteratively propagating the moments along the finite-dimensional linear dynamics across time. We provide efficient online computation methods for this propagation scheme with several error bounds for the approximation. Our results also show that precise values of certain moments at a given time step can be obtained when the truncated system is sufficiently large. Furthermore, we investigate techniques to reduce the offline computation load using reduced Kronecker power. Based on the obtained approximate moments and their errors, we also provide hyperellipsoidal regions that are safe for some given probability bound. Those bounds allow us to conduct probabilistic safety analysis online through convex optimization. We demonstrate our results on a logistic map with stochastic dynamics and a vehicle dynamics subject to stochastic disturbance.

We define a bidirectional compositional framework for Petri nets based on a line of work about compositionally defining games and computation models. This relies on defining structures with open ends that form interfaces they can be composed along. Together with this syntactic construction, we give a graphical language of morphisms in a PROP and a semantic category that describes the evolution of markings in a Petri net. Compared to previous work, the novelty is that computations in a Petri net are stateful, requiring specific care. This framework allows us to solve reachability compositionally.

We introduce a goal-aware extension of responsibility sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement-in addition to collision avoidance as in the original RSS-requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reasoning framework based on program logic, in which one can systematically develop RSS rules for smaller subscenarios and combine them to obtain RSS rules for bigger scenarios. As the basis of the framework, we introduce a program logic dFHL that accommodates continuous dynamics and safety conditions. Our framework presents a dFHL-based workflow for deriving goal-aware RSS rules; we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goal-aware RSS is indeed effective in realising both collision avoidance and goal achievement.

This is the artifact of the paper “Compositional Probabilistic Model Checking with String Diagrams of MDPs”.

This is the artifact of the paper “Compositional Probabilistic Model Checking with String Diagrams of MDPs”.

Following our recent development of a compositional model checking algorithm for Markov decision processes, we present a compositional framework for solving mean payoff games (MPGs). The framework is derived from category theory, specifically that of monoidal categories: MPGs (extended with open ends) get composed in so-called string diagrams and thus organized in a monoidal category; their solution is then expressed as a functor, whose preservation properties embody compositionality. As usual, the key question to compositionality is how to enrich the semantic domain; the categorical framework gives an informed guidance in solving the question by singling out the algebraic structure required in the extended semantic domain. We implemented our compositional solution in Haskell; depending on benchmarks, it can outperform an existing algorithm by an order of magnitude.

We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language of string diagrams. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is supported by category theory, while what we call decomposition equalities for expected rewards act as a key enabler. Experimental evaluation demonstrates its performance advantages.

We build on our recent work on formalization of responsibility-sensitive safety (RSS) and present the first formal framework that enables mathematical proofs of the safety of control strategies in intersection scenarios. Intersection scenarios are challenging due to the complex interaction between vehicles; to cope with it, we extend the program logic dFHL in the previous work and introduce a novel formalism of hybrid control flow graphs on which our algorithm can automatically discover an RSS condition that ensures safety. An RSS condition thus discovered is experimentally evaluated; we observe that it is safe (as our safety proof says) and is not overly conservative.

We define µTGL, a spatio-temporal logic with fixed points and first-order agent quantification whose expressive power allows the definition of topological properties of networks of communicating agents. The existence of temporal operators and fixed points requires particular care when defining its semantics. We demonstrate the logic’s usefulness on an example, where we monitor a complex property that ensures resilient consensus.

We develop a method to approximate the moments of a discrete-time stochastic polynomial system. Our method is built upon Carleman linearization with truncation. Specifically, we take a stochastic polynomial system with finitely many states and transform it into an infinite-dimensional system with linear deterministic dynamics, which describe the exact evolution of the moments of the original polynomial system. We then truncate this deterministic system to obtain a finite-dimensional linear system, and use it for moment approximation by iteratively propagating the moments along the finite-dimensional linear dynamics across time. We provide efficient online computation methods for this propagation scheme with several error bounds for the approximation. Our result also shows that precise values of certain moments can be obtained when the truncated system is sufficiently large. Furthermore, we investigate techniques to reduce the offline computation load using reduced Kronecker power. Based on the obtained approximate moments and their errors, we also provide probability bounds for the state to be outside of given hyperellipsoidal regions. Those bounds allow us to conduct probabilistic safety analysis online through convex optimization. We demonstrate our results on a logistic map with stochastic dynamics and a vehicle dynamics subject to stochastic disturbance.

Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways, such as bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive what we call codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric and bisimulation seminorm) as well as new ones (including what we call bisimulation topology).

We introduce a new logic named Quantitative Confidence Logic (QCL) that quantifies the level of confidence one has in the conclusion of a proof. By translating a fault tree representing a system’s architecture to a proof, we show how to use QCL to give a solution to the test resource allocation problem that takes the given architecture into account. We implemented a tool called Astrahl and compared our results to other testing resource allocation strategies.

We introduce a novel sampling algorithm for Bayesian inference on imperative probabilistic programs. It features a hierarchical architecture that separates control flows from data: the top-level samples a control flow, and the bottom level samples data values along the control flow picked by the top level. This separation allows us to plug various language-based analysis techniques in probabilistic program sampling; specifically, we use logical backward propagation of observations for sampling efficiency. We implemented our algorithm on top of Anglican. The experimental results demonstrate our algorithm's efficiency, especially for programs with while loops and rare observations.

In this paper, we introduce open parity games, which is a compositional approach to parity games. This is achieved by adding open ends to the usual notion of parity games. We introduce the category of open parity games, which is defined using standard definitions for graph games. We also define a graphical language for open parity games as a prop, which have recently been used in many applications as graphical languages. We introduce a suitable semantic category inspired by the work by Grellois and Melliès on the semantics of higher-order model checking. Computing the set of winning positions in open parity games yields a functor to the semantic category. Finally, by interpreting the graphical language in the semantic category, we show that this computation can be carried out compositionally.

We extend previous work on symbolic self-triggered control for non-deterministic continuous-time nonlinear systems without stability assumptions to a larger class of specifications. Our goal is to synthesise a controller for two objectives: the first one is modelled as a right-recursive LTL formula, and the second one is to ensure that the average communication rate between the controller and the system stays below a given threshold. We translate the control problem to solving a mean-payoff parity game played on a discrete graph. Apart from extending the class of specifications, we propose a heuristic method to shorten the computation time. Finally, we illustrate our results on the example of a navigating nonholonomic robot with several specifications.

We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives. The first objective is represented as a specification in a fragment of LTL, which we call 2-LTL. The second one is an energy objective, in the sense that control inputs are issued only when necessary, which saves energy. To this end, we first quantise the state and input spaces, and then translate the controller synthesis problem to the computation of a winning strategy in a mean-payoff parity game. We illustrate the feasibility of our method on the example of a navigating nonholonomic robot.

We propose a method to compute an approximation of the moments of a discrete-time stochastic polynomial system. We use the Carleman linearization technique to transform this finite-dimensional polynomial system into an infinite-dimensional linear one. After taking expectation and truncating the induced deterministic dynamics, we obtain a finite-dimensional linear deterministic system, which we then use to iteratively compute approximations of the moments of the original polynomial system at different time steps. We provide upper bounds on the approximation error for each moment and show that, for large enough truncation limits, the proposed method precisely computes moments for sufficiently small degrees and numbers of time steps. We use our proposed method for safety analysis to compute bounds on the probability of the system state being outside a given safety region. Finally, we illustrate our results on two concrete examples, a stochastic logistic map and a vehicle dynamics under stochastic disturbance.