World Scientific
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
Our website is made possible by displaying certain online content using javascript.
In order to view the full content, please disable your ad blocker or whitelist our website

System Upgrade on Mon, Jun 21st, 2021 at 1am (EDT)

During this period, the E-commerce and registration of new users may not be available for up to 6 hours.
For online purchase, please visit us again. Contact us at [email protected] for any enquiries.
Special Issue: Automated Technology for Verification and Analysis (ATVA 2005)No Access


    We propose a sound and complete compositional proof rule for distributed synthesis. Applying our proof rule only requires the manual strengthening of the specification into a conjunction of formulas that can be guaranteed by individual black-box processes. All premises of the proof rule can be checked automatically.

    For this purpose, we give an automata-theoretic synthesis algorithm for single processes in distributed architectures. The behavior of the local environment of a process is unknown in the process of synthesis and cannot be assumed to be maximal. We therefore consider reactive environments that have the power to disable some of their own actions, and provide methods for synthesis (and realizability checking) in this setting. We establish upper bounds for CTL (2EXPTIME) and CTL* (3EXPTIME) synthesis with incomplete information, matching the known lower bounds for these problems, and provide matching upper and lower bounds for μ-calculus synthesis (2EXPTIME) with complete or incomplete information. Synthesis in reactive environments is harder than synthesis in maximal environments, where CTL, CTL* and μ-calculus synthesis are EXPTIME, 2EXPTIME and EXPTIME complete, respectively.


    • A. Pnueli and R. Rosner, Distributed reactive systems are hard to synthesize, Proc. FOGS (1990) pp. 746–757. Google Scholar
    • O.   Kupferman and M. Y.   Vardi , Synthesizing distributed systems , IEEE Symposium on Logic in Computer Science ( 2001 ) . Google Scholar
    • B. Finkbeiner and S. Schewe, Uniform distributed synthesis, Proc. LICS (IEEE Computer Society Press, 2005) pp. 321–330. Google Scholar
    • E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Proc. IBM Workshop on Logics of Programs, LNCS 131 (Springer-Verlag, 1981) pp. 52–71. Google Scholar
    • Wolper, P.: Synthesis of Communicating Processes from Temporal-Logic Specifications. PhD thesis, Stanford University (1982) . Google Scholar
    • O.   Kupferman and M. Y.   Vardi , Synthesis with incomplete informatio , Proc. 2nd International Conference on Temporal Logic (ICTL'97) ( 1997 ) . Google Scholar
    • O. Kupferman and M. Y. Vardi, μ-calculus synthesis, Proc. MFCS, LNCS 1893 (Springer-Verlag, 2000) pp. 497–507. Google Scholar
    • O. Kupfermanet al., Open systems in reactive environments: Control and synthesis, Proc. 11th Int. Conf. on Concurrency Theory, LNCS 1877 (Springer-Verlag, 2000) pp. 92–107. Google Scholar
    • O. Kupferman and M. Y. Vardi, The bulletin of Symbolic Logic 5, 245 (1999). Crossref, ISIGoogle Scholar
    • D. E. Muller and P. E. Schupp, Theor. Comput. Sci. 54, 267 (1987), DOI: 10.1016/0304-3975(87)90133-2. Crossref, ISIGoogle Scholar
    • D. E. Muller and P. E. Schupp, Theor. Comput. Sci. 141, 69 (1995), DOI: 10.1016/0304-3975(94)00214-4. Crossref, ISIGoogle Scholar
    • M. Jurdziński, Small progress measures for solving parity games, Proc. STAGS, LNCS 1770 (Springer-Verlag, 2000) pp. 290–301. Google Scholar
    • W. P.   de Roever , H.   Langmaack and A.   Pnueli (eds.) , Compositionality: The Significant Difference. COMPOS'97 , LNCS   1536 ( Springer Verlag , 1998 ) . Google Scholar
    • Maier, P.: A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning. PhD thesis, Universität des Saarlandes, Saarbrücken (2003) . Google Scholar
    • E. A. Emerson and C. S. Jutla, Tree automata, μ-calculus and determinacy, Proc. FOGS (IEEE Computer Society Press, 1991) pp. 368–377. Google Scholar
    Remember to check out the Most Cited Articles!

    Check out these Handbooks in Computer Science