Advertisement

An automata-theoretic approach to fair realizability and synthesis

Preliminary report
  • Moshe Y. Vardi
Session 8: Invited Titorial
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

Over the last few years, the automata-theoretic approach to realizability checking and synthesis of reactive modules, developed by Pnueli and Rosner, by Abadi, Lamport, and Wolper, and by Dill and Wong-Toi, has been quite successful, handling both the synchronous and the asynchronous cases. In this approach one transforms the specification into a tree automaton. The specification is realizable if this tree automaton is nonempty, i.e., accepts some infinite tree, and a finite representation of an infinite tree accepted by this automaton can be viewed as a finite-state program realizing the specification. Anuchitanukul and Manna argued that the automata-theoretic approach cannot handle realizability checking and synthesis under fairness assumptions. In this paper we show to the contrary that the automata-theoretic approach can handle realizability checking and synthesis under a variety of fairness assumption.

Keywords

Temporal Logic Tree Automaton Fairness Condition Proof Sketch Realizability Check 
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.

References

  1. [AL91]
    M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.CrossRefGoogle Scholar
  2. [ALW89]
    M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable concurrent program specifications. In Proc. 16th Int. Colloquium on Automata, Languages and Programming, volume 372, pages 1–17. Lecture Notes in Computer Science, Springer-Verlag, July 1989.Google Scholar
  3. [AM94]
    A. Anuchitanukul and Z. Manna. Realizability and synthesis of reactive modules. In Computer-Aided Verification, Proc. 6th Int'l Workshop, pages 156–169, Stanford, California, June 1994. Springer-Verlag, Lecture Notes in Computer Science 818.Google Scholar
  4. [BL69]
    J.R. Büchi and L.HG. Landweber. Solving sequential conditions by finite-state strategies. Trans. AMS, 138:295–311, 1969.Google Scholar
  5. [Büc62]
    J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, pages 1–12, Stanford, 1962. Stanford University Press.Google Scholar
  6. [CES86]
    E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, January 1986.CrossRefGoogle Scholar
  7. [CGL93]
    E.M. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Decade of Concurrency-Reflections and Perspectives (Proceedings of REX School), Lecture Notes in Computer Science, pages 124–175. Springer-Verlag, 1993.Google Scholar
  8. [Chu63]
    A. Church. Logic, arithmetics, and automata. In Proc. International Congress of Mathematicians, 1962, pages 23–35. institut Mittag-Leffler, 1963.Google Scholar
  9. [CKS81]
    A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114–133, January 1981.Google Scholar
  10. [Dil89]
    D.L. Dill. Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, 1989.Google Scholar
  11. [EC82]
    E.A. Emerson and E.M. Clarke. Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.CrossRefGoogle Scholar
  12. [EJ88]
    E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.Google Scholar
  13. [EJ89]
    E.A. Emerson and C. Jutla. On simultaneously determinizing and complementing ω-automata. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pages 333–342, 1989.Google Scholar
  14. [Eme85]
    E.A. Emerson. Automata, tableaux, and temporal logics. In Proc. Workshop on Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79–87. Springer-Verlag, 1985.Google Scholar
  15. [Fra86]
    N. Francez. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, 1986.Google Scholar
  16. [Kla92]
    N. Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. In Proceedings of the 7th IEEE Symposium on Logic in Computer Science, pages 382–393, Santa Cruz Juan, 1992.Google Scholar
  17. [Lam83]
    L. Lamport. What good is temporal logic? In R.E.A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress. IFIP, North-Holland, 1983.Google Scholar
  18. [Liu89]
    M.T. Liu. Protocol engineering. Advances in Computing, 29:79–195, 1989.Google Scholar
  19. [LP85]
    O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97–107, New Orleans, January 1985.Google Scholar
  20. [LPS81]
    D. Lehman, A. Pnueli, and J. Stavi. Impartiality, justice, and fairness — the ethic of concurrent termination. In Proc. 8th Colloq. on Automata, Programming, and Languages (ICALP), volume 115 of Lecture Notes in Computer Science, pages 264–277. Springer-Verlag, July 1981.Google Scholar
  21. [MW80]
    Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, 2(1):90–121, 1980.CrossRefGoogle Scholar
  22. [MW84]
    Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6(1):68–93, January 1984.CrossRefGoogle Scholar
  23. [Pnu77]
    A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46–57, 1977.Google Scholar
  24. [PR89a]
    A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the Sixteenth ACM Symposium on Principles of Programming Languages, Austin, Januery 1989.Google Scholar
  25. [PR89b]
    A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module. In Proc. 16th Int. Colloquium on Automata, Languages and Programming, volume 372, pages 652–671. Lecture Notes in Computer Science, Springer-Verlag, July 1989.Google Scholar
  26. [QS81]
    J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th Int'l Symp. on Programming, volume 137, pages 337–351. Springer-Verlag, Lecture Notes in Computer Science, 1981.Google Scholar
  27. [Rud87]
    H. Rudin. Network protocols and tools to help produce them. Annual Review of Computer Science, 2:291–316, 1987.CrossRefGoogle Scholar
  28. [Saf88]
    S. Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.Google Scholar
  29. [SV89]
    S. Safra and M.Y. Vardi. On ω-automata and temporal logic. In Proceedings of the 21st ACM Symposium on Theory of Computing, pages 127–137, Seattle, May 1989.Google Scholar
  30. [SVW87]
    A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.CrossRefGoogle Scholar
  31. [Var88]
    M.Y. Vardi. A temporal fixpoint calculus. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 250–259, San Diego, January 1988.Google Scholar
  32. [VS85]
    M.Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th ACM Symp. on Theory of Computing, pages 240–251, 1985.Google Scholar
  33. [VW94]
    M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1): 1–37, November 1994.CrossRefGoogle Scholar
  34. [Wol83]
    P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1–2):72–99, 1983.CrossRefGoogle Scholar
  35. [WTD91]
    H. Wong-Toi and D.L. Dill. Synthesizing processes and schedulers from temporal specifications. In E.M. Clarke and R.P. Kurshan, editors, Computer-Aided Verification'90, volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 177–186, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Moshe Y. Vardi
    • 1
  1. 1.Department of Computer ScienceRice UniversityHoustonUSA

Personalised recommendations