Distributed Synthesis in Continuous Time

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9634
• 期：1
• 页码：353-369
• 全文大小：548 KB
• 参考文献：1.Baier, C., Größer, M., Bertrand, N.: Probabilistic \(\omega \) -automata. J. ACM 59(1), 1 (2012)MathSciNet CrossRef MATH
  2.Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
  3.Bernstein, D.S., Givan, R., Immerman, N., Zilberstein, S.: The complexity of decentralized control of Markov decision processes. Math. Oper. Res. 27(4), 819–840 (2002)MathSciNet CrossRef MATH
  4.Bertoni, A., Mauri, G., Torelli, M.: Some recursively unsolvable problems relating to isolated cutpoints in probabilistic automata. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256. Springer, Heidelberg (1997)
  5.Berwanger, D., Kaiser, L.: Information tracking in games on graphs. J. Logic Lang. Inform. 19(4), 395–412 (2010)MathSciNet CrossRef MATH
  6.Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)MathSciNet CrossRef MATH
  7.Canetti, R., Cheung, L., Kaynar, D.K., Liskov, M., Lynch, N.A., Pereira, O., Segala, R.: Analyzing security protocols using time-bounded task-PIOAs. Discrete Event Dyn. Syst. 18(1), 111–159 (2008)CrossRef MATH
  8.Cheung, L., Lynch, N.A., Segala, R., Vaandrager, F.W.: Switched PIOA: parallel composition via distributed scheduling. Theoret. Comput. Sci. 365(1–2), 83–108 (2006)MathSciNet CrossRef MATH
  9.D’Argenio, P.R., Katoen, J.-P.: A theory of stochastic systems part I: stochastic automata. Inf. Comput. 203(1), 1–38 (2005)MathSciNet CrossRef MATH
  10.Droste, M., Gastin, P.: Asynchronous cellular automata for pomsets without auto-concurrency. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)
  11.Genest, B., Gimbert, H., Muscholl, A., Walukiewicz, I.: Asynchronous games over tree architectures. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 275–286. Springer, Heidelberg (2013)
  12.Gimbert, H., Oualhadj, Y.: Probabilistic automata on finite words: decidable and undecidable problems. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 527–538. Springer, Heidelberg (2010)CrossRef
  13.Giro, S., D’Argenio, P.R., Fioriti, L.M.F.: Distributed probabilistic input/output automata: Expressiveness, (un)decidability and algorithms. Theoret. Comput. Sci. 538, 84–102 (2014)MathSciNet CrossRef MATH
  14.Guck, D., Han, T., Katoen, J.-P., Neuhäußer, M.R.: Quantitative timed analysis of interactive markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 8–23. Springer, Heidelberg (2012)CrossRef
  15.Hermanns, H., Johr, S.: May we reach it? Or must we? In what time? With what probability? In: MMB, pp. 125–140. VDE Verlag (2008)
  16.Hermanns, H.: Interactive Markov Chains and The Quest for Quantified Quality. Lecture Notes in Computer Science, vol. 2428. Springer, New York (2002)CrossRef MATH
  17.Hermanns, H., Vester, S., Krčál, J.: Distributed synthesis in continuous time. CoRR abs/1601.01587 (2016)
  18.Hermanns, H., Katoen, J.-P.: The how and why of interactive markov chains. In: Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 311–338. Springer, Heidelberg (2010)CrossRef
  19.Hermanns, H., Krčál, J., Křetínský, J.: Compositional verification and optimization of interactive markov chains. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 364–379. Springer, Heidelberg (2013)CrossRef
  20.Katoen, J.-P., Klink, D., Neuhäußer, M.R.: Compositional abstraction for stochastic systems. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 195–211. Springer, Heidelberg (2009)CrossRef
  21.Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90–104 (2011)CrossRef
  22.Madhusudan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 396–407. Springer, Heidelberg (2001)CrossRef
  23.Madhusudan, P., Thiagarajan, P.S.: A decidable class of asynchronous distributed controllers. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 145–160. Springer, Heidelberg (2002)CrossRef
  24.Milner, R.: Calculi for synchrony and asynchrony. Theoret. Comput. Sci. 25, 267–310 (1983)MathSciNet CrossRef MATH
  25.Neuts, M.F.: Matrix-Geometric Solutions in Stochastic Models: An Algorithmic Approach. Courier Corporation, New York (1981)MATH
  26.Paz, A.: Introduction to Probabilistic Automata. Academic Press Inc., London (1971)MATH
  27.Pelozo, S.S., D’Argenio, P.R.: Security analysis in probabilistic distributed protocols via bounded reachability. In: Palamidessi, C., Ryan, M.D. (eds.) TGC 2012. LNCS, vol. 8191, pp. 182–197. Springer, Heidelberg (2013)CrossRef
  28.Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)CrossRef
  29.Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: FOCS, pp. 746–757. IEEE Computer Society (1990)
  30.Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, New York (2009)MATH
  31.Saha, R., Esparza, J., Jha, S.K., Mukund, M., Thiagarajan, P.S.: Distributed markov chains. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 117–134. Springer, Heidelberg (2015)
  32.Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)
  33.Sinopoli, B., Sharp, C., Schenato, L., Schaffert, S., Sastry, S.S.: Distributed control applications within sensor networks. Proc. IEEE 91, 1235–1246 (2003)CrossRef
  34.Sue-Hwey, W., Smolka, S.A., Stark, E.W.: Composition and behaviors of probabilistic I/O automata. Theoret. Comput. Sci. 176(1–2), 1–38 (1997)MathSciNet MATH
  
• 作者单位：Holger Hermanns (15)
  Jan Krčál (15)
  Steen Vester (16)
  
  15. Computer Science, Saarland University, Saarbrücken, Germany
  16. Technical University of Denmark, Kongens Lyngby, Denmark
  
• 丛书名：Foundations of Software Science and Computation Structures
• ISBN：978-3-662-49630-5
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

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.