Advertisement

μ-Calculus Synthesis

  • Oma Kupferman
  • Moshe Y. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)

Abstract

In system synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. When the system is open, it interacts with an environment via input and output signals and its behavior depends on this interaction. An open system should satisfy its specification in all possible environments. In addition to the input signals that the system can read, an environment can also have internal signals that the system cannot read. In the above setting, of synthesis with incomplete information, we should transform a specification that refers to both readable and unreadable signals into a system whose behavior depends only on the readable signals. In this work we solve the problem of synthesis with incomplete information for specifications in μ-calculus. Since many properties of systems are naturally specified by means of fixed points, the μ-calculus is an expressive and important specification language. Our results and technique generalize and simplify previous work on synthesis. In particular, we prove that the problem of μ-calculus synthesis with incomplete information is EXPTIME-complete. Thus, it is not harder than the satisfiability or the synthesis problems for this logic.

Keywords

Incomplete Information Computation Tree Synthesis Problem Input Tree Label Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    G. Bhat and R. Cleaveland. Efficient local model-checking for fragments of the modal μ-calculus. In Proc. TACAS, LNCS 1055, 1996.Google Scholar
  2. 2.
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information & Computation, 98(2): 142–170, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    M. Daniele, P. Traverso, and M.Y. Vardi. Strong cyclic planning revisited. In Proc 5th European Conference on Planning, pp. 34–46, 1999.Google Scholar
  4. 4.
    E.A. Emerson and E.M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In Proc. 7th ICALP, pp. 169–181, 1980.Google Scholar
  5. 5.
    E.A. Emerson and E.M. Clarke. Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.zbMATHCrossRefGoogle Scholar
  6. 6.
    E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151–178, 1986.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    E.A. Emerson and C. Jutla. Tree automata, Mu-calculus and determinacy. In Proc. 32nd FOCS, pp. 368–377, 1991.Google Scholar
  8. 8.
    E.A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of μ-calculus. In Proc. 5th CAV, LNCS 697, pp. 385–396, 1993.Google Scholar
  9. 9.
    E.A. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, pp. 997–1072, 1990.Google Scholar
  10. 10.
    M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and Systems Sciences, 18:194–211, 1979.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    E. Graedel and I. Walukiewicz. Guarded fixed point logic. In Proc. 14th LICS, 1999.Google Scholar
  12. 12.
    D. Janin and I. Walukiewicz. Automata for the modal μ-calculus and related results. In Proc. 20th MFCS, LNCS, pp. 552–562, 1995.Google Scholar
  13. 13.
    R. Kumar and V.K. Garg. Modeling and control of logical discrete event systems.Kluwer Academic Publishers, 1995.Google Scholar
  14. 14.
    D. Kozen. Results on the prepositionalμ-calculus. Theoretical Computer Science, 27:333–354, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    R. Kumar and M.A. Shayman. Supervisory control of nondeterministic systems under partial observation and decentralization. SIAM J. of Control and Optimization, 1995.Google Scholar
  16. 16.
    O. Kupferman and M.Y. Vardi. Synthesis with incomplete informatio. In Proc. 2nd ICTL, pp. 91–106, July 1997.Google Scholar
  17. 17.
    O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2), March 2000.Google Scholar
  18. 18.
    D.E. Muller and P.E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141:69–107, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM TOPLAS, 2(1):90–121, 1980.zbMATHCrossRefGoogle Scholar
  20. 20.
    A. Pnueli and R. Rosner On the synthesis of a reactive module. In 16th POPL, 1989.Google Scholar
  21. 21.
    M.O. Rabin. Weakly definable relations and special automata. In Proc. Symp. Math. Logic and Foundations of Set Theory, pp. 1–23. North Holland, 1970.Google Scholar
  22. 22.
    R. Rosner. Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1992.Google Scholar
  23. 23.
    M.Y. Vardi. An automata-theoretic approach to fair realizability and synthesis. In Proc. 7th CAV, LNCS939, pp. 267–292, 1995.Google Scholar
  24. 24.
    M.Y. Vardi. Reasoning about the past with two-way automata. In Proc. 25th ICALP, LNCS 1443, pp. 628–641, 1998.Google Scholar
  25. 25.
    T. Wilke. CTL+ is exponentially more succinct than CTL. In Proc. 19th TST & TCS, LNCS 1738, pp. 110–121, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Oma Kupferman
    • 1
  • Moshe Y. Vardi
    • 2
  1. 1.Hebrew UniversityJerusalemIsrael
  2. 2.Department of Computer ScienceRice UniversityHoustonUSA

Personalised recommendations