Abstract
The grand composition of n automata may have a number of states/transitions exponential in n. When it does, it seems not unreasonable for the computation of that grand composition to require exponentially many resources (time, space, or both). Conversely, if the grand composition of n automata has a number of states/transitions only linear in n, we may reasonably expect the computation of that grand composition to also require only linearly many resources.
Recently and problematically, we saw cases of linearly-sized grand compositions whose computation required exponentially many resources. We encountered these cases in the context of Reo (a graphical language for coordinating components in component-based software), constraint automata (a general formalism for modeling systems’ behavior), and our compiler for Reo based on constraint automata. Combined with earlier research on constraint automata verification, these ingredients facilitate a correctness-by-construction approach to component-based software engineering—one of the hallmarks in Sifakis’ “rigorous system design”. To achieve that ambitious goal, however, we need to solve the previously stated problem. In this paper we present such a solution.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Arbab, F.: Reo: a channel-based coordination model for component composition. MSCS 14(3), 329–366 (2004)
Arbab, F.: Puff, the magic protocol. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 169–206. Springer, Heidelberg (2011)
Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: A uniform framework for modeling and verifying components and connectors. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 247–267. Springer, Heidelberg (2009)
Baier, C., Blechmann, T., Klein, J., Klüppelholz, S., Leister, W.: Design and verification of systems with exogenous coordination using Vereofy. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 97–111. Springer, Heidelberg (2010)
Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. SCP 61(2), 75–113 (2006)
Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995, pp. 3–18 (1995)
Ghassemi, F., Tasharofi, S., Sirjani, M.: Automated mapping of Reo circuits to constraint automata. In: FSEN 2005, ENTCS, vol. 159, pp. 99–115 (2006)
Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages, and Computation (2001)
Jongmans, S.S., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comput. Sci. 22(1), 201–251 (2012)
Jongmans, S.S., Arbab, F.: Toward sequentializing overparallelized protocol code. In: ICE 2014, EPTCS, vol. 166, pp. 38–44 (2014)
Jongmans, S.S., Arbab, F.: Can high throughput atone for high latency in compiler-generated protocol code? In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 238–258. Springer, Heidelberg (2015)
Jongmans, S.S., Kappé, T., Arbab, F.: Composing constraint automata, state-by-state (Technical report). Technical report FM-1506, CWI (2015)
Klein, J., Klüppelholz, S., Stam, A., Baier, C.: Hierarchical modeling and formal verification. An industrial case study using Reo and Vereofy. In: Salaün, G., Schätz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 228–243. Springer, Heidelberg (2011)
Pourvatan, B., Rouhy, N.: An alternative algorithm for constraint automata product. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 412–422. Springer, Heidelberg (2007)
Proença, J.: Synchronous coordination of distributed components. Ph.D. thesis, Leiden University (2011)
Sifakis, J.: Rigorous system design. In: PODC 2014, p. 292 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Jongmans, SS.T.Q., Kappé, T., Arbab, F. (2016). Composing Constraint Automata, State-by-State. In: Braga, C., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2015. Lecture Notes in Computer Science(), vol 9539. Springer, Cham. https://doi.org/10.1007/978-3-319-28934-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-28934-2_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-28933-5
Online ISBN: 978-3-319-28934-2
eBook Packages: Computer ScienceComputer Science (R0)