Distributed Synthesis in Continuous Time

We introduce a formalism modelling communication of distributed agents strictly in continuous-time. Within this framework, we study the problem of synthesizing 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, both the qualitative and quantitative reachability problem can be solved in EXPTIME. The crucial observation is that explicit continuous time enables the players to communicate their states by delaying synchronization. In general, the quantitative problem is undecidable for two or more players and the qualitative problem is EXPTIME-hard for two players and undecidable for three or more players. The qualitative undecidability is shown by a reduction to decentralized POMDPs for which we provide the strongest (and rather surprising) undecidability result so far.

Authors

• Jan Krcal

Keywords

No keywords are indexed for this paper.