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

From Murray Wiki

Jump to navigationJump to search (telecon notes) |
|||

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 | + | * 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)? | ||

− | * | + | * 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 |

## Revision as of 00:03, 14 July 2005

## Agenda

- Quick review of RFP
- Round robin: comments on RFP, interests, etc
- 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

- Put together set of 3-5 papers describing the basic ideas that we want to build on

- Send e-mail with thoughts to Richard