Optimal input sets for steering quantized systems

Limited capacity of communication channels has strongly pushed the analysis of control systems subject to a quantized input set. Quantized control system of type x ⁺ = x + u, where the u takes values in a set of 2m + 1 integer numbers, symmetric with respect to 0 arise in some fundamental situations, e.g., flat, nilpotent, and linear systems with quantized feedback. In this paper we consider this special type of systems and analyze the reachable set after K steps. We find explicit expressions, for each K and for each m, of m input values such that the reachable set after K steps is as large as possible.     

The complexity of some reachability problems for a system on a finite group

We consider a system defined as the product of a finite set of periodic systems on cyclic groups. It is of interest to determine if certain subgroups and unions of subgroups of the state set are reachable from a specified initial state, and in particular to determine the computational complexity of verifying such reachability. These questions are motivated by certain problems that arise in the modelling and control of discrete event systems and certain forms of periodic scheduling. Our main result is that deciding whether or not the union of a certain set of subgroups is reachable or not is NP-complete.     

Model following control for continuous-time discrete-valued input systems

This paper considers a model following control problem for continuous-time discrete-valued input systems, i.e., systems including the signal quantization such as networked control systems. The constraints we address is the quantized accuracy and switching speed of the signal quantization. This paper considers the two constraints simultaneously, while most of the existing results consider them separately or either of them. Our analysis and synthesis conditions are derived in terms of invariant set and BIBO stability. Especially, the synthesis condition is recast as a set of matrix inequalities based on a non-common Lyapunov variable technique of linear matrix inequality-based multi-objective control. Moreover, we clarify the effectiveness of the proposed method through a numerical example.     

Optimal input sets for time minimality in quantized control systems

Limited capacity of communication channels has brought to the attention of many researchers the analysis of control systems subject to a quantized input set. In some fundamental cases such systems can be reduced to quantized control system of type x⁺=x+u, where the u takes values in a set of 2m+1 integer numbers, symmetric with respect to 0. In this paper we consider these types of systems and analyse the reachable set after K steps. Our aim is to find a set of m input values such that the reachable set after K steps contains an interval of integers [−N, . . . , N] with N as large as possible. For m=2,3 and 4, we completely solve the problem and characterize the metric associated to this quantized control system.     

Discrete event representation of qualitative models using Petrinets

The paper discusses how Petri nets may be used for the qualitative modeling of physical systems. The qualitative state of a system is represented by the marking of the net. The crossing of a landmark value corresponds to the firing of a transition. We give a formal procedure to construct a Petri net model corresponding to a given set of qualitative equations. The approach can be used to study both autonomous systems and systems with forcing inputs. The dynamic behavior of the system can be studied as sequences of reachable markings of the net and can be computed with standard Petri net execution techniques. This approach also leads to a simple framework for the study of hybrid systems, i.e., systems whose behavior is described by both continuous and discrete event dynamics. Several examples, with applications to diagnosis and control, are fully discussed.     

Zonotopic reachable set estimation for linear discrete‐time systems with time delay

This article studies reachable set estimation for linear discrete‐time systems with time delay, which are influenced by unknown but bounded disturbances. We propose a novel reachable set estimation method based on zonotopes for the considered systems. The proposed method can estimate real‐time reachable set under nonzero initial conditions. In order to increase estimation accuracy, we propose an iterative method to reduce the conservatism caused by the couplings between reachable sets at different instants. The effectiveness of the proposed method is illustrated by three numerical simulations.     

Discontinuous stabilization of nonlinear systems: Quantized and switching controls

In this paper we consider the classical problem of stabilizing nonlinear systems in the case the control laws take values in a discrete set. First, we present a robust control approach to the problem. Then, we focus on the class of dissipative systems and rephrase classical results available for this class taking into account the constraint on the control values. In this setting, feedback laws are necessarily discontinuous and solutions of the implemented system must be considered in some generalized sense. The relations with the problems of quantized and switching control are discussed.     

Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams

Current approaches for analyzing timed systems are based on an explicit enumeration of the discrete states and thus these techniques are only capable of analyzing systems with a handful of timers and a few thousand states. We address this limitation by describing how to analyze a timed system fully symbolically, i.e., by representing sets of discrete states and their associated timing information implicitly. We demonstrate the efficiency of the symbolic technique by computing the set of reachable states for a non-trivial timed system and compare the results with the state-of-the-art tools Kronos and Uppaal. With an implementation based on difference decision diagrams, the runtimes are several orders of magnitudes better. The key operation in obtaining these results is the ability to advance time symbolically. We show how to do this efficiently by essentially quantifying out a special variable z which is used to represent the constant zero. The symbolic manipulations given in this paper are sufficient to verify TCTL-formulae fully symbolically.     

一种求解线性控制系统可达集的数值方法

针对线性控制系统,研究应用常微分方程数值方法和优化技术相结合的近似可达集的方法.首先,用常微分方程数值方法对系统进行离散化.然后,提出基于优化技术的外部投影法来近似离散系统的可达集.外部投影法构造有限多个投影问题,每个都对应一个凸优化问题,通过求解这些凸优化问题最终可以得到可达集的近似描述.最后,通过数值仿真结果验证了所提出方法的有效性.与文献中已有的方法相比,在求解相同数量凸优化问题的情况下,外部投影法的近似精度更高.     

Bayesian statistical model checking with application to Stateflow/Simulink verification

We address the problem of model checking stochastic systems, i.e., checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for a certain class of hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic discrete systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and non-Bayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing (i.e., testing against a probability threshold) or estimation (i.e., computing with high probability a value close to the true probability). We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discrete-time hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than state-of-the-art statistical techniques. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models. It is in principle applicable to a variety of stochastic models from other domains, e.g., systems biology.     

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.     

Verifying Programs with Unreliable Channels

We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model, e.g., link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, we show that several interesting verification problems are decidable by giving algorithms for verifying (1) thereachability problem—is a finite set of global states reachable from some other global state of the system ? (2)safety properties over tracesformulated as regular sets of allowed finite traces, and (3)eventuality properties—do all computations of a system eventually reach a given set of states? We have used the algorithms to verify some idealized sliding-window protocols with reasonable time and space resources. Our results should be contrasted with the well-known fact that these problems are undecidable for systems with unboundedperfectFIFO channels.     

Quantized feedback stabilization of linear systems

This paper addresses feedback stabilization problems for linear time-invariant control systems with saturating quantized measurements. We propose a new control design methodology, which relies on the possibility of changing the sensitivity of the quantizer while the system evolves. The equation that describes the evolution of the sensitivity with time (discrete rather than continuous in most cases) is interconnected with the given system (either continuous or discrete), resulting in a hybrid system. When applied to systems that are stabilizable by linear time-invariant feedback, this approach yields global asymptotic stability     

不确定离散系统的峰峰增益优化:矩阵不等式方法

A matrix inequality approach to peak-to-peak gain minimization for a class of uncertain linear discrete systems is studied.We minimize the *-norm, which is the best upper bound on the induced L_∞norm obtained by bounding the reachable set with inescapable ellipsoids,instead of minimizing the induced L_∞norm directly.Based on this idea,the problems of robust peak-to-peak gain minimization and controller synthesis are re- duced to solving the feasibility problems of a set of matrix in- equalities.A numerical example is used to demonstrate the fea- sibility and effectiveness of the presented method.     

Controlling a Class of Nonlinear Systems on Rectangles

In this paper, we focus on a particular class of nonlinear affine control systems of the form xdot=f(x)+Bu, where the drift f is a multi-affine vector field (i.e., affine in each state component), the control distribution B is constant, and the control u is constrained to a convex set. For such a system, we first derive necessary and sufficient conditions for the existence of a multiaffine feedback control law keeping the system in a rectangular invariant. We then derive sufficient conditions for driving all initial states in a rectangle through a desired facet in finite time. If the control constraints are polyhedral, we show that all these conditions translate to checking the feasibility of systems of linear inequalities to be satisfied by the control at the vertices of the state rectangle. This work is motivated by the need to construct discrete abstractions for continuous and hybrid systems, in which analysis and control tasks specified in terms of reachability of sets of states can be reduced to searches on finite graphs. We show the application of our results to the problem of controlling the angular velocity of an aircraft with gas jet actuators     

On the boolean minimal realization problem in the max-plus algebra

One of the open problems in the max-plus-algebraic system theory for discrete event systems is the minimal realization problem. In this paper we present some results in connection with the minimal realization problem in the max-plus algebra. First we characterize the minimal system order of a max-linear discrete event system. We also introduce a canonical representation of the impulse response of a max-linear discrete event system. Next we consider a simplified version of the general minimal realization problem: the boolean minimal realization problem, i.e., we consider models in which the entries of the system matrices are either equal to the max-plus-algebraic zero element or to the max-plus-algebraic identity element. We give a lower bound for the minimal system order of a max-plus-algebraic boolean discrete event system. We show that the decision problem that corresponds to the boolean realization problem (i.e., deciding whether or not a boolean realization of a given order exists) is decidable, and that the boolean minimal realization problem can be solved in a number of elementary operations that is bounded from above by an exponential of the square of (any upper bound of) the minimal system order. We also point out some open problems, the most important of which is whether or not the boolean minimal realization problem can be solved in polynomial time.     

Measure-controlled dynamic systems: Polyhedral approximation of their reachable set boundary

An algorithm for polyhedral approximation of the reachable set of impulsive dynamic control systems is designed. The boundary points of the reachable set are determined by recursively generating and solving a family of auxiliary optimal impulsive control problems with state-linear objective functional. The impulsive control problem is solved with an algorithm that implicitly reduces the problem an ordinary optimal control problem. The reduced problem thus obtained is solved with an algorithm based on local approximations of the reachable set.     

Overapproximating Reachable Sets by Hamilton-Jacobi Projections

In earlier work, we showed that the set of states which can reach a target set of a continuous dynamic game is the zero sublevel set of the viscosity solution of a time dependent Hamilton-Jacobi-Isaacs (HJI) partial differential equation (PDE). We have developed a numerical tool—based on the level set methods of Osher and Sethian—for computing these sets, and we can accurately calculate them for a range of continuous and hybrid systems in which control inputs are pitted against disturbance inputs. The cost of our algorithm, like that of all convergent numerical schemes, increases exponentially with the dimension of the state space. In this paper, we devise and implement a method that projects the true reachable set of a high dimensional system into a collection of lower dimensional subspaces where computation is less expensive. We formulate a method to evolve the lower dimensional reachable sets such that they are each an overapproximation of the full reachable set, and thus their intersection will also be an overapproximation of the reachable set. The method uses a lower dimensional HJI PDE for each projection with a set of disturbance inputs augmented with the unmodeled dimensions of that projection's subspace. We illustrate our method on two examples in three dimensions using two dimensional projections, and we discuss issues related to the selection of appropriate projection subspaces.