连续时间分布综合
Distributed Synthesis in Continuous Time
摘要：
我们介绍了一种形式主义建模通信的分布式代理严格在连续时间。在这个框架内，我们研究的问题，合成的局部策略，个别代理，使一组指定的目标状态达到，或达到至少一个给定的概率。时间流是基于连续时间随机性明确建模的，有两个自然的含义：第一，来自交织的非确定性消失了。第二，当我们限制到非紧急模型的子类时，两个玩家的定量价值问题可以在EXPTIME中解决。事实上，显式的连续时间使参与者能够通过延迟同步来传达他们的状态（这对于非紧急模型是不受限制的）。一般来说，在定量的情况下，对于两个参与者和定性的情况下，对于三个参与者，问题已经是不可判定的。定性的不可判定性是通过减少到分散的POMDPs，我们提供了最强的（而令人惊讶的）不可判定性的结果到目前为止。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
