Synthesis of Reo Connectors for Strategies and Controllers

• Autorzy: Baier Ch. , Klein J. , Klüppelholz S.

Identyfikatory

DOI

10.3233/FI-2014-980

• Języki publikacji: EN

Abstrakty

EN

In controller synthesis, i.e., the question whether there is a controller or strategy to achieve some objective in a given system, the controller is often realized as some kind of automaton. In the context of the exogenous coordination language Reo, where the coordination glue code between the components is realized as a network of channels, it is desirable for such synthesized controllers to also take the form of a Reo connector built from a repertoire of basic channels. In this paper, we address the automatic construction of such Reo connectors directly from a constraint automaton representation.

Słowa kluczowe

EN

reo; information retrieval system; computer software; robots; computer networks; coding theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 130, nr 1
• Strony: 1--20
• Opis fizyczny: Bibliogr. 20 poz., rys.

Twórcy

autor

Baier Ch.

• Faculty of Computer Science, Technische Universit¨at Dresden, Germany

autor

Klein J.

• Faculty of Computer Science, Technische Universit¨at Dresden, Germany

autor

Klüppelholz S.

• Faculty of Computer Science, Technische Universit¨at Dresden, Germany

Bibliografia

• [1] M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable specifications of reactive systems. In ICALP’89, volume 372 of Lecture Notes in Computer Science, pages 1–17. Springer, 1989.
• [2] R. Alur, T. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672–713, 2002.
• [3] F. Arbab. Reo: A Channel-Based Coordination Model for Component Composition. Mathematical Structures in Computer Science, 14(3):329–366, 2004.
• [4] F. Arbab, C. Baier, F. de Boer, J. Rutten, and M. Sirjani. Synthesis of Reo Circuits for Implementation of Component-Connector Automata Specifications. In Coordination’05, volume 3454 of Lecture Notes in Computer Science, pages 236–251. Springer, 2005.
• [5] E. Asarin, O. Bournez, T. Dang, O. Maler, and A. Pnueli. Effective Synthesis of Switching Controllers for Linear Systems. IEEE Special Issue on Hybrid Systems, 88:1011–1025, 2000.
• [6] E. Asarin, O. Maler, and A. Pnueli. Symbolic Controller Synthesis for Discrete and Timed Systems. In Hybrid Systems II, volume 131 of Lecture Notes in Computer Science, pages 1–20. Springer, 1995.
• [7] C. Baier, T. Blechmann, J. Klein, and S. Klüppelholz. A Uniform Framework for Modeling and Verifying Components and Connectors. In Coordination’09, volume 5521 of Lecture Notes in Computer Science, pages 247–267. Springer, 2009.
• [8] C. Baier, T. Blechmann, J. Klein, and S. Klüppelholz. Formal Verification for Components and Connectors. In FMCO’08, volume 5751 of Lecture Notes in Computer Science, pages 82–101. Springer, 2009.
• [9] C. Baier, J. Klein, and S. Klüppelholz. A Compositional Framework for Controller Synthesis. In CONCUR’11, volume 6901 of Lecture Notes in Computer Science, pages 512–527. Springer, 2011.
• [10] C. Baier, J. Klein, and S. Klüppelholz. Modeling and Verification of Components and Connectors. In SFM’11, volume 6659 of Lecture Notes in Computer Science, pages 114–147. Springer, 2011.
• [11] C. Baier, M. Sirjani, F. Arbab, and J. Rutten. Modeling Component Connectors in Reo by Constraint Automata. Science of Computer Programming, 61(2):75–113, 2006.
• [12] T. Blechmann and C. Baier. Checking equivalence for Reo networks. In FACS’07, volume 215 of Electronic Notes in Theoretical Computer Science, pages 209–226. Elsevier, 2008.
• [13] T. Blechmann, J. Klein, and S. Klüppelholz. Vereofy, Technische Universität Dresden. http://www. vereofy.de/.
• [14] Centrum Wiskunde & Informatica (CWI) Amsterdam. Extensible Coordination Tools. http://reo.project.cwi.nl/.
• [15] A. Church. Logic, arithmetic, and automata. In Proc. Int. Congress of Mathematicans, pages 23–35. Institut Mittag-Leffler, 1962.
• [16] L. de Alfaro and T. Henzinger. Interface automata. In ESEC / SIGSOFT FSE, pages 109–120. ACM, 2001.
• [17] S. Klüppelholz. Verification of Branching-Time and Alternating-Time Properties for Exogenous Coordination Models. PhD thesis, Technische Universität Dresden, Germany, 2012.
• [18] S. Klüppelholz and C. Baier. Alternating-time stream logic for multi-agent systems. Science of Computer Programming, 75(6):398–425, 2010.
• [19] A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In Proceedings of the 16th annual ACM Symposium on Principles of Programming Languages, pages 179–190. ACM Press, 1989.
• [20] W. Wonham. On the control of discrete-event systems. In Three Decades of Mathematical System Theory, volume 135 of Lecture Notes in Control and Information Sciences, pages 542–562. Springer, 1989.