Abstract
In synthesis we construct finite state systems from temporal specifications. While this problem is well understood in the classical setting of non-probabilistic synthesis, this paper suggests the novel approach of open synthesis under the assumptions of an environment that chooses its actions randomized rather than nondeterministically. Assuming a randomized environment inspires alternative semantics both for linear-time and branching-time logics. For linear-time, natural acceptance criteria are almost-sure and observable acceptance, where it suffices if the probability measure of accepting paths is 1 and greater than 0, respectively.
We distinguish 0-environments, which can freely assign probabilities to each environment action, from ε-environments, where the probabilities assigned by the environment are bound from below by some ε>0. While the results in case of 0-environments are essentially the same as for nondeterministic environments, the languages occurring in case of ε-environments are topologically different from the results for nondeterministic and 0-environments (in case of LTL, recognizable by weak alternating automata vs. recognizable by deterministic automata). The complexity of open synthesis is, in both cases, EXPTIME and 2EXPTIME-complete for CTL and LTL specifications, respectively.
This work was partly supported by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable concurrent program specifications. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Anuchitanukul, A., Manna, Z.: Realizability and synthesis of reactive modules. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 156–168. Springer, Heidelberg (1994)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. IBM Workshop on Logics of Programs, pp. 52–71. Springer, Heidelberg (1981)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)
de Alfaro, L.: From fairness to chance. In: Proc. PROBMIV 1998 (1999)
Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proc. LICS, pp. 321–330. IEEE Computer Society Press, Los Alamitos (2005)
Gurevich, Y., Harrington, L.: Trees, automata and games 14, 60–65 (1982)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Kupferman, O., Vardi, M.: Freedom, weakness, and determinism: From linear-time to branching-time. In: Proc. LICS (June 1995)
Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Proc. ICTL, Manchester, pp. 91–106 (July 1997)
Kupferman, O., Vardi, M.Y.: Church’s problem revisited. The bulletin of Symbolic Logic 5(2), 245–263 (1999)
Kupferman, O., Vardi, M.Y.: Synthesizing distributed systems. In: Proc. LICS 2001, pp. 389–398. IEEE Computer Society Press, Los Alamitos (2001)
Lehmann, D., Rabin, M.O.: On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: Proc. POPL 1981, pp. 133–138. ACM Press, New York (1981)
Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: new results and new proofs of the theorems of Rabin, McNaughton and Safra. Theor. Comput. Sci. 141(1-2), 69–107 (1995)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. POPL, pp. 179–190. ACM Press, New York (1989)
Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Automata, Languages and Programming, pp. 652–671. Springer, Heidelberg (1989)
Stockmeyer, L.J., Chandra, A.K.: Provably difficult combinatorial games. SIAM J. Comput. 8(2), 151–174 (1979)
Wolper, P.: Synthesis of Communicating Processes from Temporal-Logic Specifications. PhD thesis, Stanford University (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schewe, S. (2006). Synthesis for Probabilistic Environments. In: Graf, S., Zhang, W. (eds) Automated Technology for Verification and Analysis. ATVA 2006. Lecture Notes in Computer Science, vol 4218. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901914_20
Download citation
DOI: https://doi.org/10.1007/11901914_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47237-7
Online ISBN: 978-3-540-47238-4
eBook Packages: Computer ScienceComputer Science (R0)