Back to Search Start Over

What’s to Come is Still Unsure

Authors :
Naijun Zhan
Peter Nazier Mosaad
Mingshuai Chen
Martin Fränzle
Yangjia Li
Source :
Automated Technology for Verification and Analysis ISBN: 9783030010898, ATVA
Publication Year :
2018
Publisher :
Springer International Publishing, 2018.

Abstract

The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and adding an appropriate winning condition permits to specify desirable behavior. The classical model here is the positional game, where both players can (fully or partially) observe the current position in the game graph, which in turn is indicative of their mutual current states. In practice, neither sensing or actuating the environment through physical devices nor data forwarding to and signal processing in the controller are instantaneous. The resultant delays force the controller to draw decisions before being aware of the recent history of a play. It is known that existence of a winning strategy for the controller in games with such delays is decidable over finite game graphs and with respect to \(\omega \)-regular objectives. The underlying reduction, however, is impractical for non-trivial delays as it incurs a blow-up of the game graph which is exponential in the magnitude of the delay. For safety objectives, we propose a more practical incremental algorithm synthesizing a series of controllers handling increasing delays and reducing game-graph size in between. It is demonstrated using benchmark examples that even a simplistic explicit-state implementation of this algorithm outperforms state-of-the-art symbolic synthesis algorithms as soon as non-trivial delays have to be handled. We furthermore shed some light on the practically relevant case of non-order-preserving delays, as arising in actual networked control, thereby considerably extending the scope of regular game theory under delay pioneered by Klein and Zimmermann.

Details

ISBN :
978-3-030-01089-8
ISBNs :
9783030010898
Database :
OpenAIRE
Journal :
Automated Technology for Verification and Analysis ISBN: 9783030010898, ATVA
Accession number :
edsair.doi...........7b67fef2f7ddf40e5302985b9ddc38ff
Full Text :
https://doi.org/10.1007/978-3-030-01090-4_4