Abstract
Constraint automata have been proposed as the operational semantics of Reo, a glue-code language for the exogenous composition and orchestration of components in a software system. In this paper we recast the theory of constraint automata into that of Büchi automata on infinite strings of records. We use records to express simultaneity constraints of I/O operations and show that every constraint automaton can be expressed as a Büchi automaton on an appropriate alphabet of records. Further, we give examples of component compositions that are expressible as Büchi automata but not as constraint automata. Finally, we show that the join composition operator for constraint automata and its counterpart for Büchi automata of records can be expressed as two basic operations on Büchi automata: alphabet extension and product.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Arbab, F.: Reo: A Channel-based Coordination Model for Component Composition. Math. Struc. in Computer Science 14(3), 329–366 (2004)
Arbab, F., Baier, C., de Boer, F., Rutten, J., Sirjani, M.: Synthesis of Reo circuites for implementation of component-connector automata specifications. In: Jacquet, J.-M., Picco, G.P. (eds.) COORDINATION 2005. LNCS, vol. 3454, pp. 236–251. Springer, Heidelberg (2005)
Arbab, F., Chothia, T., Meng, S., Moon, Y.-J.: Component Connectors with QoS Guarantees. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467. Springer, Heidelberg (2007)
Arbab, F., Rutten, J.J.M.M.: A Coinductive Calculus of Component Connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 35–56. Springer, Heidelberg (2003)
Arbab, F., Baier, C., de Boer, F., Rutten, J.: Models and temporal logics for timed component connectors. In: Proc. of the IEEE International Conference SEFM, pp. 198–207. IEEE Computer Society Press, Los Alamitos (2004)
Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modelling Component Connectors in Reo by Constraint Automata. Science of Computer Programming 61, 75–113 (2006)
Baier, C., Wolf, V.: Stochastic reasoning about channel-based component connectors. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 1–15. Springer, Heidelberg (2006)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Hayes, J.P.: Computer Architecture and Organization, 2nd edn. McGraw Hill Publishing Company, New York (1998)
Holzmann, G.J.: The Model Checker SPIN. IEEE Transactions on software engineering 23(5), 279–295 (1997)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley, Reading (2006)
Kupferman, O., Vardi, M.: Verification of Fair Transition Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Remy, D.: Efficient representation of extensible records. In: Proc. ACM SIGPLAN Workshop on ML and its applications, pp. 12–16 (1994)
Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming, 2nd edn. Addison-Wesley, Reading (2002)
Thomas, W.: Automata on Infinite Objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–191. Elsevier, Amsterdam (1990)
Vardi, M.: An Automata-Theoretic Approach to Linear Temporal Logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Izadi, M., Bonsangue, M.M. (2008). Recasting Constraint Automata into Büchi Automata. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)