Murray Wiki - User contributions [en]

File:Parrilo introcomp-15aug06.pdf

2006-08-17T05:33:56Z

Parrilo:

Connections II

2006-08-07T23:25:52Z

Parrilo: /* Confirmed speakers */

<table align=center width=100%>
<tr>
<td rowspan=3 align=center>[[Image:citlogo.png|75px]]</td>
<td align=center>Connections II:</td>
<td rowspan=3 align=center>[[Image:afosrlogo.png|85px]]</td>
<tr><td align=center> Fundamentals of Network Science</td>
<tr><td align=center>14-18 August 2006 Pasadena, CA</td>
</table>


{| width=100% border = 1
|-
| width=20% align=center | [[#agenda|Agenda]]
| width=20% align=center | [http://www.cds.caltech.edu/~murray/connections/register.html Register]
| width=20% align=center | Participants
| width=20% align=center | [[Connections_II_travel|Travel Info]]
| width=20% align=center | [http://www.cds.caltech.edu CDS Home]
|} __NOTOC__

== Description ==

The ''Connections'' workshop series pulls together researchers in mathematics,
science and engineering who bring together novel ideas and tools from
outside their traditional training to influence problems in areas as diverse
as networking protocols, systems biology, ecology, geophysics, finance,
fluid mechanics, and multiscale physics. An underlying theme of this
workshop is to look forward to ways in which future scientists can be
educated in mathematical, computational, and quantitative methods, to
prepare them to interact broadly from the time they are students and
throughout their academic careers.

The first Connections workshop, held at Caltech in July 2004, brought
together over 200 researchers in the fields of mathematics, biology,
physics, engineering and other disciplines to participate in a 3 day
conference exploring the connections between diverse applications and common
underlying mathematics, particularly with regard to the role of uncertainty
and robustness in complex systems. For the second Connections workshop, we
plan to focus on the connections within the mathematics that would form the
foundation of a theoretical framework for network science, still motivated
by the diverse applications in science and technology that were focus of
Connections I.

We are organizing the activities around three main themes (roughly one each
day) of Hard Limits, Short Proofs, and Small Models, together with the
crosscutting theme of Architecture:

* ''Hard limits'' - a major challenge in network science is to understand the fundamental limits on networks due to their components and their interconnection. One challenge is unifying and extending the previously fragmented hard limit theories that arise in thermodynamics, control, communications, and computing, and are often associated with the names Carnot, Bode, Shannon, and Turing. There are encouraging pairwise connections, like the Bode-Shannon theory developed by Martins et al and others, and this theme will explore the progress and potential for further integration. Also encouraging is the opportunity for overcoming hard limits when new connections are made, such as the relationship between proof complexity and problem fragility.

* ''Short proofs'' - in general, overcoming the apparent computational intractability of analysis and design of complex networks is a central challenge, from formal verification of programs and protocols to the robustness analysis of the dynamics of biological networks and advanced technologies. Here the apparent asymmetry between NP/coNP is as significant as that between P/NP, and moving from analysis to synthesis involves higher complexity classes in fundamental ways. Substantial progress has been made recently in creating frameworks to systematically search for short proofs, but the research communities involved and the results are again somewhat fragmented. Fortunately there is also encouraging progress in creating a more unified framework, motivated by new connections within mathematics, the pervasive role of duality, and the concept of "complexity implies fragility" from the first theme.

* ''Small models'' - an important route to short proofs is finding small models of complex phenomena through model identification from data, and model reduction. Again, there has been substantial recent progress within relatively fragmented research communities, with encouraging results that suggest the potential for a richer and more unified framework.

* ''Architecture'' - a cross-cutting theme in the background throughout the workshop will be the challenge of a theory of ''architecture,'' as in the claim that "the architecture of the cell and the Internet have enabled their robustness and evolvability." Despite its widespread usage, there is little formalization of the concept and essentially no theory. The existing hard limits theories all assume architectures a priori which are incompatible and incomparable, and thus offer little guidance in the tradeoffs associated with architecture design. Short proofs and small models also arise only in the context of a priori specified proof and modeling architectures. A diverse set of examples of successful and unsuccessful architectures in technology and biology are now available, and motivate the study of a theory. More unified theories of hard limits, short proofs, and small models appear to be essential first steps towards a theory of architecture.

== Confirmed speakers ==

* Samuel Buss, University of California, San Diego
* Mung Chiang, Princeton University
* John Doyle, California Institute of Technology
* Keith Glover, Cambridge University
* Bill Helton, University of California at San Diego
* Mustafa Khammash, Univeristy of California, Santa Barbara
* Nuno Martins, U. Maryland
* Pablo Parrilo, Massuchusetts Institute of Technology
* Mihai Putinar, University of California, Santa Barbara
* Ben Recht, California Institute of Technology
* Lawrence Saul, University of California, San Diego
* Lin Xiao, Microsoft Research




{| width=100% border=1
|-
|
'''Monday''' - Tutorial sessions
* Schedule TBD: John Doyle, Maryam Fazel, Nuno Martins, Pablo Parrilo, Ben Recht.
|-
|
'''Tuesday''' - Hard Limits
{{agenda begin}}
{{agenda item|8:00a|Breakfast}}
{{agenda item|8:30a|John Doyle, Workshop Overview}}
{{agenda item| |Henrik Sandberg: Control and statistical mechanics}}
{{agenda item| |Nuno Martins: Communications and control}}
{{agenda item| |Lijun Chen: Wireless network capacity}}
{{agenda item|12:00p|Lunch}}
{{agenda item|1:00p|Mani Chandy: Computational complexity and model checking}}
{{agenda item| |Mustafa Khammash: Complexity of the chemical master equation}}
{{agenda item| |Maryam Fazel, Dennice Gayme, Xin Liu: Complexity implies fragility}}
{{agenda item| |John Doyle: Recap and wrapup}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Reception and cocktails}}
{{agenda item|7:30p|Dinner presentation: Christina Smolke: Regulatory mechanisms in natural and synthetic biology}}
{{agenda end}}

|-
|
'''Wednesday''' - Short Proofs
{{agenda begin}}
{{agenda item|8:30a|Breakfast}}
{{agenda item|9:00a|Pablo Parrilo, Day Overview}}
{{agenda item| |Bill Helton: Scale-independent proofs in systems and control}}
{{agenda item| |Samuel Buss: Proof systems}}
{{agenda item| |Mihai Putinar: Polynomial proofs and operator theory}}
{{agenda item|12:00p|Lunch}}
{{agenda item| 1:00p|Mung Chiang: Layering and duality}}
{{agenda item| |Bart Selman/ Carla Gomes: SAT Solvers and state of the art}}
{{agenda item| |Doyle/Parrilo: Recap and wrapup}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Reception and cocktails}}
{{agenda item|7:00p|Dinner presentation: Neil Gershenfeld: Math as computer programming}}
{{agenda end}}

|-
|
'''Thursday''' - Small Models
{{agenda begin}}
{{agenda item|8:30a|Breakfast}}
{{agenda item|9:00a|Ben Recht, Lin Xiao: Day Overview}}
{{agenda item| |Lawrence Saul, Spectral methods in machine learning}}
{{agenda item| |Keith Glover, Model reduction and system ID}}
{{agenda item|12:00p|Lunch}}
{{agenda item|1:00p|Antonis Papachristodoulou: Scalable proof for networking}}
{{agenda item| |Ali Jadbabaie, Sanjay Lall: Networks and decentralized control}}
{{agenda item| |Ben Recht, Lin Xiao: Convex optimization approaches}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Social event: Dinner at Dabney Lounge}}
{{agenda end}}

|-
|
'''Friday''' - Student talks
* Schedule TBD
|}

== Additional Information ==

The main workshop will be held on 15-17 August 2006 in Pasadena, CA, with additional sessions on Monday and Friday for interested participants:

* Monday: tutorial sessions
* Tuesday: Hard Limits
* Wednesday: Short Proofs
* Thursday: Small Models
* Friday: student presentations 
* [http://www.cds.caltech.edu/~murray/connections/register.html Register to attend] 
* [[Connections II Participants|Participants (restricted page)]]

The Connections workshop is sponsored by Caltech and the Air Force Office of Scientific Research.

Connections II

2006-08-03T05:21:02Z

Parrilo: /* Confirmed speakers */

<table align=center width=100%>
<tr>
<td rowspan=3 align=center>[[Image:citlogo.png|75px]]</td>
<td align=center>Connections II:</td>
<td rowspan=3 align=center>[[Image:afosrlogo.png|85px]]</td>
<tr><td align=center> Fundamentals of Network Science</td>
<tr><td align=center>14-18 August 2006 Pasadena, CA</td>
</table>


{| width=100% border = 1
|-
| width=20% align=center | [[#agenda|Agenda]]
| width=20% align=center | [http://www.cds.caltech.edu/~murray/connections/register.html Register]
| width=20% align=center | Participants
| width=20% align=center | [[Connections_II_travel|Travel Info]]
| width=20% align=center | [http://www.cds.caltech.edu CDS Home]
|} __NOTOC__

== Description ==

The ''Connections'' workshop series pulls together researchers in mathematics,
science and engineering who bring together novel ideas and tools from
outside their traditional training to influence problems in areas as diverse
as networking protocols, systems biology, ecology, geophysics, finance,
fluid mechanics, and multiscale physics. An underlying theme of this
workshop is to look forward to ways in which future scientists can be
educated in mathematical, computational, and quantitative methods, to
prepare them to interact broadly from the time they are students and
throughout their academic careers.

The first Connections workshop, held at Caltech in July 2004, brought
together over 200 researchers in the fields of mathematics, biology,
physics, engineering and other disciplines to participate in a 3 day
conference exploring the connections between diverse applications and common
underlying mathematics, particularly with regard to the role of uncertainty
and robustness in complex systems. For the second Connections workshop, we
plan to focus on the connections within the mathematics that would form the
foundation of a theoretical framework for network science, still motivated
by the diverse applications in science and technology that were focus of
Connections I.

We are organizing the activities around three main themes (roughly one each
day) of Hard Limits, Short Proofs, and Small Models, together with the
crosscutting theme of Architecture:

* ''Hard limits'' - a major challenge in network science is to understand the fundamental limits on networks due to their components and their interconnection. One challenge is unifying and extending the previously fragmented hard limit theories that arise in thermodynamics, control, communications, and computing, and are often associated with the names Carnot, Bode, Shannon, and Turing. There are encouraging pairwise connections, like the Bode-Shannon theory developed by Martins et al and others, and this theme will explore the progress and potential for further integration. Also encouraging is the opportunity for overcoming hard limits when new connections are made, such as the relationship between proof complexity and problem fragility.

* ''Short proofs'' - in general, overcoming the apparent computational intractability of analysis and design of complex networks is a central challenge, from formal verification of programs and protocols to the robustness analysis of the dynamics of biological networks and advanced technologies. Here the apparent asymmetry between NP/coNP is as significant as that between P/NP, and moving from analysis to synthesis involves higher complexity classes in fundamental ways. Substantial progress has been made recently in creating frameworks to systematically search for short proofs, but the research communities involved and the results are again somewhat fragmented. Fortunately there is also encouraging progress in creating a more unified framework, motivated by new connections within mathematics, the pervasive role of duality, and the concept of "complexity implies fragility" from the first theme.

* ''Small models'' - an important route to short proofs is finding small models of complex phenomena through model identification from data, and model reduction. Again, there has been substantial recent progress within relatively fragmented research communities, with encouraging results that suggest the potential for a richer and more unified framework.

* ''Architecture'' - a cross-cutting theme in the background throughout the workshop will be the challenge of a theory of ''architecture,'' as in the claim that "the architecture of the cell and the Internet have enabled their robustness and evolvability." Despite its widespread usage, there is little formalization of the concept and essentially no theory. The existing hard limits theories all assume architectures a priori which are incompatible and incomparable, and thus offer little guidance in the tradeoffs associated with architecture design. Short proofs and small models also arise only in the context of a priori specified proof and modeling architectures. A diverse set of examples of successful and unsuccessful architectures in technology and biology are now available, and motivate the study of a theory. More unified theories of hard limits, short proofs, and small models appear to be essential first steps towards a theory of architecture.

== Confirmed speakers ==
* Samuel Buss, University of California, San Diego
* John Doyle, California Institute of Technology
* Keith Glover, Cambridge University
* Bill Helton, University of California at San Diego
* Mustafa Khammash, Univeristy of California, Santa Barbara
* Nuno Martins, U. Maryland
* Pablo Parrilo, Massuchusetts Institute of Technology
* Mihai Putinar, University of California, Santa Barbara
* Ben Recht, California Institute of Technology
* Lawrence Saul, University of California, San Diego
* Lin Xiao, Microsoft Research



{| width=100% border=1
|-
|
'''Monday''' - Tutorial sessions
* Schedule TBD: John Doyle, Maryam Fazel, Nuno Martins, Pablo Parrilo, Ben Recht.
|-
|
'''Tuesday''' - Hard Limits
{{agenda begin}}
{{agenda item|8:00a|Breakfast}}
{{agenda item|8:30a|John Doyle, Workshop Overview}}
{{agenda item| |Henrik Sandberg: Control and statistical mechanics}}
{{agenda item| |Nuno Martins: Communications and control}}
{{agenda item| |Lijun Chen: Wireless network capacity}}
{{agenda item|12:00p|Lunch}}
{{agenda item|1:00p|Mani Chandy: Computational complexity and model checking}}
{{agenda item| |Mustafa Khammash: Complexity of the chemical master equation}}
{{agenda item| |Maryam Fazel, Dennice Gayme, Xin Liu: Complexity implies fragility}}
{{agenda item| |John Doyle: Recap and wrapup}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Reception and cocktails}}
{{agenda item|7:30p|Dinner presentation: Christina Smolke: Regulatory mechanisms in natural and synthetic biology}}
{{agenda end}}

|-
|
'''Wednesday''' - Short Proofs
{{agenda begin}}
{{agenda item|8:30a|Breakfast}}
{{agenda item|9:00a|Pablo Parrilo, Day Overview}}
{{agenda item| |Bill Helton: Scale-independent proofs in systems and control}}
{{agenda item| |Samuel Buss: Proof systems}}
{{agenda item| |Mihai Putinar: Polynomial proofs and operator theory}}
{{agenda item|12:00p|Lunch}}
{{agenda item| 1:00p|Mung Chiang: Layering and duality}}
{{agenda item| |Bart Selman/ Carla Gomes: SAT Solvers and state of the art}}
{{agenda item| |Doyle/Parrilo: Recap and wrapup}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Reception and cocktails}}
{{agenda item|7:00p|Dinner presentation: Neil Gershenfeld: Math as computer programming}}
{{agenda end}}

|-
|
'''Thursday''' - Small Models
{{agenda begin}}
{{agenda item|8:30a|Breakfast}}
{{agenda item|9:00a|Ben Recht, Lin Xiao: Day Overview}}
{{agenda item| |Laurence Saul, Spectral methods in machine learning}}
{{agenda item| |Keith Glover, Model reduction and system ID}}
{{agenda item|12:00p|Lunch}}
{{agenda item|1:00p|Antonis Papachristodoulou: Scalable proof for networking}}
{{agenda item| |Ali Jadbabaie, Sanjay Lall: Networks and decentralized control}}
{{agenda item| |Ben Recht, Lin Xiao: Convex optimization approaches}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Social event: Dinner at Dabney Lounge}}
{{agenda end}}

|-
|
'''Friday''' - Student talks
* Schedule TBD
|}

== Additional Information ==

The main workshop will be held on 15-17 August 2006 in Pasadena, CA, with additional sessions on Monday and Friday for interested participants:

* Monday: tutorial sessions
* Tuesday: Hard Limits
* Wednesday: Short Proofs
* Thursday: Small Models
* Friday: student presentations 
* [http://www.cds.caltech.edu/~murray/connections/register.html Register to attend] 
* [[Connections II Participants|Participants (restricted page)]]

The Connections workshop is sponsored by Caltech and the Air Force Office of Scientific Research.

Connections II

2006-08-03T05:17:43Z

Parrilo:

<table align=center width=100%>
<tr>
<td rowspan=3 align=center>[[Image:citlogo.png|75px]]</td>
<td align=center>Connections II:</td>
<td rowspan=3 align=center>[[Image:afosrlogo.png|85px]]</td>
<tr><td align=center> Fundamentals of Network Science</td>
<tr><td align=center>14-18 August 2006 Pasadena, CA</td>
</table>


{| width=100% border = 1
|-
| width=20% align=center | [[#agenda|Agenda]]
| width=20% align=center | [http://www.cds.caltech.edu/~murray/connections/register.html Register]
| width=20% align=center | Participants
| width=20% align=center | [[Connections_II_travel|Travel Info]]
| width=20% align=center | [http://www.cds.caltech.edu CDS Home]
|} __NOTOC__

== Description ==

The ''Connections'' workshop series pulls together researchers in mathematics,
science and engineering who bring together novel ideas and tools from
outside their traditional training to influence problems in areas as diverse
as networking protocols, systems biology, ecology, geophysics, finance,
fluid mechanics, and multiscale physics. An underlying theme of this
workshop is to look forward to ways in which future scientists can be
educated in mathematical, computational, and quantitative methods, to
prepare them to interact broadly from the time they are students and
throughout their academic careers.

The first Connections workshop, held at Caltech in July 2004, brought
together over 200 researchers in the fields of mathematics, biology,
physics, engineering and other disciplines to participate in a 3 day
conference exploring the connections between diverse applications and common
underlying mathematics, particularly with regard to the role of uncertainty
and robustness in complex systems. For the second Connections workshop, we
plan to focus on the connections within the mathematics that would form the
foundation of a theoretical framework for network science, still motivated
by the diverse applications in science and technology that were focus of
Connections I.

We are organizing the activities around three main themes (roughly one each
day) of Hard Limits, Short Proofs, and Small Models, together with the
crosscutting theme of Architecture:

* ''Hard limits'' - a major challenge in network science is to understand the fundamental limits on networks due to their components and their interconnection. One challenge is unifying and extending the previously fragmented hard limit theories that arise in thermodynamics, control, communications, and computing, and are often associated with the names Carnot, Bode, Shannon, and Turing. There are encouraging pairwise connections, like the Bode-Shannon theory developed by Martins et al and others, and this theme will explore the progress and potential for further integration. Also encouraging is the opportunity for overcoming hard limits when new connections are made, such as the relationship between proof complexity and problem fragility.

* ''Short proofs'' - in general, overcoming the apparent computational intractability of analysis and design of complex networks is a central challenge, from formal verification of programs and protocols to the robustness analysis of the dynamics of biological networks and advanced technologies. Here the apparent asymmetry between NP/coNP is as significant as that between P/NP, and moving from analysis to synthesis involves higher complexity classes in fundamental ways. Substantial progress has been made recently in creating frameworks to systematically search for short proofs, but the research communities involved and the results are again somewhat fragmented. Fortunately there is also encouraging progress in creating a more unified framework, motivated by new connections within mathematics, the pervasive role of duality, and the concept of "complexity implies fragility" from the first theme.

* ''Small models'' - an important route to short proofs is finding small models of complex phenomena through model identification from data, and model reduction. Again, there has been substantial recent progress within relatively fragmented research communities, with encouraging results that suggest the potential for a richer and more unified framework.

* ''Architecture'' - a cross-cutting theme in the background throughout the workshop will be the challenge of a theory of ''architecture,'' as in the claim that "the architecture of the cell and the Internet have enabled their robustness and evolvability." Despite its widespread usage, there is little formalization of the concept and essentially no theory. The existing hard limits theories all assume architectures a priori which are incompatible and incomparable, and thus offer little guidance in the tradeoffs associated with architecture design. Short proofs and small models also arise only in the context of a priori specified proof and modeling architectures. A diverse set of examples of successful and unsuccessful architectures in technology and biology are now available, and motivate the study of a theory. More unified theories of hard limits, short proofs, and small models appear to be essential first steps towards a theory of architecture.

== Confirmed speakers ==
* John Doyle, California Institute of Technology
* Keith Glover, Cambridge University
* Jean Carlson, Univeristy of California, Santa Barbara 
* Lawrence Saul, UC San Diego
* Pablo Parrilo, Massuchusetts Insttute of Technology
* Nuno Martins, U. Maryland
* Ben Recht, California Institute of Technology
* Lin Xiao, Microsoft Research



{| width=100% border=1
|-
|
'''Monday''' - Tutorial sessions
* Schedule TBD: John Doyle, Maryam Fazel, Nuno Martins, Pablo Parrilo, Ben Recht.
|-
|
'''Tuesday''' - Hard Limits
{{agenda begin}}
{{agenda item|8:00a|Breakfast}}
{{agenda item|8:30a|John Doyle, Workshop Overview}}
{{agenda item| |Henrik Sandberg: Control and statistical mechanics}}
{{agenda item| |Nuno Martins: Communications and control}}
{{agenda item| |Lijun Chen: Wireless network capacity}}
{{agenda item|12:00p|Lunch}}
{{agenda item|1:00p|Mani Chandy: Computational complexity and model checking}}
{{agenda item| |Mustafa Khammash: Complexity of the chemical master equation}}
{{agenda item| |Maryam Fazel, Dennice Gayme, Xin Liu: Complexity implies fragility}}
{{agenda item| |John Doyle: Recap and wrapup}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Reception and cocktails}}
{{agenda item|7:30p|Dinner presentation: Christina Smolke: Regulatory mechanisms in natural and synthetic biology}}
{{agenda end}}

|-
|
'''Wednesday''' - Short Proofs
{{agenda begin}}
{{agenda item|8:30a|Breakfast}}
{{agenda item|9:00a|Pablo Parrilo, Day Overview}}
{{agenda item| |Bill Helton: Scale-independent proofs in systems and control}}
{{agenda item| |Samuel Buss: Proof systems}}
{{agenda item| |Mihai Putinar: Polynomial proofs and operator theory}}
{{agenda item|12:00p|Lunch}}
{{agenda item| 1:00p|Mung Chiang: Layering and duality}}
{{agenda item| |Bart Selman/ Carla Gomes: SAT Solvers and state of the art}}
{{agenda item| |Doyle/Parrilo: Recap and wrapup}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Reception and cocktails}}
{{agenda item|7:00p|Dinner presentation: Neil Gershenfeld: Math as computer programming}}
{{agenda end}}

|-
|
'''Thursday''' - Small Models
{{agenda begin}}
{{agenda item|8:30a|Breakfast}}
{{agenda item|9:00a|Ben Recht, Lin Xiao: Day Overview}}
{{agenda item| |Laurence Saul, Spectral methods in machine learning}}
{{agenda item| |Keith Glover, Model reduction and system ID}}
{{agenda item|12:00p|Lunch}}
{{agenda item|1:00p|Antonis Papachristodoulou: Scalable proof for networking}}
{{agenda item| |Ali Jadbabaie, Sanjay Lall: Networks and decentralized control}}
{{agenda item| |Ben Recht, Lin Xiao: Convex optimization approaches}}
{{agenda item|4:00p|Afternoon break}}
{{agenda item|6:30p|Social event: Dinner at Dabney Lounge}}
{{agenda end}}

|-
|
'''Friday''' - Student talks
* Schedule TBD
|}

== Additional Information ==

The main workshop will be held on 15-17 August 2006 in Pasadena, CA, with additional sessions on Monday and Friday for interested participants:

* Monday: tutorial sessions
* Tuesday: Hard Limits
* Wednesday: Short Proofs
* Thursday: Small Models
* Friday: student presentations 
* [http://www.cds.caltech.edu/~murray/connections/register.html Register to attend] 
* [[Connections II Participants|Participants (restricted page)]]

The Connections workshop is sponsored by Caltech and the Air Force Office of Scientific Research.

2005 MURI White Paper

2005-08-03T09:25:30Z

Parrilo: =Sum of Squares Techniques (Pablo, with John; 1 page)=

<table width=100% border=0>
<tr><td align=right>Return to [[2005 MURI Proposal]]
</table>
== Cover letter (optional) ==
* Not sure what to put here. Perhaps description of team? Assume this won't be read by anyone but program manager.

== Cover Page ==
* The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address

== Identification of the research and issues (Richard; 1/2 page) ==

We propose to develop a mathematical language for specification, design and verification of distributed, embedded systems that provides an analyzable framework for robust performance.

Our specific goals for this MURI are to:
# ''Develop common mathematical framework for analyzing distributed, hybrid systems.'' This framework will be able to handle a combination of continuous dynamics and temporal logic, building on our previous work in analysis of hybrid dynamical systems. This will require a significant extension of current work to include temporal logic and distributed computing. In addition, we believe that it will be important to include stochastic systems, extending work such as SOSTOOLS to include probabilistic analysis.
# ''Extend ideas from distributed/parallel computing to apply to dynamical systems.'' Concepts such as fairness, safety, progress and concurrency are not strongly linked with concepts such as dynamics, stability and performance in embedded systems. We plan to extend tools in distributed computing to allow for dynamic changes in behavior and provide methods for analyzing robustness to such changes. This includes incremental changes (evolution of the dynamic state), large changes (changes in mode or failure of a component) and probabalistic changes (noise, disturbances and other stochastic uncertainties).
# ''Move the handoff between handcrafted proofs and formal methods further upstream.'' A major theme of our work will be to show how to take currently handcrafted proofs and formal methods for verification and validation of embedded systems and move them to higher levels of complexity and abstraction. This will enable the design of increasingly complex systems without the need for huge amounts of iteration and Monte Carlo analysis to verify performance.
# ''Demonstrate the utility of these methods on problems in network centric environments.'' We will make use of two testbeds at Caltech for this purpose - the Caltech Multi-Vehicle Wireless Testbed (MVWT) and "Alice", our 2005 DARPA Grand Challenge entry. Alice provides a sophisticated embedded system environment that includes 5 Gb/s raw data rates from sensors, 12 high speed processing cores linked by 1 Gb/s ethernet and a complex set of tasks and environments for autonomous operations. The MVWT offers a simpler dynamic and computational environment, but allows cooperative control of multiple vehicles operating in a dynamic, uncertain and adversarial environment. In each case we propose to develop a collection of primitive operations which can be used to "program" the systems and provide automatically verified code that satisfies a given performance specification.

== Proposed technical approach ==

=== Background (Richard; 1/2 page) ===

DoD systems are becoming increasingly sophisticated as we seek to design, build, test and field systems that are capable of higher levels of decision making and stronger integration into C4ISR infrastructure. The command and control software required to implement such systems is increasingly complex and our ability to verify that a system meets its specifications and validate the proper operation of the system is fast becoming a bottleneck in deploying new capability.

A distributed, embedded control system requires a sophisticated supervisory control structure that not only switches between control modes, but also manages communication and information among UAVs, responds to commands, automatically generates tasks and subtasks, monitors the health of the system, and so on. However, current software engineering practice cannot produce large complex systems for which any substantial formal guarantees can be made. In fact, in software engineering, it is usually assumed that large systems ''will'' have bugs. Unfortunately, the enormous complexities of such systems coupled with the fact that they are embedded in a physical, often adversarial, world means that exhaustively testing them is essentially impossible. The cost of and time associated with developing software for these systems makes rapidly reconfiguring them to adapt to new scenarios impossible. This makes the entire infrastructure fragile and susceptible to failure and compromise.

We seek to address this situation through the development of new approaches for specifying, implementing and verifying command and control systems. We will build on two new areas of development over the past five years under AFOSR and other funding: sum-of-squares techniques for constructing proof certificates for hybrid systems and formal methods for analysis and design of distributed computation and control systems. New results in each of these areas are ripe for further development and integration as part of developing a mathematical framework for analyzing distributed, hybrid systems.

=== Sum of Squares Techniques (Pablo, with John; 1 page) ===

Sum of squares (SOS) based techniques constitute one of the most
comprehensive methodologies available for the algorithmic analysis of
uncertain dynamical systems, encompassing and subsuming many earlier
successful techniques. Though conceptually simple, SOS-based methods
are based on a combination of techniques from real algebraic geometry
and convex optimization, and provide a novel and powerful
generalization of duality-based methods.

In recent years, there have been a great number of exciting
applications of these techniques in many areas, ranging from
optimization and control to geometric theorem proving and quantum
information theory. In particular, in the Systems and Control area,
the methods have yielded novel analysis and design tools in areas such
as nonlinear stability, robustness analysis, and safety verification
for hybrid systems. Many known successful alternative approaches (such
as $\mu$ or IQCs) can be understood, combined, or reformulated as
particular cases of this general methodology.

Despite the many successes, there are several important issues that
remain to be improved upon for the successful application of the
techniques to large-scale heterogeneous, distributed systems. The most
pressing one is the need to incorporate in a solid mathematical
footing elements of temporal logic and/or concurrency. Most of the
current SOS applications in a dynamic context entail a transformation
(e.g., via loop invariants, Lyapunov, or barrier functions) to
semialgebraic questions. It is very desirable to have a direct, formal
path that connects directly the logic specification and the
corresponding certificates.

Furthermore, in the SOS framework, the system properties under
consideration (e.g., stability, safety, performance) are proved and
certified algebraically by multivariate polynomials identities, which
are obtained by numerical convex optimization. Among the difficulties
towards the scalability of SOS techniques, is the relative lack of
sophistication of the families of possible proof certificates in the
optimization, since the current approach utilizes a simple notion of
proof length directly related with the degree of the corresponding
polynomials. A different (but related) source of problems concerns the
exploitation of algebraic structure in the formulation of efficient
numerical methods for large-scale convex optimization problems.

To address these issues, we propose:

* Fully integrate elements of temporal logic and SOS-based verification of semialgebraic conditions. A possible step in this direction would be the formulation of differential algebra based analogues of the Positivstellansatz, to be used in a decision procedure for solution of differential systems.

* We propose to refine SOS methods, to allow for the efficient search over structured families of certificates. We will also explore the incorporation of human-computer interaction strategies from automatic theorem proving for help in guiding development of SOS-based proofs, as well as the use of libraries of already proven theorems (e.g., identical subsystems) and associated heuristics.

* Extend SOS-based methods to the analysis and verification of systems in an adversarial setting. A concrete starting point are continuous-state two player zero-sum games.

* Incorporate probabilistic notions, both at the specification level (e.g., "the property holds with 99% probability") as well as through randomized algorithms for the efficient solution of the underlying deterministic search and optimization problems.

=== Specification and Programming Languages (Eric, with Mani; 1 page) ===

Two of the PIs (E. Klavins and R. Murray) have recently designed a specification language called CCL (The Computation and Control Language) that is model loosely after UNITY (developed by M. Chandy for modeling parallel systems) and which bears a strong resemblance to Promela (part of the SPIN model-checker developed by G. Holtzmann, a collaborator on this project). The idea behind CCL is to allow the control engineer to specify a simple model of the behavior of the system and to specify and reason about correctness properties in temporal logic. In particular, CCL allows (1) a formal model of the environment to be included as part of the specification and (2) allows the user to specify a model of how synchronized the distributed control elements are to be with each other and the environment (for example, one could say that the frequency of their
clocks differs by no more than some small amount). Thus, the goal of CCL is to replace software engineering and testing with model-building, formal specification and proof.

Presently, there are many limitations to CCL (and of other systems that attempt to accomplish the same thing) that allow it to be used for only simple systems. First, the proofs in CCL are done by either by hand or with the help of a difficult to use theorem prover. Second, specifying and reasoning about a sophisticated set of continuous feedback control laws in CCL is difficult due to the fact that one typically uses a different tools to reason about concurrency
(e.g. model checking and theorem proving) than one uses to reason about dynamical systems (e.g. barrier functions and sum of squares). Third, incorporating stochastic elements, such as the probability of a component failure or of the behavior of an adversary, in a formal and tractable way is presently impossible.

We propose to improve the approach in several ways:

* We propose to simplify the language to disallow arbitrarily complex specifications. The PIs believe that a simple set of building blocks, each accompanied by a formal reasoning ''tactic'' will allow the "specification and proof" engineer to easily build and reason about systems without having to do one-of-a-kind proofs.

* We propose to develop a common framework for reasoning about continuous controllers, dynamical systems and concurrent, loosely synchronized supervisory control structures. The PIs believe that the tantalizing use of barrier functions in hybrid control structures can be extended to systems with the sophistication of those specified in CCL.

* We propose to extend our techniques to include probabilistic specifications. The state of the art in probabilistic model checking, for example, is presently to the point where simple systems can be reasoned about efficiently.

=== Testbeds (Richard; 1/2 page) ===

To test our methods and motivate new insights into their performance (and limitations), we plan to make use of two testbeds that have been developed at Caltech: the multi-vehicle wireless testbed and "Alice", an autonomous vehicle that will compete in the 2005 DARPA Grand Challenge. These systems represent complementary challenges that are very representative of those faced by designers of Air Force systems (and systems of systems).

==== MVWT ====

Over the past five years (under AFOSR DURIP and MURI funding), Caltech has built a testbed consisting of up to 18 mobile vehicles with embedded computing and communications capability for use in testing new approaches for command and control across dynamic networks. The system allows testing of a variety of communications-related technologies, including distributed command and control algorithms, dynamically reconfigurable network topologies, source coding for real-time transmission of data in lossy environments, and multi-network communications.

We propose to use the MVWT to demonstrate the ability to specify and verify cooperative control missions for multiple vehicles. We will do so by
building an ''automated specification and proof interface'' to the MVWT that implements our approach to building systems that exhibit complex behaviors. Sample tasks include cooperative surveillance, area denial (in adversarial environments), and dynamic reconfiguration in the presence of vehicle failures (full or partial).

==== Alice ====

As a second testbed, we will make use of the infrastructure we have developed over the past 2.5 years through our participation in the 2004 and 2005 DARPA Grand Challenge. Our current vehicle, which the students have named "Alice", has six cameras, 4 LADAR units, an inertial measurement unit (IMU), a GPS navigation system, and numerous internal temperature and vibration sensors. The
raw data rate for Alice is approximately 5 Gb/s, which must be processed and acted upon at rates of up to 100 Hz in order to insure safe operation at high driving speeds.

The control system for Alice makes use of a highly networked control architecture, with distributed data fusion to determine elevation maps (for the height of the terrain in front of the vehicle), multiple optimization-based controllers to plan possible routes forthe vehicle, and online modeling, fault management, and decision making to provide reliable and reconfigurable
operation. Eight onboard computers distribute the computational load, sharing information at mixed rates across a 1 Gb/s switched network. System specifications call for reliable operation in the presence of up to 1 computer failure and 2 sensor failures, requiring careful coordination between computational elements.

Alice is representative of the level of complexity of UAVs and other systems. The verification and validation of software for such systems is a major challenge and by testing our techniques on Alice, we will enhance the likelihood of transition to industry and government.

== Potential impact on DoD capabities (Richard; 1/2 page) ==

If successful, the techniques developed under this proposal will provide a fundamental understanding of how to design, implement and test complex, distributed command and control systems that can be used for mixed manned and unmanned environments. Specifically, we aim to develop as mathematical framework and specification/programming languages that allow formal analysis of performance and robustness of distributed systems. While these techniques will never elimininate the need for Monte Carlo simulations and test-based validation, they will narrow the gap between theory and implementation, allow more rapid (and more reliable) development of complex, distributed, embedded systems.

== Potential team and management plan (Richard; 1/4 page) ==

The team will consist of five co-PIs at three universities: Murray (PI), Chandy and Doyle at Caltech; Klavins at U. Washington, and Parrilo at MIT. This group has a history of joint work (Parrilo got his PhD from Caltech CDS working with Doyle and Klavins was a postdoc in Caltech CS working with Murray) and represents an excellent collaboration between researchers with expertise in control and dynamical systems, computer science, and applied mathematics.

In addition to the university researchers, we plan to team with the Laboratory for Reliable Software (LARS) at the Jet Propulsion Laboratory (JPL) and we will leverage ongoing research at Caltech sponsored by Boeing. We are also exploring linkages to SRI (the author of PVS, a theorem-proving environment) and Honeywell. In all cases, these partnerships will provide transition paths for the proposed research as well as insights into additional research challenges as the program develops.

The program will be led by Richard Murray at Caltech. Because of the tight collaboration between the co-PIs, we anticipate frequent joint meetings and workshops, as well as student and faculty visits between institutions.

== Summary of estimated costs (1/2 page) ==

We anticipate a budget of $1M/year, with approximately $600K to be spent at Caltech and $200K each at MIT and U. Washington. Funds will be used to support graduate students, postdoctoral scholars, and some faculty salary support. The experimental testbeds that will be used in the proposal have already been constructed using other funds.

== Curriculum vitae of key investigators ==

* '''Note:''' this section does '''not''' count against page limit
* Everyone should send Richard a 2 page CV to be included
** Chandy: missing
** Doyle: missing
** Klavins: received
** Murray: received
** Parillo: received

2005 MURI White Paper

2005-08-03T09:23:26Z

Parrilo: =Sum of Squares Techniques (Pablo, with John; 1 page)=

<table width=100% border=0>
<tr><td align=right>Return to [[2005 MURI Proposal]]
</table>
== Cover letter (optional) ==
* Not sure what to put here. Perhaps description of team? Assume this won't be read by anyone but program manager.

== Cover Page ==
* The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address

== Identification of the research and issues (Richard; 1/2 page) ==

We propose to develop a mathematical language for specification, design and verification of distributed, embedded systems that provides an analyzable framework for robust performance.

Our specific goals for this MURI are to:
# ''Develop common mathematical framework for analyzing distributed, hybrid systems.'' This framework will be able to handle a combination of continuous dynamics and temporal logic, building on our previous work in analysis of hybrid dynamical systems. This will require a significant extension of current work to include temporal logic and distributed computing. In addition, we believe that it will be important to include stochastic systems, extending work such as SOSTOOLS to include probabilistic analysis.
# ''Extend ideas from distributed/parallel computing to apply to dynamical systems.'' Concepts such as fairness, safety, progress and concurrency are not strongly linked with concepts such as dynamics, stability and performance in embedded systems. We plan to extend tools in distributed computing to allow for dynamic changes in behavior and provide methods for analyzing robustness to such changes. This includes incremental changes (evolution of the dynamic state), large changes (changes in mode or failure of a component) and probabalistic changes (noise, disturbances and other stochastic uncertainties).
# ''Move the handoff between handcrafted proofs and formal methods further upstream.'' A major theme of our work will be to show how to take currently handcrafted proofs and formal methods for verification and validation of embedded systems and move them to higher levels of complexity and abstraction. This will enable the design of increasingly complex systems without the need for huge amounts of iteration and Monte Carlo analysis to verify performance.
# ''Demonstrate the utility of these methods on problems in network centric environments.'' We will make use of two testbeds at Caltech for this purpose - the Caltech Multi-Vehicle Wireless Testbed (MVWT) and "Alice", our 2005 DARPA Grand Challenge entry. Alice provides a sophisticated embedded system environment that includes 5 Gb/s raw data rates from sensors, 12 high speed processing cores linked by 1 Gb/s ethernet and a complex set of tasks and environments for autonomous operations. The MVWT offers a simpler dynamic and computational environment, but allows cooperative control of multiple vehicles operating in a dynamic, uncertain and adversarial environment. In each case we propose to develop a collection of primitive operations which can be used to "program" the systems and provide automatically verified code that satisfies a given performance specification.

== Proposed technical approach ==

=== Background (Richard; 1/2 page) ===

DoD systems are becoming increasingly sophisticated as we seek to design, build, test and field systems that are capable of higher levels of decision making and stronger integration into C4ISR infrastructure. The command and control software required to implement such systems is increasingly complex and our ability to verify that a system meets its specifications and validate the proper operation of the system is fast becoming a bottleneck in deploying new capability.

A distributed, embedded control system requires a sophisticated supervisory control structure that not only switches between control modes, but also manages communication and information among UAVs, responds to commands, automatically generates tasks and subtasks, monitors the health of the system, and so on. However, current software engineering practice cannot produce large complex systems for which any substantial formal guarantees can be made. In fact, in software engineering, it is usually assumed that large systems ''will'' have bugs. Unfortunately, the enormous complexities of such systems coupled with the fact that they are embedded in a physical, often adversarial, world means that exhaustively testing them is essentially impossible. The cost of and time associated with developing software for these systems makes rapidly reconfiguring them to adapt to new scenarios impossible. This makes the entire infrastructure fragile and susceptible to failure and compromise.

We seek to address this situation through the development of new approaches for specifying, implementing and verifying command and control systems. We will build on two new areas of development over the past five years under AFOSR and other funding: sum-of-squares techniques for constructing proof certificates for hybrid systems and formal methods for analysis and design of distributed computation and control systems. New results in each of these areas are ripe for further development and integration as part of developing a mathematical framework for analyzing distributed, hybrid systems.

=== Sum of Squares Techniques (Pablo, with John; 1 page) ===

Sum of squares (SOS) based techniques constitute one of the most
comprehensive methodologies available for the algorithmic analysis of
uncertain dynamical systems, encompassing and subsuming many earlier
successful techniques. Though conceptually simple, SOS-based methods
are based on a combination of techniques from real algebraic geometry
and convex optimization, and provide a novel and powerful
generalization of duality-based methods.

In recent years, there have been a great number of exciting
applications of these techniques in many areas, ranging from
optimization and control to geometric theorem proving and quantum
information theory. In particular, in the Systems and Control area,
the methods have yielded novel analysis and design tools in areas such
as nonlinear stability, robustness analysis, and safety verification
for hybrid systems. Many known successful alternative approaches (such
as $\mu$ or IQCs) can be understood, combined, or reformulated as
particular cases of this general methodology.

Despite the many successes, there are several important issues that
remain to be improved upon for the successful application of the
techniques to large-scale heterogeneous, distributed systems. The most
pressing one is the need to incorporate in a solid mathematical
footing elements of temporal logic and/or concurrency. Most of the
current SOS applications in a dynamic context entail a transformation
(e.g., via loop invariants, Lyapunov, or barrier functions) to
semialgebraic questions. It is very desirable to have a direct, formal
path that connects directly the logic specification and the
corresponding certificates.

Furthermore, in the SOS framework, the system properties under
consideration (e.g., stability, safety, performance) are proved and
certified algebraically by multivariate polynomials identities, which
are obtained by numerical convex optimization. Among the difficulties
towards the scalability of SOS techniques, is the relative lack of
sophistication of the families of possible proof certificates in the
optimization, since the current approach utilizes a simple notion of
proof length directly related with the degree of the corresponding
polynomials. A different (but related) source of problems concerns the
exploitation of algebraic structure in the formulation of efficient
numerical methods for large-scale convex optimization problems.

To address these issues, we propose:

1. Fully integrate elements of temporal logic and SOS-based
verification of semialgebraic conditions. A possible step in this
direction would be the formulation of differential algebra based
analogues of the Positivstellansatz, to be used in a decision
procedure for solution of differential systems.

2. We propose to refine SOS methods, to allow for the efficient search
over structured families of certificates. We will also explore the
incorporation of human-computer interaction strategies from
automatic theorem proving for help in guiding development of
SOS-based proofs, as well as the use of libraries of already proven
theorems (e.g., identical subsystems) and associated heuristics.

3. Extend SOS-based methods to the analysis and verification of
systems in an adversarial setting. A concrete starting point are
continuous-state two player zero-sum games.

4. Incorporate probabilistic notions, both at the specification level
(e.g., "the property holds with 99% probability") as well as
through randomized algorithms for the efficient solution of the
underlying deterministic search and optimization problems.

=== Specification and Programming Languages (Eric, with Mani; 1 page) ===

Two of the PIs (E. Klavins and R. Murray) have recently designed a specification language called CCL (The Computation and Control Language) that is model loosely after UNITY (developed by M. Chandy for modeling parallel systems) and which bears a strong resemblance to Promela (part of the SPIN model-checker developed by G. Holtzmann, a collaborator on this project). The idea behind CCL is to allow the control engineer to specify a simple model of the behavior of the system and to specify and reason about correctness properties in temporal logic. In particular, CCL allows (1) a formal model of the environment to be included as part of the specification and (2) allows the user to specify a model of how synchronized the distributed control elements are to be with each other and the environment (for example, one could say that the frequency of their
clocks differs by no more than some small amount). Thus, the goal of CCL is to replace software engineering and testing with model-building, formal specification and proof.

Presently, there are many limitations to CCL (and of other systems that attempt to accomplish the same thing) that allow it to be used for only simple systems. First, the proofs in CCL are done by either by hand or with the help of a difficult to use theorem prover. Second, specifying and reasoning about a sophisticated set of continuous feedback control laws in CCL is difficult due to the fact that one typically uses a different tools to reason about concurrency
(e.g. model checking and theorem proving) than one uses to reason about dynamical systems (e.g. barrier functions and sum of squares). Third, incorporating stochastic elements, such as the probability of a component failure or of the behavior of an adversary, in a formal and tractable way is presently impossible.

We propose to improve the approach in several ways:

* We propose to simplify the language to disallow arbitrarily complex specifications. The PIs believe that a simple set of building blocks, each accompanied by a formal reasoning ''tactic'' will allow the "specification and proof" engineer to easily build and reason about systems without having to do one-of-a-kind proofs.

* We propose to develop a common framework for reasoning about continuous controllers, dynamical systems and concurrent, loosely synchronized supervisory control structures. The PIs believe that the tantalizing use of barrier functions in hybrid control structures can be extended to systems with the sophistication of those specified in CCL.

* We propose to extend our techniques to include probabilistic specifications. The state of the art in probabilistic model checking, for example, is presently to the point where simple systems can be reasoned about efficiently.

=== Testbeds (Richard; 1/2 page) ===

To test our methods and motivate new insights into their performance (and limitations), we plan to make use of two testbeds that have been developed at Caltech: the multi-vehicle wireless testbed and "Alice", an autonomous vehicle that will compete in the 2005 DARPA Grand Challenge. These systems represent complementary challenges that are very representative of those faced by designers of Air Force systems (and systems of systems).

==== MVWT ====

Over the past five years (under AFOSR DURIP and MURI funding), Caltech has built a testbed consisting of up to 18 mobile vehicles with embedded computing and communications capability for use in testing new approaches for command and control across dynamic networks. The system allows testing of a variety of communications-related technologies, including distributed command and control algorithms, dynamically reconfigurable network topologies, source coding for real-time transmission of data in lossy environments, and multi-network communications.

We propose to use the MVWT to demonstrate the ability to specify and verify cooperative control missions for multiple vehicles. We will do so by
building an ''automated specification and proof interface'' to the MVWT that implements our approach to building systems that exhibit complex behaviors. Sample tasks include cooperative surveillance, area denial (in adversarial environments), and dynamic reconfiguration in the presence of vehicle failures (full or partial).

==== Alice ====

As a second testbed, we will make use of the infrastructure we have developed over the past 2.5 years through our participation in the 2004 and 2005 DARPA Grand Challenge. Our current vehicle, which the students have named "Alice", has six cameras, 4 LADAR units, an inertial measurement unit (IMU), a GPS navigation system, and numerous internal temperature and vibration sensors. The
raw data rate for Alice is approximately 5 Gb/s, which must be processed and acted upon at rates of up to 100 Hz in order to insure safe operation at high driving speeds.

The control system for Alice makes use of a highly networked control architecture, with distributed data fusion to determine elevation maps (for the height of the terrain in front of the vehicle), multiple optimization-based controllers to plan possible routes forthe vehicle, and online modeling, fault management, and decision making to provide reliable and reconfigurable
operation. Eight onboard computers distribute the computational load, sharing information at mixed rates across a 1 Gb/s switched network. System specifications call for reliable operation in the presence of up to 1 computer failure and 2 sensor failures, requiring careful coordination between computational elements.

Alice is representative of the level of complexity of UAVs and other systems. The verification and validation of software for such systems is a major challenge and by testing our techniques on Alice, we will enhance the likelihood of transition to industry and government.

== Potential impact on DoD capabities (Richard; 1/2 page) ==

If successful, the techniques developed under this proposal will provide a fundamental understanding of how to design, implement and test complex, distributed command and control systems that can be used for mixed manned and unmanned environments. Specifically, we aim to develop as mathematical framework and specification/programming languages that allow formal analysis of performance and robustness of distributed systems. While these techniques will never elimininate the need for Monte Carlo simulations and test-based validation, they will narrow the gap between theory and implementation, allow more rapid (and more reliable) development of complex, distributed, embedded systems.

== Potential team and management plan (Richard; 1/4 page) ==

The team will consist of five co-PIs at three universities: Murray (PI), Chandy and Doyle at Caltech; Klavins at U. Washington, and Parrilo at MIT. This group has a history of joint work (Parrilo got his PhD from Caltech CDS working with Doyle and Klavins was a postdoc in Caltech CS working with Murray) and represents an excellent collaboration between researchers with expertise in control and dynamical systems, computer science, and applied mathematics.

In addition to the university researchers, we plan to team with the Laboratory for Reliable Software (LARS) at the Jet Propulsion Laboratory (JPL) and we will leverage ongoing research at Caltech sponsored by Boeing. We are also exploring linkages to SRI (the author of PVS, a theorem-proving environment) and Honeywell. In all cases, these partnerships will provide transition paths for the proposed research as well as insights into additional research challenges as the program develops.

The program will be led by Richard Murray at Caltech. Because of the tight collaboration between the co-PIs, we anticipate frequent joint meetings and workshops, as well as student and faculty visits between institutions.

== Summary of estimated costs (1/2 page) ==

We anticipate a budget of $1M/year, with approximately $600K to be spent at Caltech and $200K each at MIT and U. Washington. Funds will be used to support graduate students, postdoctoral scholars, and some faculty salary support. The experimental testbeds that will be used in the proposal have already been constructed using other funds.

== Curriculum vitae of key investigators ==

* '''Note:''' this section does '''not''' count against page limit
* Everyone should send Richard a 2 page CV to be included
** Chandy: missing
** Doyle: missing
** Klavins: received
** Murray: received
** Parillo: received

2005 MURI Proposal

2005-08-03T08:36:53Z

Parrilo: =Background Reading=

__NOTOC__
<center>
= Title TBD =

Richard Murray (PI), Mani Chandy, John Doyle, Eric Klavins, Pablo Parrilo
</center>

<table border=1 width=100%>
<tr valign=top><td width=60%>

===== Proposal Overview =====
* Topic: High Confidence Design for Distributed, Embedded Systems
* White paper deadline: 9 Aug 05 (Tue), 4 pm EDT
* Full proposal deadline: 3 Nov 05 (Thu), 4 pm EDT
<td width=40%>
===== Quick Links =====
* [http://www.onr.navy.mil/sci_tech/industrial/363/muri.asp Proposal Overview] (ONR)
* [http://www.onr.navy.mil/02/baa/docs/baa_05-017.pdf Complete Announcement] (pdf)
* [[#Topic Description|Topic Description]]
* [[#White Paper|White Paper Instructions]]
</table>

<table border=0 width=100%>
<tr valign=top><td width=50%>

== Meetings and Telecons ==

* [[MURI Telecon 2005-07-13]]
* [[MURI Telecon 2005-07-21]]
* [[MURI Telecon 2005-07-27]]
<td width=50%>

== Working Documents ==
* [[2005 MURI White Paper]]
</table>
<hr>

== Background Reading ==

* E. Klavins, R. Ghrist and D. Lipsky, [[Media:Kgl05-tac.pdf|A Grammatical Approach to Self-Organizing Robotic Systems]], Submitted ''IEEE T. Automatic Control'', 2005.

* S. Prajna, A. Papachristodoulou, P. Seiler, P.A. Parrilo, [[Media:SOSTOOLSandControlApplications.pdf|SOSTOOLS and its Control applications]], In Positive polynomials in Control, Lecture Notes in Control and Information Sciences, Vol. 312, pp. 273--292, Springer, 2005.

== Topic Description ==

'''High Confidence Design For Distributed, Embedded Systems'''

''Background'': Prescribed safety and security is a significant challenge for current flight management systems. Requirements, design, and test coverage and their quantification all significantly impact overall system quality, but extensive software test coverage is especially significant to development costs. For certain current systems, verification and validation (V&V) comprise over 50% of total development costs. This percentage will be even higher using current V&V strategies on emerging autonomous systems. Although traditional certification practices have historically produced sufficiently safe and reliable systems, they will not be cost effective for next-generation autonomous systems due to inherent size and complexity increases from added functionality. New methods in high confidence software combined with advances in systems engineering and the use of closed- loop feedback for active management of uncertainty provide new possibilities for fundamental research aimed at addressing these issues. These methods move beyond formal methods in computer science to incorporate dynamics and feedback as part of the system specification.

''Objective'': Develop new approaches to designing/developing distributed embedded systems to inherently promote high confidence, as opposed to design-then-test approaches as prescribed by the current V&V process. Proposing teams should focus on developing new design methods, analysis techniques, specification and integrated software development/test environments that will radically lower V&V costs for future mixed critical systems. The multidisciplinary team should include the necessary expertise in mathematics, software architectures, security, modeling and simulation, fault tolerant systems, and dynamics and control.

''Research Concentration Areas'': Areas of interest include, but are not limited to:
# formal reasoning about distributed, dynamic, feedback systems, including the application of temporal logic and other tools from computer science and mathematics to reason about real-time software. This applies to both cooperative and adversarial systems in distributed computational environments;
# development of relationships between system properties and test coverage to reduce the required testing and provide improved efficiency, including a mixture of automated testing and model-based reasoning to improve efficiency;
# development and analysis of architectures that provide behavior guarantees of online V&V. Extend current methods for built-in-test (BIT) to higher levels of abstraction, including the use of safety "wrappers" to insure that high performance code is replaced by safe code when online monitors are triggered;
# V&V aware architectures- techniques that are designed to generate software and systems that are easier to verify and validate. Manage V&V complexity instead of managing system functionality;
# multi-threaded control: new tools for reasoning about asynchronous, distributed processing common in multi-threaded computational environments; and
# approximate V&V-development of model-based approaches to V&V that make use of simplifying approximations to improve V&V efficiency. Develop relations of system analysis to the test vector generation to reduce/eliminate required testing.

''Impact'': Next-generation Unmanned Aerial Vehicles (UAVs) and unmanned space vehicles will require advanced mixed critical system attributes to enable safe autonomous operations. These emerging attributes will manifest themselves in all aspects of the system including requirements, system architectures, software algorithms, and hardware components. Development of new theory and algorithms for V&V will provide reduced development time and cost, improved system functionality, and increased robustness to uncertainty for new systems.

''Research Topic Chief'': Lt Col Sharon Heise, sharon.heise@afosr.af.mil, 703-696-7796

== White Paper ==

==== White Paper Format ====

A WHITE PAPER MAY BE SUBMITTED EITHER ELECTRONICALLY OR IN HARD COPY FORM. FOR ELECTRONIC (as relevant) AND HARD COPY SUBMISSION:
* Paper Size – 8.5 x 11 inch paper
* Margins – 1 inch
* Spacing – single
* Font – Times New Roman, 12 point
* Number of Pages – no more than four (4) single-sided pages (excluding cover letter, cover, and curriculum vitae). White papers exceeding the page limit may not be evaluated.
* Copies – one (1) original and two (2) copies (applies only to hard copy submission)

==== White Paper Content ====
* A one page cover letter (optional)
* Cover Page – The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address
* Identification of the research and issues
* Proposed technical approaches
* Potential impact on DoD capabilities
* Potential team and management plan
* Summary of estimated costs
* Curriculum vitae of key investigators

White papers should be sent to the attention of the responsible Research Topic Chief at the agency specified for the topic using the address provided in Section IV. 5. The white paper should provide sufficient information on the research being proposed (e.g. hypothesis, theories, concepts, approaches, data measurements and analysis, etc.) to allow for an assessment by a technical expert. It is not necessary for white papers to carry official institutional signatures.

2005 MURI Proposal

2005-08-03T08:35:42Z

Parrilo: =Background Reading=

__NOTOC__
<center>
= Title TBD =

Richard Murray (PI), Mani Chandy, John Doyle, Eric Klavins, Pablo Parrilo
</center>

<table border=1 width=100%>
<tr valign=top><td width=60%>

===== Proposal Overview =====
* Topic: High Confidence Design for Distributed, Embedded Systems
* White paper deadline: 9 Aug 05 (Tue), 4 pm EDT
* Full proposal deadline: 3 Nov 05 (Thu), 4 pm EDT
<td width=40%>
===== Quick Links =====
* [http://www.onr.navy.mil/sci_tech/industrial/363/muri.asp Proposal Overview] (ONR)
* [http://www.onr.navy.mil/02/baa/docs/baa_05-017.pdf Complete Announcement] (pdf)
* [[#Topic Description|Topic Description]]
* [[#White Paper|White Paper Instructions]]
</table>

<table border=0 width=100%>
<tr valign=top><td width=50%>

== Meetings and Telecons ==

* [[MURI Telecon 2005-07-13]]
* [[MURI Telecon 2005-07-21]]
* [[MURI Telecon 2005-07-27]]
<td width=50%>

== Working Documents ==
* [[2005 MURI White Paper]]
</table>
<hr>

== Background Reading ==

* E. Klavins, R. Ghrist and D. Lipsky, [[Media:Kgl05-tac.pdf|A Grammatical Approach to Self-Organizing Robotic Systems]], Submitted ''IEEE T. Automatic Control'', 2005.

* S. Prajna, A. Papachristodoulou, P.A. Parrilo,[[Media:SOSTOOLSandControlApplications.pdf|SOSTOOLS and its Control applications]], In Positive polynomials in Control, Lecture Notes in Control and Information Sciences, Vol. 312, pp. 273--292, Springer, 2005.

== Topic Description ==

'''High Confidence Design For Distributed, Embedded Systems'''

''Background'': Prescribed safety and security is a significant challenge for current flight management systems. Requirements, design, and test coverage and their quantification all significantly impact overall system quality, but extensive software test coverage is especially significant to development costs. For certain current systems, verification and validation (V&V) comprise over 50% of total development costs. This percentage will be even higher using current V&V strategies on emerging autonomous systems. Although traditional certification practices have historically produced sufficiently safe and reliable systems, they will not be cost effective for next-generation autonomous systems due to inherent size and complexity increases from added functionality. New methods in high confidence software combined with advances in systems engineering and the use of closed- loop feedback for active management of uncertainty provide new possibilities for fundamental research aimed at addressing these issues. These methods move beyond formal methods in computer science to incorporate dynamics and feedback as part of the system specification.

''Objective'': Develop new approaches to designing/developing distributed embedded systems to inherently promote high confidence, as opposed to design-then-test approaches as prescribed by the current V&V process. Proposing teams should focus on developing new design methods, analysis techniques, specification and integrated software development/test environments that will radically lower V&V costs for future mixed critical systems. The multidisciplinary team should include the necessary expertise in mathematics, software architectures, security, modeling and simulation, fault tolerant systems, and dynamics and control.

''Research Concentration Areas'': Areas of interest include, but are not limited to:
# formal reasoning about distributed, dynamic, feedback systems, including the application of temporal logic and other tools from computer science and mathematics to reason about real-time software. This applies to both cooperative and adversarial systems in distributed computational environments;
# development of relationships between system properties and test coverage to reduce the required testing and provide improved efficiency, including a mixture of automated testing and model-based reasoning to improve efficiency;
# development and analysis of architectures that provide behavior guarantees of online V&V. Extend current methods for built-in-test (BIT) to higher levels of abstraction, including the use of safety "wrappers" to insure that high performance code is replaced by safe code when online monitors are triggered;
# V&V aware architectures- techniques that are designed to generate software and systems that are easier to verify and validate. Manage V&V complexity instead of managing system functionality;
# multi-threaded control: new tools for reasoning about asynchronous, distributed processing common in multi-threaded computational environments; and
# approximate V&V-development of model-based approaches to V&V that make use of simplifying approximations to improve V&V efficiency. Develop relations of system analysis to the test vector generation to reduce/eliminate required testing.

''Impact'': Next-generation Unmanned Aerial Vehicles (UAVs) and unmanned space vehicles will require advanced mixed critical system attributes to enable safe autonomous operations. These emerging attributes will manifest themselves in all aspects of the system including requirements, system architectures, software algorithms, and hardware components. Development of new theory and algorithms for V&V will provide reduced development time and cost, improved system functionality, and increased robustness to uncertainty for new systems.

''Research Topic Chief'': Lt Col Sharon Heise, sharon.heise@afosr.af.mil, 703-696-7796

== White Paper ==

==== White Paper Format ====

A WHITE PAPER MAY BE SUBMITTED EITHER ELECTRONICALLY OR IN HARD COPY FORM. FOR ELECTRONIC (as relevant) AND HARD COPY SUBMISSION:
* Paper Size – 8.5 x 11 inch paper
* Margins – 1 inch
* Spacing – single
* Font – Times New Roman, 12 point
* Number of Pages – no more than four (4) single-sided pages (excluding cover letter, cover, and curriculum vitae). White papers exceeding the page limit may not be evaluated.
* Copies – one (1) original and two (2) copies (applies only to hard copy submission)

==== White Paper Content ====
* A one page cover letter (optional)
* Cover Page – The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address
* Identification of the research and issues
* Proposed technical approaches
* Potential impact on DoD capabilities
* Potential team and management plan
* Summary of estimated costs
* Curriculum vitae of key investigators

White papers should be sent to the attention of the responsible Research Topic Chief at the agency specified for the topic using the address provided in Section IV. 5. The white paper should provide sufficient information on the research being proposed (e.g. hypothesis, theories, concepts, approaches, data measurements and analysis, etc.) to allow for an assessment by a technical expert. It is not necessary for white papers to carry official institutional signatures.

File:SOSTOOLSandControlApplications.pdf

2005-08-03T08:34:32Z

Parrilo:

Murray.cds:Upload log

2005-08-03T08:34:32Z

Parrilo: uploaded "SOSTOOLSandControlApplications.pdf"

Below is a list of the most recent file uploads.
All times shown are server time (UTC).
<ul><li>08:34, 3 Aug 2005 [[User:Parrilo|Parrilo]] uploaded "[[:Image:SOSTOOLSandControlApplications.pdf|SOSTOOLSandControlApplications.pdf]]"</li>
<li>05:19, 18 Jul 2005 [[User:Murray|Murray]] uploaded "[[:Image:Kgl05-tac.pdf|Kgl05-tac.pdf]]" (Klavins, Ghrist, Lipsky paper)</li>
<li>22:56, 12 Aug 2004 [[User:Brian|Brian]] uploaded "[[:Image:C2_Block_Diagram_8_12.ppt|C2_Block_Diagram_8_12.ppt]]" (C2 Block Chart, 7/12/04)</li>
<li>22:35, 12 Aug 2004 [[User:Demetri|Demetri]] uploaded "[[:Image:MVWTII_Pos_GOTChA_081104.ppt|MVWTII_Pos_GOTChA_081104.ppt]]" (Positioning GOTCHA Aug 11th)</li>
<li>22:22, 12 Aug 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Tasks_Vehicle_12aug04.ppt|Tasks_Vehicle_12aug04.ppt]]"</li>
<li>04:11, 10 Aug 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:New_Bat.ppt|New_Bat.ppt]]"</li>
<li>22:19, 6 Aug 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Kellys_status.doc|Kellys_status.doc]]"</li>
<li>22:52, 5 Aug 2004 [[User:Demetri|Demetri]] uploaded "[[:Image:MVWT_Status_2004-08-05.ppt|MVWT_Status_2004-08-05.ppt]]" (Status chart Aug 5th)</li>
<li>18:12, 5 Aug 2004 [[User:Jgibbs|Jgibbs]] uploaded "[[:Image:MVWT_API.zip|MVWT_API.zip]]" (MVWT API and documentation )</li>
<li>17:28, 5 Aug 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Tasks_Vehicle_05aug04.ppt|Tasks_Vehicle_05aug04.ppt]]"</li>
<li>22:23, 28 Jul 2004 [[User:Brian|Brian]] uploaded "[[:Image:Design_Review_C2_Team.ppt|Design_Review_C2_Team.ppt]]" (C2 Design Review Presentation)</li>
<li>21:31, 28 Jul 2004 [[User:Xiong|Xiong]] uploaded "[[:Image:ArchitectureReview7_28.ppt|ArchitectureReview7_28.ppt]]" (Positioning Team Architecture Review)</li>
<li>19:13, 28 Jul 2004 [[User:Xiong|Xiong]] uploaded "[[:Image:ArchitectureReview7_28.ppt|ArchitectureReview7_28.ppt]]" (Positioning Team Architecture Review)</li>
<li>16:17, 28 Jul 2004 [[User:Xiong|Xiong]] uploaded "[[:Image:ArchitectureReview7_28.ppt|ArchitectureReview7_28.ppt]]" (Positioning Team Architecture Review )</li>
<li>00:05, 24 Jul 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Kellys_status.doc|Kellys_status.doc]]"</li>
<li>21:27, 23 Jul 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Kellys_status.doc|Kellys_status.doc]]"</li>
<li>21:26, 23 Jul 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Kellys_status.doc|Kellys_status.doc]]"</li>
<li>22:25, 22 Jul 2004 [[User:Davetung|Davetung]] uploaded "[[:Image:C2_Block_Diagram_7_22.ppt|C2_Block_Diagram_7_22.ppt]]" (C2 Block Diagram for 07-15-04 meeting)</li>
<li>22:09, 22 Jul 2004 [[User:Sutherla|Sutherla]] uploaded "[[:Image:Steelebots_status.doc|Steelebots_status.doc]]"</li>
<li>22:08, 22 Jul 2004 [[User:Sutherla|Sutherla]] uploaded "[[:Image:Steelebots_status.doc|Steelebots_status.doc]]"</li>
<li>22:00, 22 Jul 2004 [[User:Xiong|Xiong]] uploaded "[[:Image:SystemBlockDiagram7_22.ppt|SystemBlockDiagram7_22.ppt]]" (Positioning Team Block Diagram 7/22)</li>
<li>22:00, 22 Jul 2004 [[User:Xiong|Xiong]] uploaded "[[:Image:SystemBlockDiagram7_22.ppt|SystemBlockDiagram7_22.ppt]]" (Positioning Team Block Diagram 7/22)</li>
<li>18:53, 22 Jul 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Kelly_quickstart.pdf|Kelly_quickstart.pdf]]"</li>
<li>18:48, 22 Jul 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Tasks_Vehicle_22jul04.ppt|Tasks_Vehicle_22jul04.ppt]]"</li>
<li>18:34, 22 Jul 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Steelebots_status.doc|Steelebots_status.doc]]"</li>
<li>18:34, 22 Jul 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Kellys_status.doc|Kellys_status.doc]]"</li>
<li>18:34, 22 Jul 2004 [[User:Jzp|Jzp]] uploaded "[[:Image:Bats_status.doc|Bats_status.doc]]"</li>
<li>17:50, 22 Jul 2004 [[User:Jzp|Jzp]] uploaded \"[[:Image:MVWT_status_2004-07-22.ppt|MVWT_status_2004-07-22.ppt]]\"</li>
<li>05:43, 22 Jul 2004 [[User:Murray|Murray]] uploaded \"[[:Image:MVWT_status_2004-07-22.ppt|MVWT_status_2004-07-22.ppt]]\" (22 Jul 04 project meeting charts)</li>
<li>20:12, 17 Jul 2004 [[User:Murray|Murray]] uploaded \"[[:Image:MVWT_status_2004-07-15.ppt|MVWT_status_2004-07-15.ppt]]\" (15 Jul 04 meeting charts)</li>
<li>21:27, 12 Jul 2004 [[User:Shiling|Shiling]] uploaded \"[[:Image:C2_Block_Diagram_7_15.ppt|C2_Block_Diagram_7_15.ppt]]\" (C2_Block_Diagram_7_15)</li>
<li>22:55, 8 Jul 2004 [[User:Demetri|Demetri]] uploaded \"[[:Image:SystemBlockDiagram7_8.ppt|SystemBlockDiagram7_8.ppt]]\" (Posn Team Block Diagram Jul 8th)</li>
<li>21:39, 8 Jul 2004 [[User:Brian|Brian]] uploaded \"[[:Image:Notes_for_7-8_meeting.txt|Notes_for_7-8_meeting.txt]]\" (Notes for 7/8 Meeting)</li>
<li>20:36, 8 Jul 2004 [[User:Demetri|Demetri]] uploaded \"[[:Image:2004_07_07_16_15_47_mvwt6.data|2004_07_07_16_15_47_mvwt6.data]]\" (vision test data 2 (circle formation))</li>
<li>20:32, 8 Jul 2004 [[User:Demetri|Demetri]] uploaded \"[[:Image:2004_07_07_15_59_12_mvwt6.data|2004_07_07_15_59_12_mvwt6.data]]\" (vision test data 1 (circle formation))</li>
<li>05:18, 8 Jul 2004 [[User:Murray|Murray]] uploaded \"[[:Image:MVWT_status_2004-07-08.ppt|MVWT_status_2004-07-08.ppt]]\" (8 Jul 04 meeting charts)</li>
<li>21:27, 7 Jul 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_Block_Diagram_7_8.ppt|C2_Block_Diagram_7_8.ppt]]\" (Block Chart for 7-8 Meeting)</li>
<li>23:22, 1 Jul 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_Block_Diagram_7_1.ppt|C2_Block_Diagram_7_1.ppt]]\" (C2 Block Diagram 7/1)</li>
<li>22:11, 1 Jul 2004 [[User:Demetri|Demetri]] uploaded \"[[:Image:MVWTII_Pos_GOTChA_070104.ppt|MVWTII_Pos_GOTChA_070104.ppt]]\" (Positioning GOTCHA Jul 1st 2004)</li>
<li>21:55, 1 Jul 2004 [[User:Demetri|Demetri]] uploaded \"[[:Image:Rfid-feasibility.ppt|Rfid-feasibility.ppt]]\" (RFID Feasibility)</li>
<li>21:50, 1 Jul 2004 [[User:Demetri|Demetri]] uploaded \"[[:Image:SystemBlockDiagram7_1.ppt|SystemBlockDiagram7_1.ppt]]\" (Positioning Team Block Diagram July 1st, 2004)</li>
<li>05:59, 1 Jul 2004 [[User:Murray|Murray]] uploaded \"[[:Image:MVWT_status_2004-07-01.ppt|MVWT_status_2004-07-01.ppt]]\" (MVWT project meeting charts, 1 Jul 04)</li>
<li>02:25, 27 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:Murray-redeye.gif|Murray-redeye.gif]]\" (Richard Murray)</li>
<li>02:14, 27 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:Murray-redeye.gif|Murray-redeye.gif]]\" (Richard Murray)</li>
<li>01:39, 25 Jun 2004 [[User:Raktim|Raktim]] uploaded \"[[:Image:TI-HF-I-Midrange_Eval_Kit.tar.gz|TI-HF-I-Midrange_Eval_Kit.tar.gz]]\" (TI-HF-I-Midrange Development Kit)</li>
<li>01:20, 25 Jun 2004 [[User:Raktim|Raktim]] uploaded \"[[:Image:Skyetek_quote.pdf|Skyetek_quote.pdf]]\" (Price Quote for Readers from SkyeTek)</li>
<li>21:00, 24 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_Block_Diagram_6_24.ppt|C2_Block_Diagram_6_24.ppt]]\" (Reverted to earlier revision)</li>
<li>20:59, 24 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_Block_Diagram_6_24.ppt|C2_Block_Diagram_6_24.ppt]]\" (Reverted to earlier revision)</li>
<li>20:58, 24 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_Block_Diagram_6_24.ppt|C2_Block_Diagram_6_24.ppt]]\" (C2 Block Diagram, 6/24/04)</li>
<li>20:56, 24 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_Block_Diagram_6_24.ppt|C2_Block_Diagram_6_24.ppt]]\" (C2 Block Diagram, 6/24/04)</li>
<li>20:54, 24 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_Block_Diagram_6_24.ppt|C2_Block_Diagram_6_24.ppt]]\" (C2 Block Diagram, 6/24/04)</li>
<li>19:46, 24 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:MVWT_status-2004_06_24.ppt|MVWT_status-2004_06_24.ppt]]\" (MVWT meeting charts, 24 Jun 04)</li>
<li>22:08, 23 Jun 2004 [[User:Demetri|Demetri]] uploaded \"[[:Image:MVWTII_Pos_GOTChA_062404.jpg|MVWTII_Pos_GOTChA_062404.jpg]]\" (updated GOTChA 6/24/04)</li>
<li>21:44, 23 Jun 2004 [[User:Demetri|Demetri]] uploaded \"[[:Image:SystemBlockDiagram.jpg|SystemBlockDiagram.jpg]]\" (Posn team block diagram)</li>
<li>18:22, 23 Jun 2004 [[User:Dvangogh|Dvangogh]] uploaded \"[[:Image:EmbsysStatus2Mar04-small.JPG|EmbsysStatus2Mar04-small.JPG]]\" (Status Chart - embedded systems March 2004)</li>
<li>00:25, 23 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_Block_Diagram_6_24.ppt|C2_Block_Diagram_6_24.ppt]]\" (C2 Block Chart, 6/24/04)</li>
<li>22:47, 21 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:C2_GOTChA_Chart_6_24.ppt|C2_GOTChA_Chart_6_24.ppt]]\" (C2 GOTChA Chart, 6/24)</li>
<li>00:19, 21 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:Communications_Code_Summary_-_061804.pdf|Communications_Code_Summary_-_061804.pdf]]\" (Communications Code Summary, 6/18/04)</li>
<li>00:36, 20 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:CPMT_Timeline.jpg|CPMT_Timeline.jpg]]\" (Timeline chart, 19 Jun 04)</li>
<li>23:55, 19 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:Ccli-16jun04.pdf|Ccli-16jun04.pdf]]\" (NSF CCLI proposal)</li>
<li>23:15, 19 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:CPMT_Status_2004-06-19.jpg|CPMT_Status_2004-06-19.jpg]]\" (added additional links to industry)</li>
<li>22:56, 19 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:CPMT_Status_2004-06-19.jpg|CPMT_Status_2004-06-19.jpg]]\" (CPMT (DGC 75) status chart (revised))</li>
<li>20:23, 19 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:CPMT_Status_2004-06-19.jpg|CPMT_Status_2004-06-19.jpg]]\" (CPMT (DGC 75) status chart)</li>
<li>00:02, 19 Jun 2004 [[User:Jzp|Jzp]] uploaded \"[[:Image:GOTChA_Vehicle.ppt|GOTChA_Vehicle.ppt]]\" (First draft of the vehicle team GOTChA chart)</li>
<li>21:15, 18 Jun 2004 [[User:Brian|Brian]] uploaded \"[[:Image:Communications_Code_Summary_-_061804.wpd|Communications_Code_Summary_-_061804.wpd]]\" (Communications Protocol Description, 6/18/04)</li>
<li>05:10, 18 Jun 2004 [[User:Murray|Murray]] uploaded \"[[:Image:Kickoff-14jun04.ppt|Kickoff-14jun04.ppt]]\" (kickoff slides)</li>
<li>22:05, 15 Jun 2004 [[User:Jzp|Jzp]] uploaded \"[[:Image:Jzp_head.jpg|Jzp_head.jpg]]\"</li>

</ul>

2005 MURI Proposal

2005-08-03T08:33:54Z

Parrilo: =Background Reading=

__NOTOC__
<center>
= Title TBD =

Richard Murray (PI), Mani Chandy, John Doyle, Eric Klavins, Pablo Parrilo
</center>

<table border=1 width=100%>
<tr valign=top><td width=60%>

===== Proposal Overview =====
* Topic: High Confidence Design for Distributed, Embedded Systems
* White paper deadline: 9 Aug 05 (Tue), 4 pm EDT
* Full proposal deadline: 3 Nov 05 (Thu), 4 pm EDT
<td width=40%>
===== Quick Links =====
* [http://www.onr.navy.mil/sci_tech/industrial/363/muri.asp Proposal Overview] (ONR)
* [http://www.onr.navy.mil/02/baa/docs/baa_05-017.pdf Complete Announcement] (pdf)
* [[#Topic Description|Topic Description]]
* [[#White Paper|White Paper Instructions]]
</table>

<table border=0 width=100%>
<tr valign=top><td width=50%>

== Meetings and Telecons ==

* [[MURI Telecon 2005-07-13]]
* [[MURI Telecon 2005-07-21]]
* [[MURI Telecon 2005-07-27]]
<td width=50%>

== Working Documents ==
* [[2005 MURI White Paper]]
</table>
<hr>

== Background Reading ==

* E. Klavins, R. Ghrist and D. Lipsky, [[Media:Kgl05-tac.pdf|A Grammatical Approach to Self-Organizing Robotic Systems]], Submitted ''IEEE T. Automatic Control'', 2005.

* S. Prajna, A. Papachristodoulou, P.A. Parrilo, [[Media:|SOSTOOLS and its Control applications]], In Positive polynomials in Control, Lecture Notes in Control and Information Sciences, Vol. 312, pp. 273--292, Springer, 2005.

== Topic Description ==

'''High Confidence Design For Distributed, Embedded Systems'''

''Background'': Prescribed safety and security is a significant challenge for current flight management systems. Requirements, design, and test coverage and their quantification all significantly impact overall system quality, but extensive software test coverage is especially significant to development costs. For certain current systems, verification and validation (V&V) comprise over 50% of total development costs. This percentage will be even higher using current V&V strategies on emerging autonomous systems. Although traditional certification practices have historically produced sufficiently safe and reliable systems, they will not be cost effective for next-generation autonomous systems due to inherent size and complexity increases from added functionality. New methods in high confidence software combined with advances in systems engineering and the use of closed- loop feedback for active management of uncertainty provide new possibilities for fundamental research aimed at addressing these issues. These methods move beyond formal methods in computer science to incorporate dynamics and feedback as part of the system specification.

''Objective'': Develop new approaches to designing/developing distributed embedded systems to inherently promote high confidence, as opposed to design-then-test approaches as prescribed by the current V&V process. Proposing teams should focus on developing new design methods, analysis techniques, specification and integrated software development/test environments that will radically lower V&V costs for future mixed critical systems. The multidisciplinary team should include the necessary expertise in mathematics, software architectures, security, modeling and simulation, fault tolerant systems, and dynamics and control.

''Research Concentration Areas'': Areas of interest include, but are not limited to:
# formal reasoning about distributed, dynamic, feedback systems, including the application of temporal logic and other tools from computer science and mathematics to reason about real-time software. This applies to both cooperative and adversarial systems in distributed computational environments;
# development of relationships between system properties and test coverage to reduce the required testing and provide improved efficiency, including a mixture of automated testing and model-based reasoning to improve efficiency;
# development and analysis of architectures that provide behavior guarantees of online V&V. Extend current methods for built-in-test (BIT) to higher levels of abstraction, including the use of safety "wrappers" to insure that high performance code is replaced by safe code when online monitors are triggered;
# V&V aware architectures- techniques that are designed to generate software and systems that are easier to verify and validate. Manage V&V complexity instead of managing system functionality;
# multi-threaded control: new tools for reasoning about asynchronous, distributed processing common in multi-threaded computational environments; and
# approximate V&V-development of model-based approaches to V&V that make use of simplifying approximations to improve V&V efficiency. Develop relations of system analysis to the test vector generation to reduce/eliminate required testing.

''Impact'': Next-generation Unmanned Aerial Vehicles (UAVs) and unmanned space vehicles will require advanced mixed critical system attributes to enable safe autonomous operations. These emerging attributes will manifest themselves in all aspects of the system including requirements, system architectures, software algorithms, and hardware components. Development of new theory and algorithms for V&V will provide reduced development time and cost, improved system functionality, and increased robustness to uncertainty for new systems.

''Research Topic Chief'': Lt Col Sharon Heise, sharon.heise@afosr.af.mil, 703-696-7796

== White Paper ==

==== White Paper Format ====

A WHITE PAPER MAY BE SUBMITTED EITHER ELECTRONICALLY OR IN HARD COPY FORM. FOR ELECTRONIC (as relevant) AND HARD COPY SUBMISSION:
* Paper Size – 8.5 x 11 inch paper
* Margins – 1 inch
* Spacing – single
* Font – Times New Roman, 12 point
* Number of Pages – no more than four (4) single-sided pages (excluding cover letter, cover, and curriculum vitae). White papers exceeding the page limit may not be evaluated.
* Copies – one (1) original and two (2) copies (applies only to hard copy submission)

==== White Paper Content ====
* A one page cover letter (optional)
* Cover Page – The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address
* Identification of the research and issues
* Proposed technical approaches
* Potential impact on DoD capabilities
* Potential team and management plan
* Summary of estimated costs
* Curriculum vitae of key investigators

White papers should be sent to the attention of the responsible Research Topic Chief at the agency specified for the topic using the address provided in Section IV. 5. The white paper should provide sufficient information on the research being proposed (e.g. hypothesis, theories, concepts, approaches, data measurements and analysis, etc.) to allow for an assessment by a technical expert. It is not necessary for white papers to carry official institutional signatures.

2005 MURI White Paper

2005-08-03T08:24:57Z

Parrilo: =Identification of the research and issues (Richard; 1/2 page)=

<table width=100% border=0>
<tr><td align=right>Return to [[2005 MURI Proposal]]
</table>
== Cover letter (optional) ==
* Not sure what to put here. Perhaps description of team? Assume this won't be read by anyone but program manager.

== Cover Page ==
* The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address

== Identification of the research and issues (Richard; 1/2 page) ==

We propose to develop a mathematical language for specification, design and verification of distributed, embedded systems that provides an analyzable framework for robust performance.

Our specific goals for this MURI are to:
# ''Develop common mathematical framework for analyzing distributed, hybrid systems.'' This framework will be able to handle a combination of continuous dynamics and temporal logic, building on our previous work in analysis of hybrid dynamical systems. This will require a significant extension of current work to include temporal logic and distributed computing. In addition, we believe that it will be important to include stochastic systems, extending work such as SOSTOOLS to include probabilistic analysis.
# ''Extend ideas from distributed/parallel computing to apply to dynamical systems.'' Concepts such as fairness, safety, progress and concurrency are not strongly linked with concepts such as dynamics, stability and performance in embedded systems. We plan to extend tools in distributed computing to allow for dynamic changes in behavior and provide methods for analyzing robustness to such changes. This includes incremental changes (evolution of the dynamic state), large changes (changes in mode or failure of a component) and probabalistic changes (noise, disturbances and other stochastic uncertainties).
# ''Move the handoff between handcrafted proofs and formal methods further upstream.'' A major theme of our work will be to show how to take currently handcrafted proofs and formal methods for verification and validation of embedded systems and move them to higher levels of complexity and abstraction. This will enable the design of increasingly complex systems without the need for huge amounts of iteration and Monte Carlo analysis to verify performance.
# ''Demonstrate the utility of these methods on problems in network centric environments.'' We will make use of two testbeds at Caltech for this purpose - the Caltech Multi-Vehicle Wireless Testbed (MVWT) and "Alice", our 2005 DARPA Grand Challenge entry. Alice provides a sophisticated embedded system environment that includes 5 Gb/s raw data rates from sensors, 12 high speed processing cores linked by 1 Gb/s ethernet and a complex set of tasks and environments for autonomous operations. The MVWT offers a simpler dynamic and computational environment, but allows cooperative control of multiple vehicles operating in a dynamic, uncertain and adversarial environment. In each case we propose to develop a collection of primitive operations which can be used to "program" the systems and provide automatically verified code that satisfies a given performance specification.

== Proposed technical approach ==

=== Background (Richard; 1/2 page) ===

DoD systems are becoming increasingly sophisticated as we seek to design, build, test and field systems that are capable of higher levels of decision making and stronger integration into C4ISR infrastructure. The command and control software required to implement such systems is increasingly complex and our ability to verify that a system meets its specifications and validate the proper operation of the system is fast becoming a bottleneck in deploying new capability.

A distributed, embedded control system requires a sophisticated supervisory control structure that not only switches between control modes, but also manages communication and information among UAVs, responds to commands, automatically generates tasks and subtasks, monitors the health of the system, and so on. However, current software engineering practice cannot produce large complex systems for which any substantial formal guarantees can be made. In fact, in software engineering, it is usually assumed that large systems ''will'' have bugs. Unfortunately, the enormous complexities of such systems coupled with the fact that they are embedded in a physical, often adversarial, world means that exhaustively testing them is essentially impossible. The cost of and time associated with developing software for these systems makes rapidly reconfiguring them to adapt to new scenarios impossible. This makes the entire infrastructure fragile and susceptible to failure and compromise.

We seek to address this situation through the development of new approaches for specifying, implementing and verifying command and control systems. We will build on two new areas of development over the past five years under AFOSR and other funding: sum-of-squares techniques for constructing proof certificates for hybrid systems and formal methods for analysis and design of distributed computation and control systems. New results in each of these areas are ripe for further development and integration as part of developing a mathematical framework for analyzing distributed, hybrid systems.

=== Sum of Squares Techniques (Pablo, with John; 1 page) ===
* Provide a short (1-2 paragraph) background on current state of SoS
* Talk about what is lacking from current approach
* Give some insights into how we plan to approach this and desired results

=== Specification and Programming Languages (Eric, with Mani; 1 page) ===

Two of the PIs (E. Klavins and R. Murray) have recently designed a specification language called CCL (The Computation and Control Language) that is model loosely after UNITY (developed by M. Chandy for modeling parallel systems) and which bears a strong resemblance to Promela (part of the SPIN model-checker developed by G. Holtzmann, a collaborator on this project). The idea behind CCL is to allow the control engineer to specify a simple model of the behavior of the system and to specify and reason about correctness properties in temporal logic. In particular, CCL allows (1) a formal model of the environment to be included as part of the specification and (2) allows the user to specify a model of how synchronized the distributed control elements are to be with each other and the environment (for example, one could say that the frequency of their
clocks differs by no more than some small amount). Thus, the goal of CCL is to replace software engineering and testing with model-building, formal specification and proof.

Presently, there are many limitations to CCL (and of other systems that attempt to accomplish the same thing) that allow it to be used for only simple systems. First, the proofs in CCL are done by either by hand or with the help of a difficult to use theorem prover. Second, specifying and reasoning about a sophisticated set of continuous feedback control laws in CCL is difficult due to the fact that one typically uses a different tools to reason about concurrency
(e.g. model checking and theorem proving) than one uses to reason about dynamical systems (e.g. barrier functions and sum of squares). Third, incorporating stochastic elements, such as the probability of a component failure or of the behavior of an adversary, in a formal and tractable way is presently impossible.

We propose to improve the approach in several ways:

* We propose to simplify the language to disallow arbitrarily complex specifications. The PIs believe that a simple set of building blocks, each accompanied by a formal reasoning ''tactic'' will allow the "specification and proof" engineer to easily build and reason about systems without having to do one-of-a-kind proofs.

* We propose to develop a common framework for reasoning about continuous controllers, dynamical systems and concurrent, loosely synchronized supervisory control structures. The PIs believe that the tantalizing use of barrier functions in hybrid control structures can be extended to systems with the sophistication of those specified in CCL.

* We propose to extend our techniques to include probabilistic specifications. The state of the art in probabilistic model checking, for example, is presently to the point where simple systems can be reasoned about efficiently.

=== Testbeds (Richard; 1/2 page) ===

To test our methods and motivate new insights into their performance (and limitations), we plan to make use of two testbeds that have been developed at Caltech: the multi-vehicle wireless testbed and "Alice", an autonomous vehicle that will compete in the 2005 DARPA Grand Challenge. These systems represent complementary challenges that are very representative of those faced by designers of Air Force systems (and systems of systems).

==== MVWT ====

Over the past five years (under AFOSR DURIP and MURI funding), Caltech has built a testbed consisting of up to 18 mobile vehicles with embedded computing and communications capability for use in testing new approaches for command and control across dynamic networks. The system allows testing of a variety of communications-related technologies, including distributed command and control algorithms, dynamically reconfigurable network topologies, source coding for real-time transmission of data in lossy environments, and multi-network communications.

We propose to use the MVWT to demonstrate the ability to specify and verify cooperative control missions for multiple vehicles. We will do so by
building an ''automated specification and proof interface'' to the MVWT that implements our approach to building systems that exhibit complex behaviors. Sample tasks include cooperative surveillance, area denial (in adversarial environments), and dynamic reconfiguration in the presence of vehicle failures (full or partial).

==== Alice ====

As a second testbed, we will make use of the infrastructure we have developed over the past 2.5 years through our participation in the 2004 and 2005 DARPA Grand Challenge. Our current vehicle, which the students have named "Alice", has six cameras, 4 LADAR units, an inertial measurement unit (IMU), a GPS navigation system, and numerous internal temperature and vibration sensors. The
raw data rate for Alice is approximately 5 Gb/s, which must be processed and acted upon at rates of up to 100 Hz in order to insure safe operation at high driving speeds.

The control system for Alice makes use of a highly networked control architecture, with distributed data fusion to determine elevation maps (for the height of the terrain in front of the vehicle), multiple optimization-based controllers to plan possible routes forthe vehicle, and online modeling, fault management, and decision making to provide reliable and reconfigurable
operation. Eight onboard computers distribute the computational load, sharing information at mixed rates across a 1 Gb/s switched network. System specifications call for reliable operation in the presence of up to 1 computer failure and 2 sensor failures, requiring careful coordination between computational elements.

Alice is representative of the level of complexity of UAVs and other systems. The verification and validation of software for such systems is a major challenge and by testing our techniques on Alice, we will enhance the likelihood of transition to industry and government.

== Potential impact on DoD capabities (Richard; 1/2 page) ==

If successful, the techniques developed under this proposal will provide a fundamental understanding of how to design, implement and test complex, distributed command and control systems that can be used for mixed manned and unmanned environments. Specifically, we aim to develop as mathematical framework and specification/programming languages that allow formal analysis of performance and robustness of distributed systems. While these techniques will never elimininate the need for Monte Carlo simulations and test-based validation, they will narrow the gap between theory and implementation, allow more rapid (and more reliable) development of complex, distributed, embedded systems.

== Potential team and management plan (Richard; 1/4 page) ==

The team will consist of five co-PIs at three universities: Murray (PI), Chandy and Doyle at Caltech; Klavins at U. Washington, and Parrilo at MIT. This group has a history of joint work (Parrilo got his PhD from Caltech CDS working with Doyle and Klavins was a postdoc in Caltech CS working with Murray) and represents an excellent collaboration between researchers with expertise in control and dynamical systems, computer science, and applied mathematics.

In addition to the university researchers, we plan to team with the Laboratory for Reliable Software (LARS) at the Jet Propulsion Laboratory (JPL) and we will leverage ongoing research at Caltech sponsored by Boeing. We are also exploring linkages to SRI (the author of PVS, a theorem-proving environment) and Honeywell. In all cases, these partnerships will provide transition paths for the proposed research as well as insights into additional research challenges as the program develops.

The program will be led by Richard Murray at Caltech. Because of the tight collaboration between the co-PIs, we anticipate frequent joint meetings and workshops, as well as student and faculty visits between institutions.

== Summary of estimated costs (1/2 page) ==

We anticipate a budget of $1M/year, with approximately $600K to be spent at Caltech and $200K each at MIT and U. Washington. Funds will be used to support graduate students, postdoctoral scholars, and some faculty salary support. The experimental testbeds that will be used in the proposal have already been constructed using other funds.

== Curriculum vitae of key investigators ==

* '''Note:''' this section does '''not''' count against page limit
* Everyone should send Richard a 2 page CV to be included
** Chandy: missing
** Doyle: missing
** Klavins: received
** Murray: received
** Parillo: received