Abstract
Synthesis is the process of automatically generating a correct running system from its specification. In this paper, we suggest a translation of a Live Sequence Chart specification into a two-player game for the purpose of synthesis. We use this representation for synthesizing a reactive system, and introduce a novel algorithm for composing two such systems for two subsets of a specification. Even though this algorithm may fail to compose the systems, or to prove the joint specification to be inconsistent, we present some promising results for which the composition algorithm does succeed and saves significant running time. We also discuss options for extending the algorithm into a sound and complete one.
The research was supported in part by The John von Neumann Minerva Center for the Development of Reactive Systems at the Weizmann Institute of Science.
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
Abadi, M., Lamport, L., Wolper, P.: Realizable and Unrealizable Concurrent Program Specifications. In: ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller Synthesis for Timed Automata. In: IFAC Symp. on System Structure and Control, pp. 469–474 (1998)
Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic Hardware Synthesis from Specifications: A Case Study. In: Proceedings of the Design, Automation and Test in Europe, pp. 1188–1193 (2007)
Bontemps, Y., Heymans, P., Schobbens, P.Y.: From Live Sequence Charts to State Machines and Back: A Guided Tour. IEEE Trans. Software Eng. 31(12), 999–1014 (2005)
Bontemps, Y., Schobbens, P.: Synthesizing Open Reactive Systems from Scenario-Based Specifications. In: Proc. of the 3rd Int. Conf. on Application of Concurrency to System Design (ACSD 2003) (2003)
Büchi, J., Landweber, L.: Solving Sequential Conditions by Finite-State Strategies. Trans. Amer. Math. Soc. 138, 295–311 (1969)
Church, A.: Logic, Arithmetic and Automata. In: Proc. 1962 Int. Congr. Math, Upsala, pp. 23–25 (1963)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. J. on Form. Meth. in Sys. Design 19(1), 45–80 (2001)
Damm, W., Toben, T., Westphal, B.: On the Expressive Power of Live Sequence Charts. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol. 4444, pp. 225–246. Springer, Heidelberg (2007)
Emerson, E., Clarke, E.: Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming 2, 241–266 (1982)
Harding, A., Ryan, M., Schobbens, P.: A New Algorithm for Strategy Synthesis in LTL Games. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 477–492. Springer, Heidelberg (2005)
Harel, D., Kantor, A., Maoz, S.: On the Power of Play-Out for Scenario-Based Programs (to appear, 2009)
Harel, D., Kugler, H.: Synthesizing State-Based Object Systems from LSC Specifications. Int. J. of Found. of Comp. Sci (IJFCS) 13(1), 5–51 (2002)
Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart Play-Out of Behavioral Requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 378–398. Springer, Heidelberg (2002)
Harel, D., Kugler, H., Pnueli, A.: Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements. In: Kreowski, H.-J., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol. 3393, pp. 309–324. Springer, Heidelberg (2005)
Harel, D., Marelly, R.: Come Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine (2003)
Harel, D., Segall, I.: Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 485–499. Springer, Heidelberg (2007)
ITU. International Telecommunication Union Recommendation Z.120: Message Sequence Charts. Technical report (1996)
Jobstmann, B., Bloem, R.: Optimizations for LTL Synthesis. In: 6th Conf. Formal Methods in Computer Aided Design (FMCAD 2006) (2006)
Kam, N., Kugler, H., Marelly, R., Appleby, L., Fisher, J., Pnueli, A., Harel, D., Stern, M., Hubbard, E.: A Scenario-Based Approach to Modeling Development: A Prototype Model of C. Elegans Vulval Fate Specification. Developmental Biology 323(1), 1–5 (2008)
Kugler, H., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal Logic for Scenario-Based Specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 445–460. Springer, Heidelberg (2005)
Kugler, H., Plock, C., Pnueli, A.: Controller Synthesis from LSC Requirements. In: 12th International Conference on Fundamental Approaches to Software Engineering (FASE 2009). LNCS. Springer, Heidelberg (2009)
Kugler, H., Segall, I.: Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. Technical report, Microsoft Research (2009)
Kupferman, O., Piterman, N., Vardi, M.: Safraless Compositional Synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)
Kupferman, O., Vardi, M.: Safraless Decision Procedures. In: Proc. 46th IEEE Symp. on Found. of Computer Science, Pittsburgh, October 2005, pp. 531–540 (2005)
Liang, H., Dingel, J., Diskin, Z.: A Comparative Survey of Scenario-Based to State-Based Model Synthesis Approaches. In: Proc. of the Intl. Work. on Scenarios and State Machines: Models, Algs., and Tools (SCESM 2006), pp. 5–12 (2006)
Manna, Z., Waldinger, R.: A Deductive Approach to Program Synthesis. ACM Trans. Programming Languages and Systems 2, 90–121 (1980)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005)
Pnueli, A.: Extracting Controllers for Timed Automata. Technical report, NYU (2005)
Pnueli, A., Rosner, R.: On the Synthesis of a Reactive Module. In: Proc. 16th ACM Symp. Princ. of Prog. Lang, pp. 179–190 (1989)
Pnueli, A., Shahar, E.: A Platform for Combining Deductive with Algorithmic Verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 184–195. Springer, Heidelberg (1996)
Rabin, M.: Decidability of Second Order Theories and Automata on Infinite Trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)
Microsoft Research Cambridge, Scenario-Based Tool for Biological Modeling (2009), http://research.microsoft.com/SBT/
Sohail, S., Somenzi, F., Ravi, K.: A Hybrid Algorithm for LTL Games. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 309–323. Springer, Heidelberg (2008)
Sun, J., Dong, J.S.: Synthesis of Distributed Processes from Scenario-Based Specifications. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 415–431. Springer, Heidelberg (2005)
Wong-Toi, H., Dill, D.: Synthesizing Processes and Schedulers from Temporal Specifications. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 272–281. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kugler, H., Segall, I. (2009). Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. In: Kowalewski, S., Philippou, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2009. Lecture Notes in Computer Science, vol 5505. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00768-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-00768-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00767-5
Online ISBN: 978-3-642-00768-2
eBook Packages: Computer ScienceComputer Science (R0)