MURI Telecon 2005-07-21

Goals

• Draft 3-5 major goals for the center
• Decide on preliminary writing assignments for next week

Agenda

4:00  Call begins
4:05  Round Robin: ideas for major goals (HW: skim papers on wiki first)
4:20  Discussion major goals and finalize 3-5
4:30  Outline of white paper (HW: read guidelines on wiki)
4:45  Action items and next call
4:55  Adjourn

Notes

Round Robin

Doyle

1. Provide a formalism for verification for a hybrid systems problems using set emptiness as the main idea. Currently two stage (barrier function + SoS); move toward one stage.
2. Move toward strong understanding of RYF: intractability related to fragility. Show that this leads for a formalism for designing systems that give short proofs (=> robustness)

Klavins

1. Develop models for concurrency in embedded (dynamic) systems that give insights into the design of verifable, distributed systems. Example: design protocols that allow vehicles to talk to each other and use the stability certificates for the controllers to inform the verification procedure for the protocol

Pablo

1. Extend current results to more abstract systems of equations. Currently have certain cases worked out. Would like a more general theory
2. Q (for Eric): what are the issues regarding concurrency. A: for general algorithm we sort of now how to distribute a problem. For a dynamic system, we don't know how to do this.

Chandy

1. Robustness: dealing with incremental change. Example: UAV with a path that was planned and something changes in the environment. Change is restricted to part of the overall problem. How do we deal with this.
2. Detection of regime change: if playing against opponent or environment, need to detect change in mode. Lots of work in HMM, etc. Would like to make sure we can do this in real time.
3. Time: in CS there is a model that allows vastly different speeds. In practice this doesn't happen. Would like to update the model of fairness. Centralized clocks, multiple clocks.
4. Probability: can we provide that with certain probability something will converge
5. Proof techniques: model checkers are very restrictive. Could also look at "proof by hand" and "theorem provers". Thm provers are exceptional hard but too hard right now; but 10-20 years down the line.
   • Doyle comment: there will always be some step that will be handcrafted
   • Eric comment: theorem provers seem like they start too early. A: start with a set of axioms that apply to dynamica systems and don't try to prove them

Summary of Goals

Develop a language/mathematical framework for specification, design and verification of distributed, embedded systems that provides an analyzable framework for robust performance (requires definition of robustness, performance)

1. Develop common mathematical framework for analyzing distributed, hybrid systems
   • Include frameworks such as temporal logic, stochastic systems
   • Move from deterministic analysis to probabalistic analysis
2. Extend ideas from distributed/parallel computing to apply to dynamic systems
   • Fairness, safety, progress, concurrency
   • Robustness to incremental change, large change, probabilistic change
   • Move from deterministic analysis to probabalistic analysis
3. Move the handoff between handcrafted proofs and formal methods further upstream
4. Demonstrate the utility of these methods on problems in <AF relevant> and <Science relevant>, using the Caltech MVWT as a university platform
   • Can we use MVWT to create a game in which a full automated team plays against humans. Can we tie this to V&V? Can we show that we always win (or at worst a draw)
   • Allow failure in network, slow down processor
   • Invite AF to come in and quickly code up a strategy that beats the other guys. One group uses our tools, the other just gets the primitives. Think about how to make it so that humans can't win. Weird deadlocks, etc.
   • DGC: can they prove that given a specific environment (desert), given certain class of sensors, etc we can get from point A to point B. Move from 1 car to 2 cars and add an opponent.
   • Network centric homes - program your homes so that it works, but don't have to know all of the details. Network of heterogeneous agents and not have all hell break lose.
   • Look for something that requires ridicoulous amount of testing

Outline of white paper

1. A one page cover letter (optional)
   • Use this to talk about background of team?
2. 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
3. Identification of the research and issues
   • One page; expand big picture goals
4. Proposed technical approaches
5. Potential impact on DoD capabilities
6. Potential team and management plan
7. Summary of estimated costs
8. Curriculum vitae of key investigators

Action items and next steps

1. Mani and Pablo: sent papers for posting
2. Richard: draft of white paper using ideas from telecons; out by Fri
3. All: react to outline

Next call: Wed, 4:30 pm