Specifying Globally, Controlling Locally

Download Report

Transcript Specifying Globally, Controlling Locally

Specifying Globally,
Controlling Locally
ERIC KLAVINS
Department of Computer Science
California Institute of Technology
Motivating Example 1:
Omniscient Beings Going Places
Problem Description: Get each robot to its
goal with no collisions.
With global knowledge it’s easy.
But it doesn’t scale:
•n2 communications
•Many solutions (like optimal control)
become computationally infeasible as n
goes up.
Cn(R
2)
is conn
Motivating Example 2:
Solipsists Going Places
(or “The LA Freeway Model”)
So what if the robots just treat others like
(moving) obstacles?
Communication and computation go down.
But you can get especially poor
performance.
A happy medium uses uses just enough
communication, sensing and computation to
perform the task. But how much is just
enough?
Decentralized Control
Given that:
•There is no leader.
•Global state or consensus with more than a constant
number of other entities is impractical.
•Communication complexity should be linear or better.
What is the right formalism for designing and reasoning
about decentralized systems?
Approach: Synthesize local controllers from a global
specification.
Example: The Minifactory
Product
description
Theorem 1: The compiler produces live
(deadlock free), cyclic distributed programs
that respect product flow.
Observation: Communication goes up
linearly. Throughput is constant.
GOAL:
[Klavins, HSCC 2000; Klavins and Koditschek,
ICRA 2000]
Automated factory assembles copies of product
(Pictured is the CMU Minifactory [Hollis, Rizzi,
Gowdy ICRA ’97-’99]).
Compiler uses a formal composition to
build up factory programs.
Example: Self Assembly
Given: A (graph) specification of an assembly. Neighbors should
be distance dnbr apart. Non-neighbors should be farther away.
Synthesize: Local controllers for each part that have the
“emergent” effect of assembling the product.
In a simplified model
Theorem 1: Only specified product is
assembled.
Theorem 2: A maximal number of
parts are assembled.
Observation: Communication is
linear since sensing is bounded. Time
to p% assembled is independent of n.
[Klavins, CCC 2002; Klavins ICRA 2002]
Example: Oscillator Networks
Equation for Individual Oscillator
What graphs are valid specifications?
[Klavins, Ghrist and Koditschek, WAFR2000; Klavins, Thesis
2001; Klavins and Koditschek, IJRR 2002,...]
n
 i  1   Ci , j sin(  i   j )
j 1
1
1
1
1
1
-1
1
The system corresponding to this connection graph meets the
specification: it has a single, global attracting behavior.
-1
Komsuoglu, Koditschek &
Full, NBR 2000]
-1
-1
Simple locomotion
model for stick insect
analysis: [Klavins,
-1
-1
-1
The same analysis on this system gives multiple stable
orbits. The system does not perform the task specified.
Observation:
Communication complexity
depends on the degree of
the connection graph.
Toward a Systematic Approach
Based on UNITY [Klavins&Hickey, Submitted to CDC2002]
IDEA: Take a processor view: Specify a decentralized
dynamical system as a parallel program.
•Each processor (vehicle) owns a set of instructions
describing its behavior.
•The dynamics of the environment is just another
processor (a computationally powerful one!).
As a result, we get:
•No continuous/discrete duality.
•A formal object amenable to automated reasoning.
•No specification/implementation duality.
A Sample Specification
In which the features of “DRL” are highlighted
rule
guard
dynamics
controller
spec
Non-deterministic Execution Model
how g:r
transforms
the state
the kth epoch
Specifying Dynamics and Controllers
controller specification
 is the “eventually”
temporal logic relation
new temporal logic
relation
Refinement
The road from specification to implementation is paved
with refinements.
PLAN: Build a toolbox of specification transformations
that can be used to systematically refine (global)
specifications into (local) implementations.
Continuous Communication Refinement
means: for some
z Bk(x).
Theorem: Given a partition of the clauses of  that
respects variable assignments, CCR()  .
A Multi-Vehicle Example
Problem: Each vehicle should
maintain an estimate of the
position of every other vehicle.
•Requirement: Nearby vehicles
should have better estimates of
each other’s position.
•What is the least amount of
communication necessary to
implement com ?
Maintaining Estimates
f
e
time to
send
time to
recv
t
The Refinement
Theorem: ’  .
Choosing the Bound Function
Recall that we want to have
What is a good ?
Assume an infinite number of robots, with density . And
suppose that a vehicle communicates with vehicles at
distance d every r(d) seconds. Then the total rate for all
robots at distance m is
Conjecture: Any choice of 
results in r(d)=O(d).
Area of nth
annulus is
2(2n-1)
Charts and Graphs
%n2
•Choose (d) = kd + 2com
0.01
0.008
•Communication rate goes
up as density of vehicles
goes up.
0.006
0.004
0.002
10
20
30
40
50
•Message rate divided by
worst case rate stays low
as n goes up.
t
rate msg s
250
200
150
100
50
t
10
20
30
40
50
vehicles
vehicles/m
10
0.20
20
0.41
30
0.61
40
0.82
50
1.02
The Road Ahead
Proof automation
Proof of concept with MVWT
More natural expression of
delays (SWCR doesn’t work)
Planning as refinement
Communication complexity of
tasks