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.
Part of this work was done at the IBM Almaden Research Center
Chapter PDF
Similar content being viewed by others
Keywords
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
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.
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.
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.
J.R. Büchi and L.HG. Landweber. Solving sequential conditions by finite-state strategies. Trans. AMS, 138:295–311, 1969.
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.
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.
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.
A. Church. Logic, arithmetics, and automata. In Proc. International Congress of Mathematicians, 1962, pages 23–35. institut Mittag-Leffler, 1963.
A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114–133, January 1981.
D.L. Dill. Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, 1989.
E.A. Emerson and E.M. Clarke. Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.
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.
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.
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.
N. Francez. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, 1986.
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.
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.
M.T. Liu. Protocol engineering. Advances in Computing, 29:79–195, 1989.
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.
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.
Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, 2(1):90–121, 1980.
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.
A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46–57, 1977.
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.
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.
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.
H. Rudin. Network protocols and tools to help produce them. Annual Review of Computer Science, 2:291–316, 1987.
S. Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.
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.
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.
M.Y. Vardi. A temporal fixpoint calculus. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 250–259, San Diego, January 1988.
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.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1): 1–37, November 1994.
P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1–2):72–99, 1983.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vardi, M.Y. (1995). An automata-theoretic approach to fair realizability and synthesis. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_56
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_56
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive