Towards scalable synthesis of stochastic control systems

Formal synthesis approaches over stochastic systems have received significant attention in the past few years, in view of their ability to provide provably correct controllers for complex logical specifications in an automated fashion. Examples of complex specifications include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. A general methodology to synthesize controllers for such properties resorts to symbolic models of the given stochastic systems. Symbolic models are finite abstractions of the given concrete systems with the property that a controller designed on the abstraction can be refined (or implemented) into a controller on the original system. Although the recent development of techniques for the construction of symbolic models has been quite encouraging, the general goal of formal synthesis over stochastic control systems is by no means solved. A fundamental issue with the existing techniques is the known “curse of dimensionality,” which is due to the need to discretize state and input sets. Such discretization generally results in an exponential complexity over the number of state and input variables in the concrete system. In this work we propose a novel abstraction technique for incrementally stable stochastic control systems, which does not require state-space discretization but only input set discretization, and that can be potentially more efficient (and thus scalable) than existing approaches. We elucidate the effectiveness of the proposed approach by synthesizing a schedule for the coordination of two traffic lights under some safety and fairness requirements for a road traffic model. Further we argue that this 5-dimensional linear stochastic control system cannot be studied with existing approaches based on state-space discretization due to the very large number of generated discrete states.     

Symbolic control of linear systems based on symbolic subsystems

This paper describes an approach to the control of continuous systems through the use of symbolic models describing the system behavior only at a finite number of points in the state space. These symbolic models can be seen as abstract representations of the continuous dynamics enabling the use of algorithmic controller design methods. We identify a class of linear control systems for which the loss of information incurred by working with symbolic subsystems can be compensated by feedback. We also show how to transform symbolic controllers designed for a symbolic subsystem into controllers for the original system. The resulting controllers combine symbolic controller dynamics with continuous feedback control laws and can thus be seen as hybrid systems. Furthermore, if the symbolic controller already accounts for software/hardware requirements, the hybrid controller is guaranteed to enforce the desired specifications by construction thereby reducing the need for formal verification.     

Symbolic approximate time-optimal control

There is an increasing demand for controller design techniques capable of addressing the complex requirements of today’s embedded applications. This demand has sparked the interest in symbolic control where lower complexity models of control systems are used to cater for complex specifications given by temporal logics, regular languages, or automata. These specification mechanisms can be regarded as qualitative since they divide the trajectories of the plant into bad trajectories (those that need to be avoided) and good trajectories. However, many applications require also the optimization of quantitative measures of the trajectories retained by the controller, as specified by a cost or utility function. As a first step towards the synthesis of controllers reconciling both qualitative and quantitative specifications, we investigate in this paper the use of symbolic models for time-optimal controller synthesis. We consider systems related by approximate (alternating) simulation relations and show how such relations enable the transfer of time-optimality information between the systems. We then use this insight to synthesize approximately time-optimal controllers for a control system by working with a lower complexity symbolic model. The resulting approximately time-optimal controllers are equipped with upper and lower bounds for the time to reach a target, describing the quality of the controller. The results described in this paper were implemented in the Matlab Toolbox Pessoa (Mazo et al., 2009 [12]) which we used to workout several illustrative examples reported in this paper.     

Linear Time Logic Control of Discrete-Time Linear Systems

The control of complex systems poses new challenges that fall beyond the traditional methods of control theory. One of these challenges is given by the need to control, coordinate and synchronize the operation of several interacting submodules within a system. The desired objectives are no longer captured by usual control specifications such as stabilization or output regulation. Instead, we consider specifications given by linear temporal logic (LTL) formulas. We show that existence of controllers for discrete-time controllable linear systems and LTL specifications can be decided and that such controllers can be effectively computed. The closed-loop system is of hybrid nature, combining the original continuous dynamics with the automatically synthesized switching logic required to enforce the specification     

An Approximate Simulation Approach to Symbolic Control

This paper introduces a methodology for the symbolic control of nonlinear systems based on an approximate notion of simulation relation. This notion generalizes existing exact notions of simulation and is completely characterized in terms of known stabilizability concepts. Equipped with this notion we show how, under certain stabilizability assumptions, we can construct finite or symbolic models for nonlinear control systems. Synthesizing controllers for the original control system can then be done by using supervisory control techniques on the finite models and by refining the resulting finite controllers to hybrid controllers enforcing the specification on the original continuous control system. The proposed design methodology can be seen as a correct-by-design way of obtaining both the feedback control laws as well as the control software responsible for deciding which law is executed and when.      

Reliable dissipative control for stochastic impulsive systems

This paper deals with the problem of reliable dissipative control for a class of stochastic hybrid systems. The systems under study are subject to Markovian jump, parameter uncertainties, possible actuator failure and impulsive effects, which are often encountered in practice and the sources of instability. Our attention is focused on the design of linear state feedback controllers and impulsive controllers such that, for all admissible uncertainties as well as actuator failure occurring among a prespecified subset of actuators, the stochastic hybrid system is stochastically robustly stable and strictly (Q,S,R)-dissipative. The sufficient conditions are obtained by using linear matrix inequality (LMI) techniques. The main results of this paper extend the existing results on H^∞ control.     

Probabilistic symbolic model checking with PRISM: a hybrid approach

In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision processes using specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve a dramatic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of magnitude larger than with sparse matrices, while almost matching or even beating them for speed.     

Modelling and motion control of a mechatronic system using BGM with intelligent controllers

In this research paper, a mechatronics system such as a pan tilt platform (PTP) has been considered for motion control under intelligent controllers. A proportional-derivative (PD) controller is considered for comparison of results obtained from fuzzy and hybrid controllers. The trajectory following performance of the mechatronics system is found against these controllers. The results of simulations show that hybrid fuzzy controller reduce the tracking error effectively in lesser settling time. The intelligent controllers require knowledge base of error and derivative of error to compensate the PTP dynamics. The intelligent controllers have similar trends as the PD controllers and compensated both electrical and mechanical dynamics. The PD controller requires position measurement. The intelligent controllers have knowledge base consisting of position and velocity data. Thus intelligent controllers have position measurement along with knowledge base for position control system. The best results were achieved with hybrid fuzzy controllers. They meet the desired specifications.     

Logic-based solution methods for optimal control of hybrid systems

Combinatorial optimization over continuous and integer variables is a useful tool for solving complex optimal control problems of hybrid dynamical systems formulated in discrete-time. Current approaches are based on mixed-integer linear (or quadratic) programming (MIP), which provides the solution after solving a sequence of relaxed linear (or quadratic) programs. MIP formulations require the translation of the discrete/logic part of the hybrid problem into mixed-integer inequalities. Although this operation can be done automatically, most of the original symbolic structure of the problem (e.g., transition functions of finite state machines, logic constraints, symbolic variables, etc.) is lost during the conversion, with a consequent loss of computational performance. In this paper, we attempt to overcome such a difficulty by combining numerical techniques for solving convex programming problems with symbolic techniques for solving constraint satisfaction problems (CSP). The resulting "hybrid" solver proposed here takes advantage of CSP solvers for dealing with satisfiability of logic constraints very efficiently. We propose a suitable model of the hybrid dynamics and a class of optimal control problems that embrace both symbolic and continuous variables/functions, and that are tailored to the use of the new hybrid solver. The superiority in terms of computational performance with respect to commercial MIP solvers is shown on a centralized supply chain management problem with uncertain forecast demand.     

A learning method for multivariable PID control synthesis based on estimated plant Jacobian

Despite decades of research involving optimal control of multivariable systems, such controllers require accurate linear models of the plant dynamics. Real systems contain nonlinearities and high-order dynamics that may be difficult to model using conventional techniques. This paper presents a novel learning control (LC) method for PID controllers that doesn’t require explicit modeling of the plant dynamics. This method utilizes gradient descent techniques to iteratively reduce an error-related objective function. Simulations involving a hydrofoil catamaran show that the proposed PID-LC algorithm improves controller performance compared to LQR controllers derived from multivariable models.     

O-Minimal Hybrid Systems

An important approach to decidability questions for verification algorithms of hybrid systems has been the construction of a bisimulation. Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original infinite state hybrid system. In this paper we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and flows are definable in an o-minimal theory. We prove that o-minimal hybrid systems always admit finite bisimulations. We then present specific examples of hybrid systems with complex continuous dynamics for which finite bisimulations exist. Date received: June 9, 1998. Date revised: June 28, 1999.     

Robust switching adaptive control of multi-input nonlinear systems

During the last decade a considerable progress has been made in the design of stabilizing controllers for nonlinear systems with known and unknown constant parameters. New design tools such as adaptive feedback linearization, adaptive back-stepping, control Lyapunov functions (CLFs) and robust control Lyapunov functions (RCLFs), nonlinear damping and switching adaptive control have been introduced. Most of the results developed are applicable to single-input feedback-linearizable systems and parametric-strict-feedback systems. These results, however, cannot be applied to multi-input feedback-linearizable systems, parametric-pure-feedback systems and systems that admit a linear-in-the-parameters CLF. In this paper, we develop a general procedure for designing robust adaptive controllers for a large class of multi-input nonlinear systems. This class of nonlinear systems includes as a special case multi-input feedback-linearizable systems, parametric-pure-feedback systems and systems that admit a linear-in-the-parameters CLF. The proposed approach uses tools from the theory of RCLF and the switching adaptive controllers proposed by the authors for overcoming the problem of computing the feedback control law when the estimation model becomes uncontrollable. The proposed control approach has also been shown to be robust with respect to exogenous bounded input disturbances     

Generalized discrete-time PI control of output PDFs using square root B-spline expansion

A new control approach is proposed for the probability density function (PDF) control of non-Gaussian stochastic systems using PI controllers. Using the square root output PDF model and the weight dynamics, the PDF tracking is transformed to a constrained dynamical tracking control problem for weight dynamics, where LMI techniques are used to design a generalized PI controller such that stability, state constraints and tracking performances can be guaranteed simultaneously.     

A survey of new trends in symbolic execution for software testing and analysis

Symbolic execution is a well-known program analysis technique which represents program inputs with symbolic values instead of concrete, initialized, data and executes the program by manipulating program expressions involving the symbolic values. Symbolic execution has been proposed over three decades ago but recently it has found renewed interest in the research community, due in part to the progress in decision procedures, availability of powerful computers and new algorithmic developments. We provide here a survey of some of the new research trends in symbolic execution, with particular emphasis on applications to test generation and program analysis. We first describe an approach that handles complex programming constructs such as input recursive data structures, arrays, as well as multithreading. Furthermore, we describe recent hybrid techniques that combine concrete and symbolic execution to overcome some of the inherent limitations of symbolic execution, such as handling native code or availability of decision procedures for the application domain. We follow with a discussion of techniques that can be used to limit the (possibly infinite) number of symbolic configurations that need to be analyzed for the symbolic execution of looping programs. Finally, we give a short survey of interesting new applications, such as predictive testing, invariant inference, program repair, analysis of parallel numerical programs and differential symbolic execution.     

Automatic symbolic verification of embedded systems

Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms     

Assume–guarantee verification of nonlinear hybrid systems with Ariadne

In many applicative fields, there is the need to model and design complex systems having a mixed discrete and continuous behavior that cannot be characterized faithfully using either discrete or continuous models only. Such systems consist of a discrete control part that operates in a continuous environment and are named hybrid systems because of their mixed nature. Unfortunately, most of the verification problems for hybrid systems, like reachability analysis, turn out to be undecidable. Because of this, many approximation techniques and tools to estimate the reachable set have been proposed in the literature. However, most of the tools are unable to handle nonlinear dynamics and constraints and have restrictive licenses. To overcome these limitations, we recently proposed an open‐source framework for hybrid system verification, called Ariadne , which exploits approximation techniques based on the theory of computable analysis for implementing formal verification algorithms. In this paper, we will show how the approximation capabilities of Ariadne can be used to verify complex hybrid systems, adopting an assume–guarantee reasoning approach. Copyright © 2012 John Wiley & Sons, Ltd.