2008 project summary

From VaVMURI

Jump to: navigation, search

Contents

This is an edited, HTML version of the annual project summary submitted to AFOSR on 24 Jul 08.

Abstract

This project is aimed at developing a common framework and the requisite theory for formal analysis and reasoning about continuous controllers, dynamical systems and concurrent, loosely synchronized supervisory control structures. We are extending existing work in graph grammars and sum of squares certificates to allow temporal logic statements and verification of semi-algebraic conditions (including stability and performance) to coexist. Work in the second year of this project has focused on increased integration of temporal logic into stability and performance analysis of dynamical systems, continued development of tools for analysis of stochastic systems, and development of tools for analyzing networked and hybrid systems.

Accomplishments

Graph Grammars

A significant challenge in the development of tools for distributed embedded systems is the relationship between different entities in the system and the (asynchronous) information flow through the system. A major avenue of exploration within our project is the use {\em graph grammars} to specify interaction rules, which we have recently adapted to the setting of cooperative control.

In~\cite{mke07-hscc} we show how Embedded Graph Grammars (EGGs) are used to specify local interaction rules between mobile robots in a natural manner. This formalism allows us to treat local network topologies, geometric transition conditions, and individual robot dynamics and control modes in a unified framework. An example EGG is demonstrated that achieves sensor coverage in a provably stable and correct manner. The algorithm results in a global network with a lattice-like triangulation.

In~\cite{mk08-acc} we consider a network of mobile agents in an initially unknown acyclic network configuration and the problem of reconfiguring them into a desired network topology and formation geometry while maintaining connectivity in an asynchronous network. We model the system and solution as an embedded graph grammar and use a method of lexicographically ordered Lyapunov functions to show the system converges non-deterministically regardless of the initial network structure and the order of communication events.

Stability of Systems Using Temporal Logic

We are working to develop temporal logic specifications of control concepts such as convergence, stability and performance. As a starting point, we have focused on developing theory and tools for formal reasoning of distributed systems with loosely synchronized supervisory structures. These tools (including automatic theorem proving systems and model checkers) are being used for verifying goal-oriented supervisory control programs as well as networked command and control protocols.

Verification of partially synchronous distributed systems is difficult because of inherent concurrency and the potentially large state space of the channels. In~\cite{CMP08-formats} we identify a subclass of such systems for which convergence properties can be verified based on the proof of convergence for the corresponding discrete-time shared state system. The proof technique extends to a class of partially synchronous systems in which an agent's state also evolves continuously over time. The proof technique has been formalized in the PVS interface for timed I/O automata and applied to verify convergence of a mobile agent pattern formation algorithm. In~\cite{MC08-tphols}, we formalize a theory proposed by Tsitsiklis for verifying stability or convergence of automata. We build on the existing PVS metatheory for untimed, timed, and hybrid input/output automata, and incorporate the concepts about fairness, stability, Lyapunov-like functions, and convergence. The resulting theory provides two sets of sufficient conditions, which when instantiated and verified for particular automata, guarantee convergence and stability, respectively.

We have also begun to use tools from temporal logic to verify performance of complex, asynchronous systems such as the control logic in autonomous vehicles. In~\cite{wm08-ivcs} we present an approach that allows mission and contingency management to be achieved in a distributed and dynamic manner without any central control over multiple software modules. This approach comprises two key elements---a mission management subsystem and a Canonical Software Architecture (CSA) for a planning subsystem. The mission management subsystem works in conjunction with the planning subsystem to dynamically replan in reaction to contingencies. The CSA ensures the consistency of the states of all the software modules in the planning subsystem. System faults are identified and replanning strategies are performed distributedly in the planning and the mission management subsystems through the CSA. The approach has been implemented and tested on Alice, an autonomous vehicle developed by the California Institute of Technology for the 2007 DARPA Urban Challenge.

Analysis of Stochastic Systems

DoD applications operate in environments that are unpredictable. In much of the literature on distributed systems, uncertainty is modeled by Byzantine processes (representing adversaries) or by discrete probabilistic models (such as models of component failure); these models are inadequate for the design of continuous control for multi-agent systems. The design of distributed algorithms in computer science is based on global constructs such as system invariants or on local constructs such as process knowledge. Both system invariants and process knowledge, as treated in the literature, are deterministic discrete constructs. We are therefore working to extend these concepts to the probabilistic continuous domain, by extending both SOS methods and graph grammars to apply to probabilistic systems.

Stochastic games are an important class of problems that generalize Markov decision processes to game theoretic scenarios. In~\cite{SP08-tac}, we consider finite state two-player zero-sum stochastic games over an infinite time horizon with discounted rewards. The players are assumed to have infinite strategy spaces and the payoffs are assumed to be polynomials. In this paper we restrict our attention to a special class of games for which the single-controller assumption holds. It is shown that minimax equilibria and optimal strategies for such games may be obtained via semidefinite programming.

In~\cite{TK08-acc} we consider the problem of finding reduced models of stochastic processes. We use Wasserstein pseudometrics to quantify the difference between processes. The method proposed in this paper is applicable to any continuous-time stochastic process with output, and pseudometrics between processes are defined only in terms of the available outputs. We demonstrate how to approximate a wide class of behavioral pseudometrics and how to optimize parameter values to minimize Wasserstein pseudometrics between processes. In particular, we introduce an algorithm that allows for the approximation of Wasserstein pseudometrics from sampled data, even in the absence of models for the processes.

Hybrid and Networked Systems

A key challenge in network-centric systems is verifying system properties in a distributed environment, where events can occur asynchronously and different agents can have different views of the state of the environment, depending on the information that they have available. In addition, many of these systems are hybrid systems, with a combination of communication protocols, layered decision-making systems, and complex dynamical behavior.

In~\cite{SP08-cdc} we employ the theory of partially ordered sets to model and analyze a class of decentralized control problems. We show that posets provide a natural way of modeling problems where communication constraints between subsystems have a hierarchical structure. We show that such problems have appealing algebraic properties that can be exploited to parameterize the set of stabilizing controllers. While much of the work is devoted to problems where the plant and controller have identical communication constraints, we also generalize our theory to case where they may have different communication constraints.

In~\cite{AP08-cdc}, we relax the monotonicity requirement of Lyapunov's theorem to enlarge the class of functions that can provide certificates of stability. To this end, we propose two new sufficient conditions for global asymptotic stability that allow the Lyapunov functions to increase locally, but guarantee an average decrease every few steps. Our first condition is non-convex, but allows an intuitive interpretation. The second condition, which includes the first one as a special case, is convex and can be cast as a semidefinite program. We show that when non-monotonic Lyapunov functions exist, one can construct a more complicated function that decreases monotonically. We demonstrate the strength of our methodology over standard Lyapunov theory through examples from three different classes of dynamical systems. First, we consider polynomial dynamics where we utilize techniques from sum-of-squares programming. Second, analysis of piecewise affine systems is performed. Here, connections to the method of piecewise quadratic Lyapunov functions are made. Finally, we examine systems with arbitrary switching between a finite set of matrices. It will be shown that tighter bounds on the joint spectral radius can be obtained using our technique.

Fault tolerance and safety verification of control systems that have state variable estimation uncertainty are essential for the success of autonomous robotic systems. A software control architecture called Mission Data System, developed at the Jet Propulsion Laboratory, uses goal networks as the control program for autonomous systems. Certain types of goal networks can be converted into linear hybrid systems and verified for safety using existing symbolic model checking software. In~\cite{BM08-acc}, we present a process for calculating the probability of failure of certain classes of verifiable goal networks due to state estimation uncertainty. A verifiable example task is presented and the failure probability of the control program based on estimation uncertainty is found.

References

  • A partial order approach to decentralized control. P. Shah and P. A. Parrilo. In Proc. IEEE Control and Decision Conference, 2008. To appear. pdf

Newly submitted papers (Oct 08)

Retrieved from "http://fedelm.cds.caltech.edu../../../../articles/2/0/0/2008_project_summary.html"
Personal tools