Journal Title
Title of Journal:
|
|
|
Publisher
Springer, Berlin, Heidelberg
|
|
|
|
|
|
Authors: Rüdiger Ehlers Robert Mattmüller HansJörg Peter
Publish Date: 2010/9/8
Volume: , Issue: , Pages: 107-121
Abstract
We present a general approach to combine symbolic state space representations for the discrete and continuous parts in the synthesis of winning strategies for timed reachability games The combination is based on abstraction refinement where discrete symbolic techniques are used to produce a sequence of abstract timed game automata After each refinement step the resulting abstraction is used for computing an under and an overapproximation of the timed winning states The key idea is to identify large relevant and irrelevant parts of the precise weakest winning strategy already on coarse and therefore simple abstractions If neither the existence nor nonexistence of a winning strategy can be established in the approximations we use them to guide the refinement process Based on a prototype that combines binary decision diagrams79 and difference bound matrices5 we experimentally evaluate the technique on standard benchmarks from timed controller synthesis The results clearly demonstrate the potential of the new approach concerning running time and memory consumption compared to the classical onthefly algorithm implemented in UppaalTiga 104
Keywords:
.
|
Other Papers In This Journal:
|