Difference between revisions of "MURI Telecon 2005-07-13"

From Murray Wiki
Jump to navigationJump to search
(telecon notes)
 
 
(One intermediate revision by the same user not shown)
Line 39: Line 39:
 
* Erik: moving back and forth between writing continuous part using discrete language versus the other way
 
* 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.
 
* 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 ==
 
== Discussion ==
  
* Possible key themes:
+
* 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
 
** Problem features: hybrid, distributed, stochastic, adversarial
 
** ''Fundamental framework'' for reasoning about distributed computation for real-time, feedback systems
 
** ''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
+
** 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
 
** 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)?
  
* Should we add others to the group?
+
* 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
 
* Homework
 
** Put together set of 3-5 papers describing the basic ideas that we want to build on
 
** Put together set of 3-5 papers describing the basic ideas that we want to build on
** CCL paper
+
*** CCL paper
** V&V from Mani
+
*** V&V from Mani
** SoS Barrier Certificates
+
*** SoS Barrier Certificates
 +
*** NCBC: Prajna and Lincoln section
 +
 
 +
* Send e-mail with thoughts to Richard

Latest revision as of 00:04, 14 July 2005

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