We study formal synthesis of control policies for discrete-time stochastic control systems against complex temporal properties. Our goal is to synthesize a control policy for the system together with a lower bound on the probability that the system satisfies a complex temporal property. The desired properties of the system are expressed as a fragment of linear temporal logic (LTL), called safe-LTL over finite traces. We propose leveraging control barrier certificates which alleviate the issue of the curse of dimensionality associated with discretization-based approaches existing in the literature. We show how control barrier certificates can be used for synthesizing policies while guaranteeing lower bounds on the probability of satisfaction for the given property. Our approach decomposes negation of the specification into sequential reachabilities and then finds control barrier certificates for computing upper-bounds on the reachability probabilities. Control policies associated with these barrier certificates are then combined as a hybrid control policy for the concrete system that guarantees a lower bound on the probability of satisfaction of the property.

Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backed up by the increase of research in the field. Significant efforts are being made to improve the reliability of quantum hardware and to develop suitable software to program quantum computers. In contrast, the verification of quantum programs has received relatively less attention. Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware. Research into creating verification frameworks for quantum programs has seen recent development, with a variety of tools implemented using a collection of theoretical ideas. This survey aims to be a short introduction into the area of formal verification of quantum programs, bringing together theory and tools developed to date. Further, this survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.

We present shrinking horizon model predictive control for discrete-time linear systems under stochastic disturbances with constraints encoded as Signal Temporal Logic (STL) specification. The control objective is to satisfy a given STL specification with high probability against stochastic uncertainties while maximizing the robust satisfaction of an STL specification with minimum control effort. We formulate a general solution, which does not require precise knowledge of probability distributions of (possibly dependent) stochastic disturbances; only the bounded support of the density functions and moment intervals are used. For the specific case of disturbances that are normally distributed, we optimize the controllers by utilizing knowledge of the probability distribution of the disturbance. We show that in both cases, the control law can be obtained by solving optimization problems with linear constraints at each step. We experimentally demonstrate effectiveness of this approach by synthesizing a controller for an HVAC system.

This paper is concerned with a formal verification scheme for both discrete- and continuous-time deterministic systems with unknown mathematical models. The main target is to verify the safety of unknown systems based on the construction of barrier certificates via a set of data collected from trajectories of systems while providing an a-priori guaranteed confidence on the safety. In our proposed framework, we first cast the original safety problem as a robust convex program (RCP). Solving the proposed RCP is not tractable in general since the unknown model appears in one of the constraints. Instead, we collect finite numbers of data from trajectories of the system and provide a scenario convex program (SCP) corresponding to the original RCP. We then establish a probabilistic closeness between the optimal value of SCP and that of RCP, and as a result, we formally quantify the safety guarantee of unknown systems based on the number of data points and a required level of confidence. We propose our framework in both discrete-time and continuous-time settings. We illustrate the effectiveness of our proposed results by first applying them to an unknown continuous-time room temperature system. We verify that the temperature of the room maintains in a comfort zone with some desirable confidence by collecting data from trajectories of the system. To show the applicability of our techniques to higher dimensional systems with nonlinear dynamics, we then apply our results to a continuous-time nonlinear jet engine compressor and a discrete-time DC motor.

Controller synthesis techniques for continuous systems with respect to temporal logic specifications typically use a finite-state symbolic abstraction of the system model. Constructing this abstraction for the entire system is computationally expensive, and does not exploit natural decompositions of many systems into interacting components. We describe a methodology for compositional symbolic abstraction to help scale controller synthesis for temporal logic to larger systems. We introduce disturbance bisimulation, which strengthens the standard approximate alternating bisimulation relation used in control. It extends naturally to systems which are composed of weakly interconnected sub-components, possibly connected in feedback, and models the coupling signals as disturbances. We show how networks of incrementally input-to-state stable, nonlinear, continuous-time control systems can be abstracted compositionally, so that all local abstractions are simultaneously disturbance bisimilar to their continuous counterparts. Furthermore, our construction ensures that the final composed abstraction is disturbance bisimilar to the original system. Finally, we discuss how

Discrete-time stochastic systems are an essential modelling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class of models, methods for the formal verification and synthesis of control strategies are computationally hard and generally rely on the use of approximate abstractions. Building on approximate abstractions, we compute control strategies with lower- and upper-bounds for satisfying unbounded temporal logic specifications. Firstly, robust dynamic programming mappings over the abstract system are introduced to solve the control synthesis and verification problem. These mappings yield a control strategy and a unique lower bound on the satisfaction probability for temporal logic specifications that is robust to the incurred approximation errors. Secondly, upper-bounds on the satisfaction probability are quantified, and properties of the mappings are analysed and discussed. Finally, we show the implications of these results to continuous state space of linear stochastic dynamic systems. This abstraction-based synthesis framework is shown to be able to handle infinite-horizon properties.