2005 MURI White Paper - Revision history

Murray at 17:18, 3 August 2005

2005-08-03T17:18:11Z

@@ Line 27: / Line 27: @@
 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) ===
@@ Line 80: / Line 96: @@
 * 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.
 === Testbeds (Richard; 1/2 page) ===

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

2005-08-03T09:25:30Z

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

← Older revision		Revision as of 09:25, 3 August 2005
Line 73:		Line 73:
	To address these issues, we propose:		To address these issues, we propose:

	1. Fully integrate elements of temporal logic and SOS-based		* 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.
	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		* 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.
	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		* 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.
	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		* 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.
	(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) ===		=== Specification and Programming Languages (Eric, with Mani; 1 page) ===

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

2005-08-03T09:23:26Z

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

@@ Line 29: / Line 29: @@
 === 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
+Sum of squares (SOS) based techniques constitute one of the most
-* Give some insights into how we plan to approach this and desired results
+comprehensive methodologies available for the algorithmic analysis of
 === Specification and Programming Languages (Eric, with Mani; 1 page) ===

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

2005-08-03T08:24:57Z

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

← Older revision		Revision as of 08:24, 3 August 2005
Line 13:		Line 13:

	Our specific goals for this MURI are to:		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 ~~stochatic~~ systems, extending work such as ~~SoSTools~~ to include ~~probabalistic~~ analysis.		# ''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).		# ''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.		# ''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.

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

2005-08-02T16:59:46Z

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

← Older revision		Revision as of 16:59, 2 August 2005
Line 33:		Line 33:
	* Give some insights into how we plan to approach this and desired results		* Give some insights into how we plan to approach this and desired results

	==== Specification and Programming Languages (Eric, with Mani; 1 page) ====		=== 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		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

Murray: =Curriculum vitae of key investigators=

2005-08-02T16:58:43Z

=Curriculum vitae of key investigators=

← Older revision		Revision as of 16:58, 2 August 2005
Line 90:		Line 90:
	* '''Note:''' this section does '''not''' count against page limit		* '''Note:''' this section does '''not''' count against page limit
	* Everyone should send Richard a 2 page CV to be included		* Everyone should send Richard a 2 page CV to be included
			** Chandy: missing
			** Doyle: missing
			** Klavins: received
			** Murray: received
			** Parillo: received

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

2005-08-02T16:57:49Z

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

← Older revision		Revision as of 16:57, 2 August 2005
Line 83:		Line 83:

	== Summary of estimated costs (1/2 page) ==		== Summary of estimated costs (1/2 page) ==
	* $1M/year
			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 ==		== Curriculum vitae of key investigators ==

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

2005-08-02T16:54:27Z

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

← Older revision		Revision as of 16:54, 2 August 2005
Line 71:		Line 71:

	== Potential impact on DoD capabities (Richard; 1/2 page) ==		== 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) ==		== Potential team and management plan (Richard; 1/4 page) ==

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

2005-08-02T16:34:13Z

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

← Older revision		Revision as of 16:34, 2 August 2005
Line 73:		Line 73:

	== Potential team and management plan (Richard; 1/4 page) ==		== 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) ==		== Summary of estimated costs (1/2 page) ==

Murray: =Alice=

2005-08-02T16:25:00Z

=Alice=

← Older revision		Revision as of 16:25, 2 August 2005
Line 62:		Line 62:
	==== Alice ====		==== 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",		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) ==		== Potential impact on DoD capabities (Richard; 1/2 page) ==