Abstract
Synthesis from components is the automated construction of a composite system from a library of reusable components such that the system satisfies the given specification. This is in contrast to classical synthesis, where systems are always “constructed from scratch”. In the control-flow model of composition, exactly one component is in control at a given time and control is switched to another when the component reaches an exit state. The composition can then be described implicitly by a transducer, called a composer, which statically determines how the system transitions between components.
Recently, Lustig, Nain and Vardi have shown that control-flow synthesis of deterministic composers from libraries of probabilistic components is decidable. In this work, we consider the more general case of probabilistic composers. We show that probabilistic composers are more expressive than deterministic composers, and that the synthesis problem still remains decidable.
Work supported in part by NSF grants CCF-0728882 and CNS 1049862, and BSF grant 9800096. The authors are grateful to Orna Kupferman for suggesting the study of probabilistic composers.
Chapter PDF
Similar content being viewed by others
References
Baier, C., Größer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proc. TCS 2004, pp. 493–506. Kluwer (2004)
Baier, C., Bertrand, N., Größer, M.: On Decision Problems for Probabilistic Büchi Automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 287–301. Springer, Heidelberg (2008)
Berardi, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Mecella, M.: Automatic Composition of E-services That Export Their Behavior. In: Orlowska, M.E., Weerawarana, S., Papazoglou, M.P., Yang, J. (eds.) ICSOC 2003. LNCS, vol. 2910, pp. 43–58. Springer, Heidelberg (2003)
Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Trading memory for randomness. In: QEST 2004, pp. 206–217. IEEE Computer Society (2004)
Courcoubetis, C., Yannakakis, M.: Markov Decision Processes and Regular Events. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 336–349. Springer, Heidelberg (1990)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42, 857–907 (1995)
de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Engineering Theories of Software-Intensive Systems, pp. 83–104. Springer, Heidelberg (2005)
Lustig, Y., Nain, S., Vardi, M.Y.: Synthesis from probabilistic components. In: Proc. CSL 2011. LIPICS, vol. 12, pp. 412–427 (2011)
Lustig, Y., Vardi, M.Y.: Synthesis from Component Libraries. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 395–409. Springer, Heidelberg (2009)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. POPL 1989, pp. 179–190 (1989)
Sifakis, J.: A framework for component-based construction extended abstract. In: Proc. SEFM 2005, pp. 293–300. IEEE Computer Society (2005)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. 26th FOCS 1985, pp. 327–338 (1985)
Vardi, M.Y.: Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 265–276. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nain, S., Vardi, M.Y. (2012). Synthesizing Probabilistic Composers. In: Birkedal, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2012. Lecture Notes in Computer Science, vol 7213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28729-9_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-28729-9_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28728-2
Online ISBN: 978-3-642-28729-9
eBook Packages: Computer ScienceComputer Science (R0)