Abstract
We present a tractable method for synthesizing arbitrarily large concurrent programs from specifications expressed in temporal logic. Our method does not explicitly construct the global state transition diagram of the program to be synthesized, and thereby avoids state explosion. Instead, it constructs a state transition diagram for each pair of component processes (of the program) that interact. This “pair-program” embodies all possible interactions of the two processes. Our method proceeds in two steps. First, we construct a pair-program for every pair of “connected” processes, and analyze these pair-programs for desired correctness properties. We then take the “pair processes” of the pair-programs, and “compose” them in a certain way to synthesize the large concurrent program. We establish a “large model” theorem which shows that the synthesized large program inherits correctness properties from the pair-programs.
Supported in part by NSF CAREER Grant CCR-9702616 and AFOSR Grant F49620-96-1-0221
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Anuchitanukul and Z. Manna. Realizability and synthesis of reactive modules. In Proc. 6th Intl. CAV Conference, volume 818 of LNCS. Springer-Verlag, 1994.
A. Arora, P. C. Attie, and E. A. Emerson. Synthesis of fault-tolerant concurrent systems. In Proc. 17’th Annual ACM Symposium on Principles of Distributed Computing, pages 173–182, June 1998.
P. C. Attie and E. A. Emerson. Synthesis of concurrent systems for an atomic read/atomic write model of computation (extended abstract). In Proc. 15’th ACM Symposium on Principles of Distributed Computing, pages 111–120, May 1996.
P. C. Attie and E. A. Emerson. Synthesis of concurrent systems with many similar processes. ACM Trans. Program. Lang. Syst.., 20(1):51–115, January 1998.
E. M. Clarke, E. A. Emerson, and P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst.., 8(2):244–263, April 1986.
P. J. Courtois, H. Heymans, and D. L. Parnas. Concurrent control with readers and writers. Communications of the ACM, 14(10):667–668, 1971.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall Inc., 1976.
E. W. Dijkstra. Selected Writings on Computing: A Personal Perspective, pages 188–199. Springer-Verlag, New York, 1982.
D. L. Dill and H. Wong-Toi. Synthesizing processes and schedulers from temporal specifications. In 2’nd Intl.CAV Conference, LNCS vol. 531. Springer-Verlag, 1990.
E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B. The MIT Press/Elsevier, Cambridge, Mass., 1990.
E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program.., 2:241–266, 1982.
E. A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program.., 8:275–306, 1987.
O. Grumberg and D. E. Long. Model checking and modular verification. ACM Trans. Program. Lang. Syst.., 16(3):843–871, May 1994.
Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst.., 6(1):68–93, January 1984.
A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symposium on Principles of Programming Languages, New York, 1989. ACM.
A. Pnueli and R. Rosner. On the synthesis of asynchronous reactive modules. In Proc. 16th ICALP, volume 372 of LNCS, Berlin, 1989. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Attie, P.C. (1999). Synthesis of Large Concurrent Programs via Pairwise Composition. In: Baeten, J.C.M., Mauw, S. (eds) CONCUR’99 Concurrency Theory. CONCUR 1999. Lecture Notes in Computer Science, vol 1664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48320-9_11
Download citation
DOI: https://doi.org/10.1007/3-540-48320-9_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66425-3
Online ISBN: 978-3-540-48320-5
eBook Packages: Springer Book Archive