# An automata-theoretic approach to fair realizability and synthesis

## 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## References

- [AL91]M. Abadi and L. Lamport. The existence of refinement mappings.
*Theoretical Computer Science*, 82(2):253–284, 1991.CrossRefGoogle Scholar - [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 - [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 - [BL69]J.R. Büchi and L.HG. Landweber. Solving sequential conditions by finite-state strategies.
*Trans. AMS*, 138:295–311, 1969.Google Scholar - [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 - [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 - [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 - [Chu63]A. Church. Logic, arithmetics, and automata. In
*Proc. International Congress of Mathematicians, 1962*, pages 23–35. institut Mittag-Leffler, 1963.Google Scholar - [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 - [Dil89]D.L. Dill.
*Trace theory for automatic hierarchical verification of speed independent circuits*. MIT Press, 1989.Google Scholar - [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 - [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 - [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 - [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 - [Fra86]N. Francez.
*Fairness*. Texts and Monographs in Computer Science. Springer-Verlag, 1986.Google Scholar - [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 - [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 - [Liu89]M.T. Liu. Protocol engineering.
*Advances in Computing*, 29:79–195, 1989.Google Scholar - [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 - [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 - [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 - [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 - [Pnu77]A. Pnueli. The temporal logic of programs. In
*Proc. 18th IEEE Symposium on Foundation of Computer Science*, pages 46–57, 1977.Google Scholar - [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 - [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 - [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 - [Rud87]H. Rudin. Network protocols and tools to help produce them.
*Annual Review of Computer Science*, 2:291–316, 1987.CrossRefGoogle Scholar - [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 - [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 - [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 - [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 - [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 - [VW94]M.Y. Vardi and P. Wolper. Reasoning about infinite computations.
*Information and Computation*, 115(1): 1–37, November 1994.CrossRefGoogle Scholar - [Wol83]P. Wolper. Temporal logic can be more expressive.
*Information and Control*, 56(1–2):72–99, 1983.CrossRefGoogle Scholar - [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