Time-optimal control for discrete-time hybrid automata

In this paper, the problem of time-optimal control for hybrid systems with discrete-time dynamics is considered. The hybrid controller steers all trajectories starting from a maximal set to a given target set in minimum time. We derive an algorithm that computes this maximal winning set. Also, algorithms for the computation of level sets associated with the value function rather than the value function itself are presented. We show that by solving the reachability problem for the discrete time hybrid automata we obtain the time optimal solution as well. The control synthesis is subject to hard constraints on both control inputs and states. For linear discrete-time dynamics, linear programming and quantifier elimination techniques are employed for the backward reachability analysis. Emphasis is given on the computation of operators for non-convex sets using an extended convex hull approach. A two-tank example is considered in order to demonstrate the techniques of the paper.     

BACH:线性混成系统有界可达性模型检验工具

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类--线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具--BACH(bounded reacha...     

Path-oriented bounded reachability analysis of composed linear hybrid systems

The existing techniques for reachability analysis of linear hybrid systems do not scale well to the problem size of practical interest. The performance of existing techniques is even worse for reachability analysis of a composition of several linear hybrid automata. In this paper, we present an efficient path-oriented approach to bounded reachability analysis of composed systems modeled by linear hybrid automata with synchronization events. It is suitable for analyzing systems with many components by selecting critical paths, while this task was quite insurmountable before because of the state explosion problem. This group of paths will be transformed to a group of linear constraints, which can be solved by a linear programming solver efficiently. This approach of symbolic execution of paths allows design engineers to check important paths, and accordingly increase the faith in the correctness of the system. This approach is implemented into a prototype tool Bounded reAchability CHecker (BACH). The experimental data show that both the path length and the number of participant automata in a system checked using BACH can scale up greatly to satisfy practical requirements.     

Hybrid heuristic search approach for deadlock-free scheduling of flexible manufacturing systems using Petri nets

Based on the Petri net models of flexible manufacturing systems (FMSs), this paper focuses on deadlock-free scheduling problem with the objective of minimizing the makespan. Two hybrid heuristic search algorithms for solving such scheduling problems of FMSs are proposed. To avoid deadlocks, the deadlock control policy is embedded into heuristic search strategies. The proposed algorithms combine the heuristic best-first strategy with the controlled backtracking strategy based on the execution of the Petri nets. The scheduling problem is transformed into a heuristic search problem in the reachability graph of the Petri net, and a schedule is a transition sequence from the initial marking to the final marking in the reachability graph. By using the one-step look-ahead method in the deadlock control policy, the safety of a state in the reachability graph is checked, and hence, deadlock is avoided. Experimental results are provided and indicate the effectiveness of the proposed hybrid heuristic search algorithms in solving deadlock-free scheduling problems of FMSs. Especially, the comparison against previous work shows that both new algorithms are promising in terms of solution quality and computing times.     

基于迁移系统分析的线性混成系统安全验证

混成自动机行为中既包含离散行为又包含连续行为,非常复杂。其安全性验证问题难以解决,即使是线性混成自动机,它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集,复杂度高,可处理问题规模非常有限。为了避免这类问题,实现了一种新的工具。该工具将线性混成自动机表达为等价的迁移系统,并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明,方法有效可行,工具具有良好的性能。     

Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming

The existing techniques for reachability analysis of linear hybrid automata do not scale well to problem sizes of practical interest. Instead of developing a tool to perform reachability check on all the paths of a linear hybrid automaton, a complementary approach is to develop an efficient path-oriented tool to check one path at a time where the length of the path being checked can be made very large and the size of the automaton can be made large enough to handle problems of practical interest. This approach of symbolic execution of paths can be used by design engineers to check important paths and thereby, increase the faith in the correctness of the system. Unlike simple testing, each path in our framework represents a dense set of possible trajectories of the system being analyzed. In this paper, we develop the linear programming based techniques towards an efficient path-oriented tool for the bounded reachability analysis of linear hybrid systems.     

Reachability and optimal control for linear hybrid automata: a quantifier elimination approach

This paper considers an optimal control problem for linear hybrid automata (LHA). First, we present a controller synthesis algorithm based on reachability analysis. The algorithm computes the maximal initial set from which the controller drives the system to a given target set. It is shown that, using quantifier elimination (QE), an under-approximation of the maximal reachable set can be derived. Next, a weighted time-optimal control problem is solved by transforming it into a constrained optimization problem whose constraints are a set of inequalities with quantifiers. Quantifier elimination (QE) techniques are employed in order to derive the quantifier free inequalities that are shown to be linear. Thus, the optimal cost is obtained using linear programming. For any state belonging to the maximal initial set the optimal switching times and the optimal continuous control inputs are computed. These are used in order to derive a hybrid controller which is optimal with respect to the cost function. Our results are applied to an air traffic management example which is of practical interest.     

On reachability and minimum cost optimal control

Questions of reachability for continuous and hybrid systems can be formulated as optimal control or game theory problems, whose solution can be characterized using variants of the Hamilton-Jacobi-Bellman or Isaacs partial differential equations. The formal link between the solution to the partial differential equation and the reachability problem is usually established in the framework of viscosity solutions. This paper establishes such a link between reachability, viability and invariance problems and viscosity solutions of a special form of the Hamilton-Jacobi equation. This equation is developed to address optimal control problems where the cost function is the minimum of a function of the state over a specified horizon. The main advantage of the proposed approach is that the properties of the value function (uniform continuity) and the form of the partial differential equation (standard Hamilton-Jacobi form, continuity of the Hamiltonian and simple boundary conditions) make the numerical solution of the problem much simpler than other approaches proposed in the literature. This fact is demonstrated by applying our approach to a reachability problem that arises in flight control and using numerical tools to compute the solution.     

Discrete reachability of hybrid systems

This paper concerns hybrid systems subject to discrete-event supervisory control. It investigates the discrete reachability, where the hybrid system should be moved from a discrete initial state z init into a given discrete goal state z goal by a sequence of discrete inputs. The reachability analysis is carried out in three steps. First, a discrete-event model of the hybrid system is set up. Stochastic automata are used to describe all state sequences which may be generated by the hybrid system. Such a model is called complete. Second, methods for the reachability analysis of stochastic automata are elaborated which concern a weak and a strong condition for reachability. Third, these methods are applied to the hybrid system. It is shown that the reachability of the automaton implies the discrete reachability of the hybrid system, because the model is complete. Therefore, the weak and the strong condition for reachability of the stochastic automaton yield a necessary and a sufficient condition for discrete reachability of the hybrid system.     

Reach set computation and control synthesis for discrete-time dynamical systems with disturbances

The paper is devoted to the formulation of the reachability problem for discrete-time dynamical systems with disturbances. The concept of maxmin and minmax forward and backward reach sets is addressed. Invariance of the backward reach set is discussed. The emphasis of the paper is on discrete-time linear systems, for which the ellipsoidal computational method is described. The synthesis of maxmin and minmax closed-loop control for steering the system to a given target set using ellipsoidal backward reach set approximations is explained. The ellipsoidal method covered in the paper is implemented in the Ellipsoidal Toolbox for MATLAB, a popular collection of ellipsoidal calculus routines freely available online.     

Dissonance between multiple alerting systems.II. avoidance and mitigation

For pt.I. see ibid., p. 366-75. The potential for conflicting information to be transmitted by different automated alerting systems is growing as these systems become more pervasive in process operations. Newly introduced alerting systems must be carefully designed to minimize the potential for and impact of alerting conflicts. A model of alert dissonance, developed in a companion paper (Part I), provides both a theoretical foundation for understanding conflicts and a practical basis from which specific problems can be addressed. Alerting systems are hybrid processes, involving continuous process dynamics and discrete alert level changes in state space. This paper presents a hybrid model to facilitate analysis of dissonance. Using backward reachability analysis, regions of dangerous dissonance space are identified. Then, modifications can be made to the control strategy of the process or to the alerting thresholds to avoid dangerous consequences of dissonance. An example problem is presented to demonstrate the application of the hybrid model to identify dangerous dissonance space and to identify proper actions to avoid dangerous consequences of dissonance.     

Symbolic backward reachability with effectively propositional logic

We describe a symbolic procedure for solving the reachability problem of transition systems that use formulae of Effectively Propositional Logic to represent sets of backward reachable states. We discuss the key ideas for the mechanization of the procedure where fix-point checks are reduced to SMT problems. We also show the termination of the procedure on a sub-class of transition systems. Then, we discuss how reachability problems for this sub-class can be used to encode analysis problems of administrative policies in the Role-Based Access Control (RBAC) model that is one of the most widely adopted access control paradigms. An implementation of a refinement of the backward reachability procedure, called asasp, shows better flexibility and scalability than a state-of-the-art tool on a significant set of security problems.     

Reachability analysis of complex planar hybrid systems

Hybrid systems are systems that exhibit both discrete and continuous behavior. Reachability, the question of whether a system in one state can reach some other state, is undecidable for hybrid systems in general. In this paper we are concerned with GSPDIs, 2-dimensional systems generalizing SPDIs (planar hybrid systems based on “simple polygonal differential inclusions”), for which reachability have been shown to be decidable. GSPDIs are useful to approximate 2-dimensional control systems, allowing the verification of safety properties of such systems.     

Two CEGAR-based approaches for the safety verification of PLC-controlled plants

In this paper we address the safety analysis of chemical plants controlled by programmable logic controllers (PLCs). We consider a specification of the control program of the PLCs, extended with the specification of the dynamic plant behavior. The resulting hybrid models can be transformed to hybrid automata, for which advanced techniques for reachability analysis exist. However, the hybrid automata models are often too large to be analyzed. We propose two counterexample-guided abstraction refinement (CEGAR) approaches to keep the size of the hybrid models moderate.     

Relay Reachability Algorithm for Exploring Huge State Space

Since many desirable properties about finite-state model are expressed as a reachability problem, reachability algorithms have been extensively studied in model checking. On the other hand, reachability algorithms play an important role in game solving since reachability games are often described as a finite state model. In this sense, reachability algorithms are located in the intersection of the research areas of Model Checking and Artificial Intelligence.This paper interests in solving the reachability games called Push-Push. However, both exact and approximate reachability algorithms are not sufficient to the games since its state space is huge and requires lots of iterations such as 338 steps in the reachability computation. Thus we devise the new algorithm called relay reachability algorithm. It divides the global state space into several local ones. And exact reachability algorithm is applied on each local state space one by one. With these reachability algorithms, we solve all of the games.     

Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems

In this work, probabilistic reachability over a finite horizon is investigated for a class of discrete time stochastic hybrid systems with control inputs. A suitable embedding of the reachability problem in a stochastic control framework reveals that it is amenable to two complementary interpretations, leading to dual algorithms for reachability computations. In particular, the set of initial conditions providing a certain probabilistic guarantee that the system will keep evolving within a desired ‘safe’ region of the state space is characterized in terms of a value function, and ‘maximally safe’ Markov policies are determined via dynamic programming. These results are of interest not only for safety analysis and design, but also for solving those regulation and stabilization problems that can be reinterpreted as safety problems. The temperature regulation problem presented in the paper as a case study is one such case.     

混合系统的形式验证技术及其在化工过程控制中的应用

针对PLC等逻辑控制器控制连续对象的可靠性问题。给出了混合系统的形式验证的方法,即用混合矩形自动机建模,通过其商迁移的可达性分析,证明了控制程序的正确性,应用实例表明该方法是可行和有效的。     

Reachability and control synthesis for piecewise-affine hybrid systems on simplices

In this paper, we consider the synthesis of control laws for piecewise-affine hybrid systems on simplices. The construction is based on the solution to the control-to-facet problem at the continuous level, and on dynamic programming at the discrete level. The construction is given as an explicit algorithm using only linear algebra and reach-set computations for automata; no numerical integration is required. The method is conservative, in that it may fail to find a control law where one exists, but one cannot hope for a sharp algorithm for control synthesis since reachability for piecewise-affine hybrid systems is undecidable.     

Analysis of Hybrid Systems Based on Hybrid Net Condition/Event System Model

In thispaper, hybrid net condition /event systems are introducedas a model for hybrid systems. The model consists of a discretetimed Petri net and a continuous Petri net which interact eachother through condition and event signals. By introducing timeddiscrete places in the model, timing constraints in hybrid systemscan be easily described. For a class of hybrid systems that canbe described as linear hybrid net condition /eventsystems whose continuous part is a constant continuous Petrinet, two methods are developed for their state reachability analysis.One is the predicate-transformation method, which is an extensionof a state reachability analysis method for linear hybrid automata.The other is the path-based method, which enumerates all possiblefiring seqenences of discrete transitions and verifies if a givenset of states can be reached from another set by firing a sequenceof discrete transitions. The verification is performed by solvinga constraint satisfaction problem. A technique that adds additionalconstraints to the problem when a discrete state is revisitedalong the sequence is developed and used to prevent the methodfrom infinite enumeration. These methods provide a basis foralgorithmic analysis of this class of hybrid systems.