TY - GEN
T1 - Synthesis of large concurrent programs via pairwise composition
AU - Attie, Paul C.
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84888223660&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84888223660&partnerID=8YFLogxK
U2 - 10.1007/3-540-48320-9_11
DO - 10.1007/3-540-48320-9_11
M3 - Conference contribution
AN - SCOPUS:84888223660
SN - 3540664254
SN - 9783540664253
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 130
EP - 145
BT - CONCUR 1999, Concurrency Theory - 10th International Conference, Proceedings
PB - Springer Verlag
T2 - 10th International Conference on Concurrency Theory, CONCUR 1999
Y2 - 24 August 1999 through 27 August 1999
ER -