MURI Telecon 2005-07-13

Agenda

1. Quick review of RFP
2. Round robin: comments on RFP, interests, etc
3. Wrap up and next steps

Round Robin

Eric

• V&V is really messy and hard the way that it is currently done
• Experience working with Boeing/OCP isn't encouraging
• How do you make code for a distributed system in a straightforward way that is automatically checked, etc?
• How do you know the way the controller is switched on/off is worked into the system?
• Systems Eric can get his head around are much simpler; agents running a controller, switching based on messages, etc. Can put into formal setting and reason about it; not clear how to reason about the dynamics
• Interested in figuring out how to build these sorts of systems using structured principles

John

• Focus on basic science - create theoretical infrastructure that addresses all of the research concentration areas
• Start with Prajna thesis - V&V of hybrid systems
• Build this into the SoS framework (Pablo can elaborate)
• Restrict the expressiveness of the languages (protocols, not systems). Restrict the kind of hacks people can do.
• Have examples of distributed systems using protocol stacks - use this sort of an architecture
• Think about the mathematics

Mani

• Doing things bottom up (starting with code that someone has developed) is impossible
• Start top down: what's the language for specification (temporal logic, some variant?)
• What is the theory behind the specification
• SoS + temporal logic
• Add Gerard Holzman (JPL), Rajiv Joshi (JPL)?
• Specification, theorem proving, etc
• Try to stay out of things like CORBA and other large systems that people have built up
• Use of probability: can we prove things things in a probabalistic manner?

Pablo

• Particularly interested in how we integrate discrete and continuous parts
• One possibility is establishing a middle layer where we can assert things about the time evolution (certain things will transition in a period of time)
• Barrier work of Steven could be a start; is there a way to integrate things in a tighter way?
• Incorporate adversarial effort?
• Erik: moving back and forth between writing continuous part using discrete language versus the other way
• Common way of thinking about: polynomial representations for discrete problems. But these are extremely structured proofs.

Discussion

• Computing high order polynomial certificates as a uniform framework
• Asynchronous execution
• Need way to figure out to stitch together different methods
• Propositional logic can be included in SoS; not clear how temporal logic can be included (limited subset is possible)

Discussion

• Possible themes:
  • Focus on fundamental work; stay away for trying to solve problems for today's systems. Simple systems OK, with an eye toward scaleability
  • Problem features: hybrid, distributed, stochastic, adversarial
  • Fundamental framework for reasoning about distributed computation for real-time, feedback systems
  • Top-down approach: think about a language for specifications that we can reason about. "Design for verifiability"
  • Think about whether we can incorporate probability in a formal way
  • Formulate a temporal logic that is amenable to proof techniques?

• Application testbed?
  • Make use of the MVWT?

• Should we add others to the team?
  • JPL? Holzman group on verification?
  • Boeing (through Sean Calahan)?

• Timeline for discussions and writing
  • Weekly telecons, with a fixed set of goals and agenda
  • Start writing ~25 Jul (=> two weeks)
  • Pablo will be at Caltech starting ~25 Jul (Connections)

• Homework
  • Put together set of 3-5 papers describing the basic ideas that we want to build on
    • CCL paper
    • V&V from Mani
    • SoS Barrier Certificates
    • NCBC: Prajna and Lincoln section

• Send e-mail with thoughts to Richard