MURI Telecon 2005-07-13 - Revision history

Murray: /* Discussion */

2005-07-14T00:04:08Z

Discussion

← Older revision		Revision as of 00:04, 14 July 2005
Line 75:		Line 75:
	*** NCBC: Prajna and Lincoln section		*** NCBC: Prajna and Lincoln section

	** Send e-mail with thoughts to Richard		* Send e-mail with thoughts to Richard

Murray at 00:03, 14 July 2005

2005-07-14T00:03:27Z

← Older revision		Revision as of 00:03, 14 July 2005
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

Murray: telecon notes

2005-07-13T23:32:57Z

telecon notes

New page

== 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 ==

* Possible key themes:
** 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
** Think about whether we can incorporate probability in a formal way

* Should we add others to the group?

* 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