Computing Abstractions of Nonlinear Systems

Sufficiently accurate finite state models, also called symbolic models or discrete abstractions, allow one to apply fully automated methods, originally developed for purely discrete systems, to formally reason about continuous and hybrid systems and to design finite state controllers that provably enforce predefined specifications. We present a novel algorithm to compute such finite state models for nonlinear discrete-time and sampled systems which depends on quantizing the state space using polyhedral cells, embedding these cells into suitable supersets whose attainable sets are convex, and over-approximating attainable sets by intersections of supporting half-spaces. We prove a novel recursive description of these half-spaces and propose an iterative procedure to compute them efficiently. We also provide new sufficient conditions for the convexity of attainable sets which imply the existence of the aforementioned embeddings of quantizer cells. Our method yields highly accurate abstractions and applies to nonlinear systems under mild assumptions, which reduce to sufficient smoothness in the case of sampled systems. Its practicability in the design of discrete controllers for nonlinear continuous plants under state and control constraints is demonstrated by an example.

Related papers:

title: Verification and Control of Hybrid Systems
abstract: In what case do you like reading so much? What about the type of the verification and control of hybrid systems book? The needs to read? Well, everybody has their own reason why should read some books. Mostly, it will relate to their necessity to get knowledge from the book and want to read just to get entertainment. Novels, story book, and other entertaining books become so popular this day. Besides, the scientific books will also be the best reason to choose, especially for the students, teachers, doctors, businessman, and other professions who are fond of reading.

title: Conflict resolution for air traffic management: a study in multiagent hybrid systems
abstract: Air traffic management (ATM) of the future allows for the possibility of free flight, in which aircraft choose their own optimal routes, altitudes, and velocities. The safe resolution of trajectory conflicts between aircraft is necessary to the success of such a distributed control system. In this paper, we present a method to synthesize provably safe conflict resolution manoeuvres. The method models the aircraft and the manoeuvre as a hybrid control system and calculates the maximal set of safe initial conditions for each aircraft so that separation is assured in the presence of uncertainties in the actions of the other aircraft. Examples of manoeuvres using both speed and heading changes are worked out in detail.

title: Estimation and Control over Communication Networks
abstract: Preface Introduction Topological Entropy, Observability, Robustness, Stabilizability, and Optimal Control Stabilization of Linear Multiple Sensor Systems via Limited Capacity Communication Channels Detectability and Output Feedback Stabilizability of Nonlinear Systems via Limited Capacity Communication Channels Robust Set-Valued State Estimation via Limited Capacity Communication Channels An Analog of Shannon Information Theory: State Estimation and Stabilization of Linear Noiseless Plants via Noisy Discrete Channels An Analog of Shannon Information Theory: State Estimation and Stabilization of Linear Noisy Plants via Noisy Discrete Channels An Analog of Shannon Information Theory: Stable in Probability Control and State Estimation of Linear Noisy Plants via Noisy Discrete Channels Decentralized Stabilization of Linear Systems via Limited Capacity Communication Networks H-infinity State Estimation via Communication Channels Kalman State Estimation and Optimal Control Based on Asynchronously and Irregularly Delayed Measurements Optimal Computer Control via Asynchronous Communication Channels Linear-Quadratic Gaussian Optimal Control via Limited Capacity Communication Channels Kalman State Estimation in Networked Systems with Asynchronous Communication Channels and Switched Sensors Robust Kalman State Estimation with Switched Sensors  Proof of Proposition 7.6.13 Appendix B: Some Properties of Square Ensembles of Matrices  Some Properties of the Joint Entropy of a Random Vector and Discrete Quantity References Index

title: Modeling and Control of Logical Discrete Event Systems
abstract: Preface. 1.

title: Discrete abstractions of hybrid systems
abstract: A hybrid system is a dynamical system with both discrete and continuous state changes. For analysis purposes, it is often useful to abstract a system in a way that preserves the properties being analysed while hiding the details that are of no interest. We show that interesting classes of hybrid systems can be abstracted to purely discrete systems while preserving all properties that are definable in temporal logic. The classes that permit discrete abstractions fall into two categories. Either the continuous dynamics must be restricted, as is the case for timed and rectangular hybrid systems, or the discrete dynamics must be restricted, as is the case for o-minimal hybrid systems. In this paper, we survey and unify results from both areas.

title: An Introduction to Symbolic Dynamics and Coding
abstract: From the Publisher: 
Although it originated as a method to study general dynamical systems, symbolic dynamics is useful in coding for data storage and transmission as well as in linear algebra. Requiring only a undergraduate knowledge of linear algebra, this first general textbook includes over 500 exercises.

title: Some First-Passage Problems in Random Vibration
abstract: First-passage problems for a lightly damped linear oscillator excited by white noise are described for two types of initial conditions and three different types of barrier configurations. The qualitative behavior of the probability distribution of the time to first passage is discussed. Two numerical procedures utilizing high-speed digital computers are outlined, and quantitative results for first-passage probability densities are displayed. The asymptotic behavior of this density for long mean times to failure is discussed, and a table of experimentally determined mean times to failure is included.

title: A Method of Analyzing Generalized Cell Mappings
abstract: In this paper a method for analyzing the global properties of generalized cell mappings involving a very large number of cells is presented. The procedure of the algorithm is devised by taking advantages of certain properties of Markov chains. First, the persistent groups representing the motions to which the system will eventually evolve are determined. Then the absorption probabilities of any transient cell into these persistent groups are evaluated. These two sets of information provide us with the global behavior of the system. After describing the method its viability is illustrated by two examples.

title: Dynamical systems, graphs, and algorithms
abstract: Symbolic Image.- Periodic Trajectories.- Newton's Method.- Invariant Sets.- Chain Recurrent Set.- Attractors.- Filtration.- Structural Graph.- Entropy.- Projective Space and Lyapunov Exponents.- Morse Spectrum.- Hyperbolicity and Structural Stability.- Controllability.- Invariant Manifolds.- Ikeda Mapping Dynamics.- A Dynamical System of Mathematical Biology.

title: Asymptotic Behavior of Dynamical and Control Systems under Perturbation and Discretization
abstract: Dynamics, Perturbation and Discretization.- Setup and Preliminaries.- Strongly Attracting Sets.- Weakly Attracting Sets.- Relation between Discretization and Perturbation.- Discretizations of Attractive Sets.- Domains of Attraction.- Appendices. Viscosity Solutions. Comparison Functions.

title: Approximately optimal nonlinear stabilization with preservation of the Lyapunov function property
abstract: We present an approximate optimization approach to the computation of stabilizing feedback laws using a partitioning of the state space and a corresponding approximation of the optimal value function of the problem. By including the discretization errors into the optimal control formulation we are able to compute approximate optimal value functions which preserve the Lyapunov function property and corresponding optimally stabilizing feedback laws which are constant on each partition element. The actual computation uses efficient graph theoretic algorithms.

title: A discrete method of optimal control based upon the cell state space concept
abstract: A discrete method of optimal control is proposed in this paper. The continuum state space of a system is discretized into a cell state space, and the cost function is discretized in a similar manner. Assuming intervalwise constant controls and using a finite set of admissible control levels (u) and a finite set of admissible time intervals (τ), the motion of the system under all possible interval controls (u, τ) can then be expressed in terms of a family of cell-to-cell mappings. The proposed method extracts the optimal control results from these mappings by a systematic search, culminating in the construction of a discrete optimal control table.The possibility of expressing the optimal control results in the form of a control table seems to give this method a means to make systems real-time controllable.

title: An Approximate Simulation Approach to Symbolic Control
abstract: 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.

title: An invariant-based approach to the design of hybrid control systems
abstract: In this paper, a methodology for hybrid control design is presented. The hybrid systems of interest are characterized by a feedback architecture of a continuous nonlinear plant with a discrete-event controller. The natural invariants of the continuous dynamics are used to partition the state space into regions and to synthesize simple and efficient control laws. The paper contains a complete description of the approach including a description of the hybrid control system modelling, of the invariant-based approach for the design of the partition, and of the controller synthesis methodology illustrated by examples. The implementation and optimization of the approach are also discussed. The approach presented in this paper not only describes a viable methodology to hybrid design, but also addresses fundamental issues in hybrid system theory that arise in reachability analysis and verification approaches that are based on partitions of the continuous state space.

title: Models for Dynamics
abstract: The purpose of this paper is to give a tutorial exposition of what we consider to be the basic mathematical concepts in the theory of dynamical systems.

title: Supervisory control of hybrid systems
abstract: In this paper, the supervisory control of hybrid systems is introduced and discussed at length. Such control systems typically arise in the computer control of continuous processes, for example, in manufacturing and chemical processes, in transportation systems, and in communication networks. A functional architecture of hybrid control systems consisting of a continuous plant, a discrete-event controller, and an interface is used to introduce and describe analysis and synthesis concepts and approaches. Our approach highlights the interaction between the continuous and discrete dynamics, which is the cornerstone of any hybrid system study. Discrete abstractions are used to approximate the continuous plant. Properties of the discrete abstractions to be appropriate representations of the continuous plant are presented, and important concepts such as determinism and controllability are discussed. Supervisory control design methodologies are presented to satisfy control specifications described by formal languages. Several examples are used throughout the paper to illustrate our approach.

title: Robust hybrid control from a behavioural perspective
abstract: This paper investigates the synthesis of discrete supervisors for hybrid systems where the control objective is to enforce a language inclusion specification in the presence of plant's uncertainty. The discussion is set within Willems' behavioural system theory, where we find a relationship between the robustness of closed-loop performance and earlier results on abstraction based synthesis. From this relationship, we develop our main result: a method for the synthesis of robust supervisory controllers. Note that virtually any engineering system must possess a certain amount of robustness in order to fulfil even minimal reliability requirements. This commonly accepted fact is of a particular importance for hybrid control systems, since the motivating application areas are safety-critical and high-confidence systems as air traffic control or medical instrumentation.

title: Supervisory control of hybrid systems within a behavioural framework
abstract: This contribution addresses the synthesis of supervisory control for hybrid systems Σ with discrete external signals. Such systems are in general neither l -complete nor can they be represented by finite state machines. We find an l -complete approximation (abstraction) Σ l for Σ , represent it by a finite state machine, and investigate the control problem for the approximation. If a solution exists, we synthesize the maximally permissive supervisor for Σ l . We show that it also solves the control problem for the hybrid system Σ . If no solution exists, approximation accuracy can be increased by computing a k -complete abstraction Σ k , k>l . This paper is entirely set within the framework on Willems’ behavioural systems theory.

title: Computation of Discrete Abstractions of Arbitrary Memory Span for Nonlinear Sampled Systems
abstract: In this paper, we present a new method for computing discrete abstractions of arbitrary memory span for nonlinear sampled systems with quantized output. In our method, abstractions are represented by collections of conservative approximations of reachable sets by polyhedra, which in turn are represented by collections of half-spaces. Important features of our approach are that half-spaces are shared among polyhedra, and that the determination of each half-space requires the solution of a single initial value problem in an ordinary differential equation over a single sampling interval only. Apart from these numerical integrations, the only nontrivial operation to be performed repeatedly is to decide whether a given polyhedron is empty. In particular, in contrast to previous approaches, there are no intermediate bloating steps, and convex hulls are never computed. Our method heavily relies on convexity of reachable sets and applies to any sufficiently smooth system if either the sampling period, or the system of level sets of the quantizer can be chosen freely. In particular, it is not required that the system to be abstracted have any stability properties.

title: Handbook of Analysis and Its Foundations
abstract: Sets and orderings: sets functions relations and orderings more about sups and infs sets of sets - filters topologies constructivism and choice nets and convergences.  elementary algebraic systems concrete categories the real numbers linearity convexity boolean algebras logic and intangibles. Topology and uniformity: toplogical spaces separation and regularity axioms compactness uniform spaces metric and uniform completeness Baire theory positive measure and integration. Topological vector spaces: norms normed operators generalized Riemann integrals Frechet derivatives metrization of groups and vector spaces barrels and other features of TVSs duality and weak compactness vector measures initial value problems.

title: Diagnosis and Fault-tolerant Control, 2nd edition
abstract: Fault-tolerant control aims at a gradual shutdown response in automated systems when faults occur. It satisfies the industrial demand for enhanced availability and safety, in contrast to traditional reactions to faults, which bring about sudden shutdowns and loss of availability. The book presents effective model-based analysis and design methods for fault diagnosis and fault-tolerant control. Architectural and structural models are used to analyse the propagation of the fault through the process, to test the fault detectability and to find the redundancies in the process that can be used to ensure fault tolerance. It also introduces design methods suitable for diagnostic systems and fault-tolerant controllers for continuous processes that are described by analytical models of discrete-event systems represented by automata. The book is suitable for engineering students, engineers in industry and researchers who wish to get an overview of the variety of approaches to process diagnosis and fault-tolerant control. The authors have extensive teaching experience with graduate and PhD students, as well as with industrial experts. Parts of this book have been used in courses for this audience. The authors give a comprehensive introduction to the main ideas of diagnosis and fault-tolerant control and present some of their most recent research achievements obtained together with their research groups in a close cooperatio n with European research projects. The third edition resulted from a major re-structuring and re-writing of the former edition, which has been used for a decade by numerous research groups. New material includes distributed diagnosis of continuous and discrete-event systems, methods for reconfigurability analysis, and extensions of the structural methods towards fault-tolerant control. The bibliographical notes at the end of all chapters have been up-dated. The chapters end with exercises to be used in lectures.

title: Local fill reduction techniques for sparse symmetric linear systems
abstract: Local algorithms for obtaining pivot orderings for sparse symmetric coefficient matrices are reviewed together with their mathematical background, appropriate data structures and details of efficient implementation. Heuristics that go beyond the classical Minimum Degree and Minimum Local Fill scoring functions are discussed, illustrated, improved and extensively tested on a test suite of matrices from various applications. Our tests indicate that the presented techniques have the potential of accelerating circuit simulation significantly.

title: Symbolic Models for Nonlinear Control Systems: Alternating Approximate Bisimulations
abstract: Symbolic models are abstract descriptions of continuous systems in which symbols represent aggregates of continuous states. In the last few years there has been a growing interest in the use of symbolic models as a tool for mitigating complexity in control design. In fact, symbolic models enable the use of well-known algorithms in the context of supervisory control and algorithmic game theory for controller synthesis. Since the 1990s many researchers faced the problem of identifying classes of dynamical and control systems that admit symbolic models. In this paper we make further progress along this research line by focusing on control systems affected by disturbances. Our main contribution is to show that incrementally globally asymptotically stable nonlinear control systems with disturbances admit symbolic models.

title: Global numerical approach to nonlinear discrete-time control
abstract: Interval analysis is used to characterize the set of all input sequences with a given length that drive a nonlinear discrete-time state-space system from a given initial state to a given set of terminal states. No requirement other than computability (i.e. ability to be evaluated by a finite algorithm) is put on the nature of the state equations. The method is based on an algorithm for set inversion and approximates the solution set in a guaranteed way.

title: Ordinary Differential Equations
abstract: Foreword to the Classics Edition Preface to the First Edition Preface to the Second Edition Errata I: Preliminaries II: Existence III: Differential In qualities and Uniqueness IV: Linear Differential Equations V: Dependence on Initial Conditions and Parameters VI: Total and Partial Differential Equations VII: The Poincare-Bendixson Theory VIII: Plane Stationary Points IX: Invariant Manifolds and Linearizations X: Perturbed Linear Systems XI: Linear Second Order Equations XII: Use of Implicity Function and Fixed Point Theorems XIII: Dichotomies for Solutions of Linear Equations XIV: Miscellany on Monotomy Hints for Exercises References Index.

title: Strongly convex analysis
abstract: Properties of strongly convex sets (that is, of sets that can be represented as intersections of balls of radius fixed for each particular set) are investigated. A connection between strongly convex sets and strongly convex functions is established. The concept of a strongly convex R-hull of a set (the minimal strongly convex set containing the given set) is introduced; an explicit formula for the strongly convex R-hull of a set is obtained. The behaviour of the strongly convex R-hull under the variation of R and of the sets is considered. An analogue of the Caratheodory theorem for strongly convex sets is obtained. The concept of a strongly extreme point is introduced, and a generalization of the Krein-Mil'man theorem for strongly convex sets is proved. Polyhedral approximations of convex and, in particular, of strongly convex compact sets are considered. Sharp error estimates for polyhedral and strongly convex approximations of such sets from inside and outside are established.

title: MARCO: A Reachability Algorithm for Multi-affine Systems with Applications to Biological Systems
abstract: We present a new algorithm for the reachability analysis of multi-affine hybrid systems. In our previous work on reachability analysis and that of our collaborators [1,2,3], we exploited the convexity of multiaffine functions and the fact that the vector field in modes with rectangular invariants is uniquely determined by its values at the rectangle vertices. In this paper, we explicitly calculate conical overapproximations of the reachable set in the invariant of each mode. We describe our Multi-Affine Reachability analysis using Conical Overapproximations, MARCO, and show that it yields results that are superior to those obtained by existing methods for multi-affine hybrid systems. Finally, we demonstrate the application of MARCO to the analysis of an ant house hunting model that incorporates quorum sensing  and the analysis of bi-stability of the lactose induction system regulated by glucose and lactose .

title: Approximating Continuous Systems by Timed Automata
abstract: In this work we develop a new technique for over-approximating (in the sense of timed trace inclusion) continuous dynamical systems by timed automata. This technique refines commonly-used discrete abstractions which are often too coarse to be useful. The essence of our technique is the partition of the state space into cubes and the allocation of a clock for each dimension. This allows us to get much better approximations of the behavior. We specialize this technique to multi-affine systems, a class of nonlinear systems of primary importance for the analysis of biochemical systems and demonstrate its applicability on an example taken from synthetic biology.

title: Abstractions for hybrid systems
abstract: We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions.

title: Discrete-State Abstractions of Nonlinear Systems Using Multi-resolution Quantizer
abstract: This paper proposes a design method for discrete abstractions of nonlinear systems using multi-resolution quantizer, which is capable of handling state dependent approximation precision requirements. To this aim, we extend the notion of quantizer embedding, which has been proposed by the authors' previous works as a transformation from continuous-state systems to discrete-state systems, to a multi-resolution setting. Then, we propose a computational method that analyzes how a locally generated quantization error is propagated through the state space. Based on this method, we present an algorithm that generates a multi-resolution quantizer with a specified error precision by finite refinements. Discrete abstractions produced by the proposed method exhibit non-uniform distribution of discrete states and inputs.

title: Computing Reachable Sets of Hybrid Systems Using a Combination of Zonotopes and Polytopes
abstract: The computation of reachable sets for hybrid systems with linear continuous dynamics is addressed. Zonotopes are used for the representation of reachable sets, resulting in an algorithm with low computational complexity with respect to the dimension of the considered system. However, zonotopes have drawbacks when being intersected with transition guards which determine the discrete behavior of the hybrid system. For this reason, in the proposed approach, reachable sets are represented by polytopes within guard sets as an intermediate step in order to enclose them by zonotopes afterwards. Different methods for the conservative conversion from zonotopes to polytopes and vice versa are proposed and numerically evaluated.

title: A geometric approach to bisimulation and verification of hybrid systems
abstract: The paper opens up avenues for applying model checking algorithms to the verification of safety problems for hybrid systems consisting of coordinating autonomous agents, and especially hybrid systems where the continuous level is a model of the kinematic dynamics. There are some limitations and obstacles to be overcome. First, it is likely that model checking will still be a computationally expensive tool. Initially, the number of autonomous agents will be small and the continuous dynamics will be low-dimensional, at least until further breakthroughs appear on this frontier. The approach becomes more interesting when more of the burden of control can be placed at the logic level, for the performance of model checking is relatively unaffected by the number of states of the automaton. Some work that remains to be done is obtaining the approximate automaton automatically, given the analytical representation of its bisimulation, and to characterize the robustness of the reach set to model variations.

title: A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
abstract: We describe and implement an algorithm for computing the set of reachable states of a continuous dynamic game. The algorithm is based on a proof that the reachable set is the zero sublevel set of the viscosity solution of a particular time-dependent Hamilton-Jacobi-Isaacs partial differential equation. While alternative techniques for computing the reachable set have been proposed, the differential game formulation allows treatment of nonlinear systems with inputs and uncertain parameters. Because the time-dependent equation's solution is continuous and defined throughout the state space, methods from the level set literature can be used to generate more accurate approximations than are possible for formulations with potentially discontinuous solutions. A numerical implementation of our formulation is described and has been released on the web. Its correctness is verified through a two vehicle, three dimensional collision avoidance example for which an analytic solution is available.

title: Computational techniques for hybrid system verification
abstract: This paper concerns computational methods for verifying properties of polyhedral invariant hybrid automata (PIHA), which are hybrid automata with discrete transitions governed by polyhedral guards. To verify properties of the state trajectories for PIHA, the planar switching surfaces are partitioned to define a finite set of discrete states in an approximate quotient transition system (AQTS). State transitions in the AQTS are determined by the reachable states, or flow pipes, emitting from the switching surfaces according to the continuous dynamics. This paper presents a method for computing polyhedral approximations to flow pipes. It is shown that the flow-pipe approximation error can be made arbitrarily small for general nonlinear dynamics and that the computations can be made more efficient for affine systems. The paper also describes CheckMate, a MATLAB-based tool for modeling, simulating and verifying properties of hybrid systems based on the computational methods previously described.

title: Hierarchical hybrid control systems: a lattice theoretic formulation
abstract: The notion of dynamical consistency is extended to hybrid systems so as to define the set of dynamically consistent hybrid partition machines associated with a continuous system S. Following the formulation of the notions of between-block and in-block controllable hybrid partition machines, the lattice HIBC(S) of hybrid in-block controllable partition machines is defined and investigated. Based on these constructions, the definition and properties of hierarchical-hybrid control systems are presented together with an example.

title: Stability and stabilizability of discrete event dynamic systems
abstract: A finite-state automaton is adopted as a model for Discrete Event Dynamic Systems (DEDS), Stabdity is defined as wslting a given set E mtinitely often. Stabilizability is defined as choosing state feedback such that the closed loop system is stable. These notions are proposed as properties of resiliency or error-recovery. An important ingredient in stability is shown to be a notion of transition- function-invariance. Relations between our notions of stability and invariance, and the notions of safety, fairness, hvelock, deadlock, etc., in computer science literature are pointed out. Connections are established between our notions of invariance and the classical notions of A -Invariance and (A. 11)-invariance of linear systems. Polynomial algorithms for testing stability and stabilizabdity, and for constructing a stabilizing control law are also presented.

title: Directed Hypergraphs and Applications
abstract: This paper deals with directed hypergraphs as a tool to model and solve some calsses of problems arising in Operations Research and in Computer Science. Concepts such as connectivity, paths and cuts are defined. An extension of the amin duality results to a special class of hypergraphs is presented. Algorithms to perform visits of hypergraphs and to find optimal paths are studied in detail. Some applications arising in propositional logic, An-Or graphs, relational data bases and transportation analysis are presented.

title: Abstraction based solution of complex attainability problems for decomposable continuous plants
abstract: The focus of the present paper is systems of nonlinear continuous sub-plants that share a common input but are otherwise coupled only through the specification of a control problem, possibly including state constraints. Examples include cart-pole systems and collision avoidance problems involving multiple vehicles. We propose a method that uses finite state models for solving highly complex continuous attainability problems. We first prove that finite state models, also called discrete abstractions, of the overall plant may be obtained as products of abstractions of sub-plants. The latter, which we call factors, may be determined quickly and concurrently. We also modify a state-of-the-art algorithm for the discrete, auxiliary attainability problems that arise, to work directly with the set of factors and prove that the asymptotic computational complexity of the modified algorithm matches that of the original one. In practice, the latter will often be much slower since the representation of the abstraction of the overall plant on a computer is likely to require an excessive amount of memory. Practicability of our method is demonstrated by successfully designing discrete controllers that globally stabilize decomposable nonlinear continuous plants whose overall finite state models would include millions of states and billions of transitions. Working with the factors instead, problem data fit into main memory of a customary personal computer, and computations take only minutes.

title: Temporal logic motion planning for dynamic robots
abstract: In this paper, we address the temporal logic motion planning problem for mobile robots that are modeled by second order dynamics. Temporal logic specifications can capture the usual control specifications such as reachability and invariance as well as more complex specifications like sequencing and obstacle avoidance. Our approach consists of three basic steps. First, we design a control law that enables the dynamic model to track a simpler kinematic model with a globally bounded error. Second, we built a robust temporal logic specification that takes into account the tracking errors of the first step. Finally, we solve the new robust temporal logic path planning problem for the kinematic model using automata theory and simple local vector fields. The resulting continuous time trajectory is provably guaranteed to satisfy the initial user specification.

title: Approximate Bisimulations for Nonlinear Dynamical Systems
abstract: The notion of exact bisimulation equivalence for nondeterministic discrete systems has recently resulted in notions of exact bisimulation equivalence for continuous and hybrid systems. In this paper, we establish the more robust notion of approximate bisimulation equivalence for nondeterministic nonlinear systems. This is achieved by requiring that a distance between system observations starts and remains, close, in the presence of nondeterministic system evolution. We show that approximate bisimulation relations can be characterized using a class of functions called bisimulation functions. For nondeterministic nonlinear systems, we show that conditions for the existence of bisimulation functions can be expressed in terms of Lyapunov-like inequalities, which for deterministic systems can be computed using recent sum-of-squares techniques. Our framework is illustrated on a safety verification example.