Distributed synthesis in continuous time

Holger Hermanns, Jan Krčál, Steen Vester

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

We introduce a formalism modelling communication of distributed agents strictly in continuous-time. Within this framework, we study the problem of synthesising local strategies for individual agents such that a specified set of goal states is reached, or reached with at least a given probability. The flow of time is modelled explicitly based on continuous-time randomness, with two natural implications: First, the non-determinism stemming from interleaving disappears. Second, when we restrict to a subclass of non-urgent models, the quantitative value problem for two players can be solved in EXPTIME. Indeed, the explicit continuous time enables players to communicate their states by delaying synchronisation (which is unrestricted for non-urgent models). In general, the problems are undecidable already for two players in the quantitative case and three players in the qualitative case. The qualitative undecidability is shown by a reduction to decentralized POMDPs for which we provide the strongest (and rather surprising) undecidability result so far.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science
Number of pages17
Volume9634
Publication date2016
Pages353-369
ISBN (Print)9783662496299
DOIs
Publication statusPublished - 2016
Event19th International Conference on Foundations of Software Science and Computation Structures - Eindhoven University of Technology, Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016
Conference number: 19

Conference

Conference19th International Conference on Foundations of Software Science and Computation Structures
Number19
LocationEindhoven University of Technology
CountryNetherlands
CityEindhoven
Period02/04/201608/04/2016
SeriesLecture Notes in Computer Science
Volume9634
ISSN0302-9743

Fingerprint Dive into the research topics of 'Distributed synthesis in continuous time'. Together they form a unique fingerprint.

Cite this