Transcript As Cheap as Possible: Linearly Priced Timed Automata

As cheap as possible:
Linearly Priced Timed Automata
Gerd Behrmann, Ed Brinksma, Ansgar Fehnker,
Thomas Hune, Kim Larsen, Paul Pettersson, Judi
Romijn, Frits Vaandrager
Brics Aalborg, Nijmegen, Twente, Uppsala,
CMU, TERMA, TUE
ULB, November 2004
Motivation
Observation (VHS project)
Many scheduling problems can be phrased in a natural way
as reachability problems for timed automata.
25min 20min 10min 5min
Unsafe
Can they make
it within 60 minutes ?
ULB, November 2004
Safe
Motivation
unsafe
L==0
take!
y:=0
release!
y>=25
unsafe
L==0
take!
y:=0
release!
y>=25
unsafe
y>=20
release!
L==1
take!
y:=0 safe
y>=5
L==1
take!
y:=0 safe
L==0
take!
y:=0
L==0
take!
y:=0
release!
release!
25min 20min 10min 5min
Unsafe
unsafe
y>=25
y>=25
release!
L==1
y>=25
release!
take!
y:=0 safe
What
What
What
Can
schedule
schedule
isthey
the make
fastest
minimizes
minmizes
it bridge
within
unsafe
schedule?
60
crossings?
time?
minutes ?
ULB, November 2004
take?
release?
y>=10
release!
L==1
take!
y:=0 safe
take?
release?
Safe
Outline
• Timed Automata (A review)
• Linearly Priced Timed Automata
– A basic Algorithm
– Efficient Data Structures
• Uniformly Priced Timed Automata
– More efficient Data Structures
• Improved State-Space Exploration
– Minimum-Cost Order Search, Estimates of Remaining Cost, Heuristics
• Results
–
–
–
–
Bridge Problem
Job-Shop Problems
Aircraft Landing
others
• Conclusion
ULB, November 2004
Timed Automata
(UPPAAL)
• Network of Automata
– Synchronization (CCS-like)
a!
a?
ULB, November 2004
Timed Automata
(UPPAAL)
• Network of Automata
– Synchronization (CCS-like)
x<7
• Clocks in description
3<x<7
a!
y=4
a?
y:=0
– Time passes uniformly
– Guard/reset on action
- Invariants on location
• Infinitely many states!
ULB, November 2004
Alur & Dill
Regions (review)
x<3
x<3
y>2
a
c
b
{x:=0}
y
y
y
3
3
3
2
2
2
1
1
1
1
2
3
x
1
2
3
x
An equivalence class (i.e. a region). In fact
there is only a finite number of regions!!
ULB, November 2004
1
2
3
x
Alur & Dill
Regions (review)
x<3
x<3
y>2
a
c
b
{x:=0}
y
y
y
3
3
3
2
2
2
1
1
1
1
2
3
x
1
2
3
x
Transitions with and w/o reset and delay
can be considered as transitions on regions!
ULB, November 2004
1
2
3
x
Zones (review)
x<3
x<3
y>2
a
c
b
{x:=0}
y
y
y
3
3
3
2
2
2
1
1
1
1
2
3
x
1
2
3
x
Convex unions of regions are called zones.
Delay, reset, transition in terms of zones
ULB, November 2004
x
1
2
3
Data Structures like DBMs,
CDDs g efficiency!
Linearly Priced Timed Automata
cost’=1
x<3
cost’=2
cost+=4
cost’=0
x<3
y>2
a
c
b
{x:=0}
• Timed Automata + Costs on transitions and locations
– Cost of performing transition: Transition cost
– Cost of performing delay d: ( d x location cost )
• Trace:
(a,x=y=0)
4
(b,x=y=0)
(2.5)
2.5 x 2
(b,x=y=2.5)
0
(a,x=0,y=2.5)
• Cost of Execution Trace: Sum of costs: 4 + 5 + 0 = 9
Problem: Finding the minimum cost of reaching location c
ULB, November 2004
Example: Aircraft Landing
cost
d+l*(t-T)
e*(T-t)
E
T
L
t
Planes have to keep separation
distance to avoid turbulences
caused by preceding planes
ULB, November 2004
E earliest landing time
T target time
L latest time
e cost rate for being early
l cost rate for being late
d fixed cost for being late
Example: Aircraft Landing
x >= 4
land!
x <= 5
cost’=3
x=5
x <= 5
x=5
cost+=2
x <= 9
cost’=1
land!
Planes have to keep separation
distance to avoid turbulences
caused by preceding planes
ULB, November 2004
4
5
9
3
1
2
earliest landing time
target time
latest time
cost rate for being early
cost rate for being late
fixed cost for being late
Priced Regions
cost
5
4
3
2
1
ULB, November 2004
Priced Regions
cost
5
4
3
2
1
ULB, November 2004
Priced Regions
cost
y
5
4
3
2
2
1
5
3
2
1
1
2
costs
ULB, November 2004
3
x
An Algorithm
• State-Space Exploration + Use of global variable Cost
• Updated Cost whenever goal state with min( C ) <Cost
is found:
Cost=
Cost=80
80
60
Cost=60
• Terminates when entire state-space is explored
ULB, November 2004
An Algorithm
Cost:=, Pass := {}, Wait := {(l0,C0)}, Goal=
while Wait  {} do
select (l,C) from Wait
if (l,C) =  and mincost(C)<Cost then Cost:=mincost(C)
if forall (l,C’) in Pass: C’
C then
add (l,C) to Pass
forall (m,D) such that (l,C)
(m,D):
add (m,D) to Wait
Return Cost
ULB, November 2004
An Algorithm
Cost:=, Pass := {}, Wait := {(l0,C0)}, Goal=
while Wait  {} do
select (l,C) from Wait
if (l,C) =  and mincost(C)<Cost then Cost:=mincost(C)
if forall (l’,C’) in Pass: C’
C then
add (l,C) to Pass
forall (m,D) such that (l,C)
(m,D):
add (m,D) to Wait
Performs: symbolic
Return Cost
operations Delay, Conjunction, and Reset of clocks.
ULB, November 2004
An Algorithm
Cost:=, Pass := {}, Wait := {(l0,C0)}, Goal=
while Wait  {} do
select (l,C) from Wait
if (l,C) =  and mincost(C)<Cost then Cost:=mincost(C)
if forall (l’,C’) in Pass: C’
C then
add (l,C) to Pass
that defines
forall (m,D) such that (l,C) : preorder
(m,D):
“better” cost zones.
add (m,D) to Wait
Return Cost
3
2
5
4
3
5
ULB, November 2004
3
2
6
An Algorithm
Cost:=, Pass := {}, Wait := {(l0,C0)}, Goal=
while Wait  {} do
select (l,C) from Wait
if (l,C) =  and mincost(C)<Cost then Cost:=mincost(C)
if forall (l’,C’) in Pass: C’
C then
add (l,C) to Pass
forall (m,D) such that (l,C)
(m,D):
add (m,D) to Wait
Return Cost
ULB, November 2004
An Algorithm
Theorem
When the algorithm terminates, the value of
COST equals mincost()
Theorem
The algorithm terminates
Can it be done efficiently?
ULB, November 2004
Outline
• Timed Automata. (A review}
• Linearly Priced Timed Automata
– A basic Algorithm
– Efficient Data Structures
• Uniformly Priced timed Automata
– More efficient Data Structures
• Improved State-Space Exploration
– Minimum-Cost Order Search, Estimates of Remaining Cost, Heuristics
• Results
–
–
–
–
Bridge Problem
Job-Shop Problems
Aircraft Landing
others
• Conclusion
ULB, November 2004
Priced Zones
Basic idea: Define a linear cost function on zones
BUT: Priced zones are not closed under delay, transitions, resets
y
cost=c+a x x + ay y
x
ULB, November 2004
Priced Zones
Basic idea: Define a linear cost function on zones
BUT: Priced zones are not closed under delay, transitions, resets
y
cost=c’’+3 x – 1 y
cost=c’+2 x – 0 y
cost=c+2 x – 1 y
x
cost’=1
x<3
a
cost’=2
cost+=4
{x:=0}
cost’=0
x<3
b
ULB, November 2004
y>2
c
Priced Zones
Basic idea: Define a linear cost function on zones
BUT: Priced zones are not closed under delay, transitions, resets
y
cost=c+2 x – 1 y
x
cost’=1
x<3
a
cost’=2
cost+=4
{x:=0}
cost’=0
x<3
b
ULB, November 2004
y>2
c
Priced Zones
Basic idea: Define a linear cost function on zones
BUT: Priced zones are not closed under delay, transitions, resets
y
cost=c’’+1 x – 1 y
cost=c’+2 x – 2 y
x
cost’=1
x<3
a
cost’=2
cost+=4
{x:=0}
cost’=0
x<3
b
ULB, November 2004
y>2
c
Priced Zones
Basic idea: Define a linear cost function on zones
BUT: Priced zones are not closed under delay, transitions, resets
y
cost=c’’ + 1 y
cost=c+2 x – 1 y
x
cost=c’ – 1 y
cost’=1
x<3
a
cost’=2
cost+=4
{x:=0}
cost’=0
x<3
b
ULB, November 2004
y>2
c
Outline
• Timed Automata. (A review}
• Linearly Priced Timed Automata
– A basic Algorithm
– Efficient Data Structures
• Uniformly Priced Timed Automata
– More efficient Data Structures
• Improved State-Space Exploration
– Minimum-Cost Order Search, Estimates of Remaining Cost, Heuristics
• Results
–
–
–
–
Bridge Problem
Job-Shop Problems
Aircraft Landing
others
• Conclusion
ULB, November 2004
Uniformly Priced Timed Automata
UPTA are LPTA where all locations
have the same rate
25min 20min 10min 5min
Unsafe
What is the fastest
schedule ?
ULB, November 2004
Safe
Uniformly Priced Timed Automata
UPTA are LPTA where all locations
have the same rate
Result
A small modification of the DBM-operations
for ordinary timed automata is sufficient to
solve cost (time) optimality problems
ULB, November 2004
Outline
• Timed Automata. (A review}
• Linearly Priced Timed Automata
– A basic Algorithm
– Efficient Data Structures
• Uniformly Priced Timed Automata
– More efficient Data Structures
• Improved State-Space Exploration
– Minimum-Cost Order Search, Estimates of Remaining Cost, Heuristics
• Results
–
–
–
–
Bridge Problem
Job-Shop Problems
Aircraft Landing
others
• Conclusion
ULB, November 2004
Verification vs. Optimization
• Verification Algorithms:
– Check a logical property of the
entire state-space of a model
– Efficient blind search
• Optimization Algorithms:
– Find (near) optimal solutions
– Use techniques to avoid nonoptimal parts of the state-space
(e.g. Branch and Bound)
• Objective:
– Bridge the gap between these
two
– New techniques and applications
in UPPAAL
Safe side reachable?
80
Min time of reaching safe side?
ULB, November 2004
60
Minimum-Cost Order
• The basic algorithm finds the
minimum cost trace
• Breadth or Depth-first
search-order
• Problem: Searches the entire
state-space
• Minimum-Cost Search
Order: Always explore state
with smallest minimum cost
first
ULB, November 2004
Minimum-Cost Order
Fact 1: First goal state found is optimal
• Cost grows along all paths
• The search can terminate when first goal state found
• Like Dijkstra’s shortest path algorithm
Fact 2: No other search order explores fewer states
• Simpler algorithm: variable Cost no longer needed
ULB, November 2004
Estimates of Remaining Cost
• Often a conservative estimate of the remaining cost
can be found
• REM( l, C ) = conservative estimate of remaining cost
• Bridge example:
REM( l, C ) = time of slowest person on Unsafe side
At least 25 mins needed to complete schedule
ULB, November 2004
Estimates of Remaining Cost
• Basic Algorithm + Estimate of remaining cost:
Only states with (min(C) + REM(l, C)) < Cost are
further explored
Cost=80
ULB, November 2004
Estimates of Remaining Cost
• Basic Algorithm + Estimate of remaining cost:
Only states with (min(C) + REM(l, C)) < Cost are
further explored
Cost=80
• Minimum Cost + Estimate of remaining cost:
Explore states with smallest ( min(C) + REM( l, C ) ) first
ULB, November 2004
Using Heuristics
• Allows the users to control the search order according
to heuristics
• Symbolic states extended to (l, C, h), where
h is the priority of a state
• Transitions are annotated with assignments to h
• Flexible!
Basic Algorithm + Heuristics:
State with highest h is explored first
ULB, November 2004
Using Heuristics
Try to schedule planes in the order of
their preferred landing times
ULB, November 2004
Outline
• Timed Automata. (A review}
• Linearly Priced Timed Automata
– A basic Algorithm
– Efficient Data Structures
• Uniformly Priced Timed Automata
– More efficient Data Structures
• Improved State-Space Exploration
– Minimum-Cost Order Search, Estimates of Remaining Cost, Heuristics
• Results
–
–
–
–
Bridge Problem
Sidmar
Aircraft Landing
others
• Conclusion
ULB, November 2004
Example: Bridge Problem
What is the fastest schedule?
BF = Breadth-First, DF = Depth-First, MC = Minimum Cost Order, MC+ = MC + REM
• Number of symbolic states generated with costextended version of UPPAAL
• Minimum Cost Order + Estimate of Remaining cost
<10% of Breadth-First Search
ULB, November 2004
SIDMAR Steel Production Plant
Crane A
• A. Fehnker [RTCSA99],
T. Hune, K. G. Larsen,
P. Pettersson [DSV00]
• Case study of Esprit-LTR
project 26270 VHS
• Physical plant of SIDMAR
located in Gent, Belgium
• Part between blast furnace and
hot rolling mill
Machine 1
Machine 4
Machine 2
Machine 3
Lane 1
Machine 5
Lane 2
Buffer
Crane B
Storage Place
Objective: model the plant, obtain
schedule and control program for
plant
ULB, November 2004
Continuos
Casting Machine
SIDMAR Steel Production Plant
Crane A
Input: sequence of steel loads
(“pigs”)
@10
2
2
Machine 4
Load follows Recipe to
obtain certain quality, e.g:
start; T1@10; T2@20;
T3@10; T2@10;
end within 120
Machine 2
Machine 1
15
Machine 3
@20
2
Lane 1
Machine 5
@10
Lane 2
16
Buffer
Crane B
=127
Optimal schedules for ten batches
using guiding with priorities.
Only offor
Output: sequence
two batches without higher quality steel.
ULB, November 2004
@10
Storage Place
@40
Continuos
Casting Machine
runways
Aircraft Landing Problem
ULB, November 2004
Advantages
Conclusion
• Easy and flexible modeling of systems
• Whole range of verification techniques becomes available
• Controller/Program synthesis
Disadvantages
• Existing scheduling approaches (still) perform somewhat better
Our goal
• See how far we get
• Integrate model checking and scheduling theory
• New discipline of Timing Technology?
EU IST project Ametist
ULB, November 2004
Conclusion
• Papers:
– Efficient Guiding Towards Cost-Optimality in UPPAAL [TACAS’01]
– Minimum Cost-Reachability for Priced Timed Automata [HSCC’01]
– As Cheap as Possible: Efficient Cost-Optimal Reachability for
Priced Timed Automata [CAV’01]
– Citius, Vilius, Melius: Guiding and Cost-Optimality in Model
Checking of Timed and Hybrid Systems, PhD Thesis Ansgar
Fehnker, University of Nijmegen, April 2002
•Tool:
–UPPAAL CORA!!
ULB, November 2004
End of slide show
ULB, November 2004
THE END
ULB, November 2004