Topics in Computation and Control

Abstracts

The Ellipsoidal Tool Box Alex Kurzhanskiy and Pravin Varaiya, Berkeley

Operations of ellipsoidal calculus include affine transformations, geometric (Minkowski) sums and differences, intersections of ellipsoids with ellipsoids, hyperplanes, halfspaces and polytopes; calculation of ellipsoid-to-ellipsoid, ellipsoid-to-hyperplane, ellipsoid-to-polytope distances; and ellipsoidal projections onto given subspaces.

The Ellipsoidal Toolbox is the first free MATLAB package that implements the ellipsoidal calculus and uses ellipsoidal methods for reachability analysis of continuous- and discrete-time affine systems, continuous-time linear systems with disturbances and switched systems. The reach set computation for hybrid systems with linear continuous dynamics whose guards are hyperplanes, ellipsoids or polyhedra is not explicitly implemented, but the tool for such computation exists - namely, operations of intersection.

Recent Progress in Reachability Computation Thao Dang, CNRS-Verimag

A major ingredient of any reachability analysis algorithm for hybrid systems is an efficient method to handle their continuous dynamics described by differential equations (since their discrete dynamics can be handled using well-developed verification methods in computer science). While many well-known properties of linear differential equations can be exploited to design relatively efficient methods, non-linear systems are much more difficult to verify. In this talk, we present some recent results in reachability computation methods for non-linear continuous systems.

In the first part of the presentation, we describe an approach, called hybridization. The essence behind this approach is to partition the state space of a complex system into disjoint regions and then approximate its vector field in each region by a simpler vector field. Then, the resulting system is used to yield approximate analysis results for the original system. For safety verification purposes, the usefulness of this approach (in terms of accuracy and computational tractability) depends on the choice of the approximate system. We consider two classes of approximate systems: piecewise affine and piecewise multi-affine. We show that the use of these classes allows approximating the reachable set of the original non-linear system with a good convergence rate.

When using a piecewise multi-affine system to approximate a non-linear system, one needs to be able to deal with the multi-affine system. This motivated us to focus on polynomial continuous systems. Another reason for the interest in polynomial systems is that they can be used in a variety of applications, such as in biology. In the second part of the presentation, we describe a reachability method for such systems, which is based on Bézier techniques in computer-aided geometric modelling.

Zonotope Techniques for Reachability Analysis Antoine Girard, University of Grenoble

Reachability computation has emerged from hybrid system research as a powerful analysis tool which potentially replaces the use of an infinite number of simulations. In the recent years, much effort has been directed at developing scalable methods for reachability analysis.

In this talk, we present several techniques based on the representation of the reachable set as a union of zonotopes. A zonotope is a polytope defined as the Minkowski sum of a finite number of segments. Compared to generic polytopes, zonotopes have a compact and scalable representation. Moreover, the class of zonotopes is invariant under linear transformations and Minkowski sum. These properties allow to design efficient and accurate reachability methods for linear systems. We discuss the extension of the approach to hybrid systems.

Optimization-Based Approach to Verification Stephen Prajna, Caltech

In this talk, we present an overview of techniques based on convex optimization for verifying temporal properties such as safety, reachability, eventuality, and their simple combinations. The use of convex optimization gives several advantages on both the theoretical and computational sides. The techniques are applicable to a very large class of systems, including those with nonlinearity, uncertainty, hybrid dynamics, time-delay, and stochasticity. Not only that, convex duality can also be exploited to obtain converse statements. Finally, the computation of proofs can be performed using sum of squares programming, when the system has a polynomial description.

Relay Feedback: a Simple form of Hybrid Control Karl-Johan Astrom, Santa Barbara

Relay systems are among the simplest hybrid system. They were used in early implementation of simple controllers, they are commonly used in communication systems in the form of delta-sigma modulators, and they are used in automatic tuning, just to give a few examples. The lecture presents some useful applications and a review of the theory dating back to early work of Flugge-Lotz and Tsypkin also covering more recent results. Both simple and exotic properties of relay systems are also presented

Data-rich, Networked Control Systems for Autonomous Operations Richard Murray, Caltech

Increases in fast and inexpensive computing and communications have enabled a new generation information-rich control systems that rely on multi-threaded networked execution, distributed optimization, adaptation and learning, and contingency management in increasingly sophisticated ways. This talk will describe a framework for building such systems and lay out some of the challenges to control theory that must be addressed to enable systematic design and analysis. A driving example is provided by Alice, an autonomous vehicle that competed in the 2005 DARPA Grand Challenge. Key features of Alice include a highly sensory-driven approach to fuse sensor data into speed maps used by real-time trajectory optimization algorithms, health and contingency management algorithms to manage failures at the component and system level, and a multi-threaded, networked control architecture that enables plug-and-play operations and testing.

Some Motivations for Building an Implementation Theory for Hybrid Systems Paul Caspi , CNRS-Verimag

In this presentation, we discuss some motivations for building a computer implementation theory of hybrid control systems. Three issues are considered:

- Model-based design is considered in both computer and control science with slightly different meanings and there can be a need for making them converge toward a more uniform view.

- Mixing continuous and discrete event control is still an issue. In particular, periodically sampling discrete event systems is a popular implementation technique but it yields hazard problems which are not fully understood.

- In distributed GALS systems, the implementation of fault tolerance by redundancy heavily relies on the properties of the computations that the system is supposed to perform. Then, redundancy amounts to monitoring some of these properties.

We conclude by showing that these different issues share the same need for a notion of approximation for hybrid control signals and systems.

Approximations of Discrete, Continuous, and Hybrid Systems George Pappas, University of Pennsylvania

Compositional modelling and complexity reduction in the formal verification of purely discrete systems have resulted in a wealth of system relationships, including the established notions of language inclusion, simulation and bisimulation relations. System refinement and equivalence for purely discrete systems require observations to be identical. When discrete computing systems interact with the physical world, modelled by continuous or hybrid systems, exact refinement and equivalence are both restrictive and not robust. In this talk, I will present a framework of system approximation based on approximate language inclusion, simulation and bisimulation relations. We define a hierarchy of approximation pseudo-metrics for language inclusion, simulation, and bisimulation. The established exact notions are captured as zero sections of the pseudo-metrics. For continuous systems, whether discrete-time or continuous-time, we show how to compute the bisimulation metrics using Lyapunov-like relaxations. Finally, we illustrate how this approach gives rise to novel methods for simulation-based safety verification as well as notions of robust semantics for discrete temporal logic specifications.

(Joint work with Antoine Girard).

Synthesis of Designs from Temporal Specifications Amir Pnueli, NYU and Weizmann

We consider the problem of synthesizing digital designs or control programs from their temporal specification. In spite of the theoretical double exponential lower bound for the general case, we show that for many expressive specifications of hardware designs and control programs the problem can be solved in time N³. We describe the context of the problem, as part of a general methodology that aims to provide a property-based development flow for designs. Within such methodology, synthesis plays an important role, first in order to check whether a given specification is realizable, and then for synthesizing part of the developed system. The class of LTL formulas considered is that of Generalized
Reactivity(1) (generalized Streett(1)) formulas, i.e., formulas of the form:

         GF p_1 & ... & GF p_m) -> (GF q_1 & ... & GF q_n)

where each p_i, q_i is a bBooleancombination of atomic propositions. We also consider the more general case in which each p_i, q_i is an arbitrary past LTL formula over atomic propositions.

For this class of formulas, we present an N³-time algorithm which checks whether such a formula is realizable, i.e., there exists a circuit which satisfies the formula under any set of inputs provided by the environment. In the case that the specification is realizable, the algorithm proceeds to construct an automaton which represents one of the possible implementing circuits. The automaton is computed and presented symbolically.

We will also consider the more general case and show that similar algorithms exist for the full hierarchy of Reactivity(n) formulas (capturing the full LTL logic), where its complexity grows roughly as (n!)N^n.
(This work is joint with Nir Piterman.)

The Boolean Satisfiability Problem: Theory and Practice Bart Selman, Cornell University

Just a few years ago general inference beyond hundred variable problems appeared to be out of practical reach. Current reasoning engines, based on fast Boolean satisfiability solvers, can handle problems with over a million variables and several millions of constraints. I will discuss what led to such a dramatic scale-up, and how progress in reasoning technology has opened up a range of new applications. I will also describe current research directions centered around the integration of probabilistic and logical inference, the characterization of combinatorial search spaces using methods from statistical physics, and the development of inference methods for multi-agent systems.

(Joint work with Carla Gomes).

 
Interacting Classes of Reactive Objects P.S. Thiagarajan, Singapore 
 

Reactive systems often consist of interacting objects that can be grouped together into classes, with the objects belonging to a class exhibiting similar behaviors. Such interacting classes appear in telecommunication, transportation and avionics domains. We propose a modeling and simulation technique for such systems. A key feature of our approach is that our execution semantics leads to a symbolic simulation technique which is both time and memory efficient.

(Joint work with Ankit Goel and Abhik Roy Choudhury).

Controller Synthesis with Adversaries Oded Maler, CNRS-Verimag

Many problems in numerous domains related to the design and analysis of systems can be seen, if looked at through an appropriate abstraction, as variations and special cases of one fundamental problem, namely the problem of finding a strategy in a two-player dynamic game. In this game, player I is the "controller", the system that we design, and player II is the "environment" that generates events beyond our control. Variants of this problem differ from each other by the nature of the state space and time domain on which the game is defined (discrete, continuous, timed, hybrid), by the classes of cost function (additive over time, discrete), and by the way the outcome is quantified over the actions of the adversary (worst case, average case).

In this talk I will sketch a generic model for this problem whose instances include verification by model-checking, optimal and model-predictive control, AI planning and game playing, Markov decision processes, scheduling and more. I will identify three classes of techniques which are commonly-used for computing solutions:

1) Restriction to a finite time horizon and reduction to a constrained optimization problem (SAT, LP, mixed)

2) Backward value iteration (dynamic programming, fix point computation, HJB)

3) Heuristic forward search in the space of partial strategies.

In the second part of the talk I will sketch some work on one instance of this scheme, the problem(s) of scheduling under uncertainty, where the controller is a scheduler, allocating resources to tasks and the environment may dynamically affect task specifications, task durations or resource availability. I will show how such situations can be modelled naturally using timed automata and, sometimes, be solved algorithmically.

Mathematical Modelling of Planar Cell Polarity in the Drosophila Wing Claire Tomlin, Berkeley and Stanford

In this talk, methods that we have designed to analyze and help to identify certain protein regulatory networks will be presented. Hybrid automata represent one suitable modelling framework, as the protein concentration dynamics inside each cell are modelled using linear differential equations; inputs activate or deactivate these continuous dynamics through discrete switches, which themselves are controlled by protein concentrations reaching given thresholds. We present an iterative refinement algorithm for computing discrete abstractions of a class of symbolic hybrid automata, and we apply this algorithm to parameter identification in a model of multiple cell Delta-Notch protein signalling.

However, more often, only incomplete abstracted hypotheses exist to explain observed complex patterning and functions in cellular regulatory networks. The second part of the talk will present our results in developing a partial differential equation model for Planar Cell Polarity signalling in fly wings. We explicitly demonstrate that the model can explain the complex behaviors of the system, and can be used to test developmental hypotheses, such as the function of certain protein alleles, and the relationship between cell geometry and polarity. (Joint work with Keith Amonlirdviman, Ronojoy Ghosh and Jeffrey D. Axelrod)

Protocol Design and Analysis with applications to Biology John Doyle, Caltech

A surprisingly consistent view on the fundamental nature of complex systems can now be drawn from the convergence of three distinct research themes. First, molecular biology has provided a detailed description of much of the components of biological networks, and the organizational principles of these networks are becoming increasingly apparent. It is now clear that much of the complexity in biology is driven by its regulatory networks, however poorly understood the details remain. Second, advanced technology is creating engineering examples of networks where we do know all the details and that have complexity approaching that of biology. While the components are entirely different, there is striking convergence at the network level of the architecture and the role of protocols, layering, control, and feedback in structuring complex system modularity. Finally, there is a new mathematical framework for the study of complex networks that suggests that this apparent network-level evolutionary convergence both within biology and between biology and technology is not accidental, and follows necessarily from the requirements that both biology and technology be efficient, robust, adaptive, and evolvable. This talk will describe qualitatively in as much detail as time allows these features of biological systems and their parallels in technology, using hopefully familiar and concrete examples. The aim is to be accessible to non-biologists, relying on a shared experience with technological systems and some familiarity with the mathematical framework, which will be discussed in other talks. A crucial insight is that both evolution and natural selection or engineering design must produce high robustness to uncertain environments and components in order for systems to persist. Yet this allows and even facilitates severe fragility to novel perturbations, particularly those that exploit the very mechanisms providing robustness, and this "robust yet fragile" (RYF) feature must be exploited explicitly in any theory that hopes to scale to large systems.

Systems-Science and Biology: Exploiting Creative Tensions Charles Rockland, RIKEN BSI

Biological systems manifest a diverse range of problems of coordination, of goodness-of-fitting-together, and -- to introduce a deliberately more general and elastic terminology -- of "coherence" and "coherence maintenance". These ubiquitous problems are central to "making sense" of biological organization. Yet, except in very particular manifestations, even their formulation is elusive. They seem beyond the purview not only of reductionist experimental approaches, but also of traditional systems-oriented theoretical perspectives.

Can contemporary systems-science, with its integration of communications, computation, and control, do better? In particular, does it make possible a "unified" treatment of such coherence problems? I believe that significant conceptual and technical reorientation will be necessary. Drawing on a number of examples, I will highlight some of the potentially creative tensions between biological modes of coherence and the perspectives of contemporary systems-science, and will suggest how these tensions can serve as signposts to the needed reorientation.

Controlling Hybrid Systems: From Theory to Application Manfred Morari, ETH Zurich

Theory, computation and applications define the evolution of the field of control. This premise is first illustrated with some historical examples and then with the emerging area of hybrid systems. Many practical problems can be formulated in the hybrid system framework. Power electronics are hybrid systems by their very nature, systems with hard bounds and/or friction can be described in this manner and problems from other domains, as diverse as driver assistance systems, anaesthesia and active vibration control can be put in this form. We will highlight the theoretical developments and mention the extensive software that helps to bring the theory to bear on the practical examples. We will close with an outlook for hybrid systems and control more generally.

When will we be able to verify real hybrid systems? Bruce Krogh, Carnegie-Mellon University

Formal verification of discrete-state systems, particularly model checking, is now a standard tool in the design flow for digital circuits. In contrast, applications of hybrid system verification thus far have been only "proofs of concept" carried out by hybrid systems researchers rather than domain experts. What needs to happen for hybrid system verification to become a useful tool in the design of real systems? To address this question, we will first review how discrete-state model checking made the transition from research to engineering practice. We will then consider some barriers that need to be overcome for hybrid system verification to become part of the design flow in three target applications: automobiles, airplanes, and analog circuits. Finally, we will ask if there are particular research directions that may be fruitful in addressing these barriers.