{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:26:21Z","timestamp":1740108381465,"version":"3.37.3"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,7,18]],"date-time":"2017-07-18T00:00:00Z","timestamp":1500336000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s00236-017-0302-9","type":"journal-article","created":{"date-parts":[[2017,7,18]],"date-time":"2017-07-18T12:42:17Z","timestamp":1500381737000},"page":"363-400","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Event algebra for transition systems composition application to timed automata"],"prefix":"10.1007","volume":"55","author":[{"given":"Elie","family":"Fares","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4179-6063","authenticated-orcid":false,"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,18]]},"reference":[{"key":"302_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"issue":"7\u20138","key":"302_CR2","doi-asserted-by":"crossref","first-page":"889","DOI":"10.1016\/j.scico.2010.04.002","volume":"77","author":"L Aceto","year":"2012","unstructured":"Aceto, L., Birgisson, A., Ing\u00f3lfsd\u00f3ttir, A., Mousavi, M.R., Reniers, M.A.: Rule formats for determinism and idempotence. Sci. Comput. Program. 77(7\u20138), 889\u2013907 (2012)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"302_CR3","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"issue":"2","key":"302_CR4","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20133","key":"302_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2004.05.010","volume":"55","author":"F Arbab","year":"2005","unstructured":"Arbab, F.: Abstract behavior types: a foundation model for components and their composition. Sci. Comput. Program. 55(1\u20133), 3\u201352 (2005)","journal-title":"Sci. Comput. Program."},{"issue":"2\u20133","key":"302_CR6","doi-asserted-by":"crossref","first-page":"109","DOI":"10.3233\/FI-1999-402302","volume":"40","author":"A Arnold","year":"1999","unstructured":"Arnold, A., Point, G., Griffault, A., Rauzy, A.: The AltaRica formalism for describing concurrent systems. Fundam. Inf. 40(2\u20133), 109\u2013124 (1999)","journal-title":"Fundam. Inf."},{"key":"302_CR7","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: SEFM, pp. 3\u201312. IEEE Computer Society (2006)","DOI":"10.1109\/SEFM.2006.27"},{"issue":"4","key":"302_CR8","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1017\/S0960129511000697","volume":"22","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., Juhl, L., Larsen, K.G., Legay, A., Srba, J.: Extending modal transition systems with structured labels. Math. Struct. Comput. Sci. 22(4), 581\u2013617 (2012)","journal-title":"Math. Struct. Comput. Sci."},{"key":"302_CR9","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004. Revised Lectures, volume 3185 of Lecture Notes in Computer Science, pp. 200\u2013237. Springer (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"302_CR10","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This Tutorial Volume Originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichst\u00e4tt, Germany in September 2003. In Addition to Lectures Given at ACPN 2003, Additional Chapters Have Been Commissioned], Volume 3098 of Lecture Notes in Computer Science, pp. 87\u2013124. Springer (2003)","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"302_CR11","doi-asserted-by":"crossref","unstructured":"Berendsen, J., Vaandrager, F.W.: Compositional abstraction in real-time model checking. In: Cassez, F., Jard, C. (eds.) Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15\u201317, 2008. Proceedings, volume 5215 of Lecture Notes in Computer Science, pp. 233\u2013249. Springer (2008)","DOI":"10.1007\/978-3-540-85778-5_17"},{"issue":"2","key":"302_CR12","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"key":"302_CR13","doi-asserted-by":"crossref","unstructured":"Bliudze, S., Sifakis, J.: A notion of glue expressiveness for component-based systems. In: van Breugel and Chechik [36], pp. 508\u2013522","DOI":"10.1007\/978-3-540-85361-9_39"},{"key":"302_CR14","unstructured":"Bodeveix, J.-P.: http:\/\/www.irit.fr\/~Jean-Paul.Bodeveix\/COQ\/LblStr"},{"key":"302_CR15","doi-asserted-by":"crossref","unstructured":"Brauer, W., Reisig, W., Rozenberg, G. (eds). Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, 8\u201319. September 1986, Volume 255 of Lecture Notes in Computer Science. Springer (1987)","DOI":"10.1007\/978-3-540-47919-2"},{"key":"302_CR16","doi-asserted-by":"crossref","unstructured":"Br\u00e9mond-Gr\u00e9goire, P., Lee, I., Gerber, R.: ACSR: an algebra of communicating shared resources with dense time and priorities. In: Best, E. (ed.) CONCUR \u201993, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23\u201326, 1993, Proceedings, Volume 715 of Lecture Notes in Computer Science, pp. 417\u2013431. Springer (1993)","DOI":"10.1007\/3-540-57208-2_29"},{"key":"302_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Probabilistic weighted automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009\u2014Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1\u20134, 2009. Proceedings, Volume 5710 of Lecture Notes in Computer Science, pp. 244\u2013258. Springer (2009)","DOI":"10.1007\/978-3-642-04081-8_17"},{"key":"302_CR18","doi-asserted-by":"crossref","unstructured":"Cranen, S., Mousavi, M.R., Reniers, M.A.: A rule format for associativity. In: van Breugel and Chechik [36], pp. 447\u2013461","DOI":"10.1007\/978-3-540-85361-9_35"},{"key":"302_CR19","unstructured":"Farail, P., Gaufillet, P., Peres, F., Bodeveix, J.-P., Filali, M., Berthomieu, B., Rodrigo, S., Vernadat, F., Garavel, H., Lang, F.: FIACRE: an intermediate language for model verification in the TOPCASED environment. In: European Congress on Embedded Real-Time Software, ERTS\u201908 (2008)"},{"key":"302_CR20","doi-asserted-by":"crossref","unstructured":"Fares, E., Bodeveix, J.-P., Filali, M.: Event algebra for transition systems composition\u2014application to timed automata. In: Proceedings of the 2013 20th International Symposium on Temporal Representation and Reasoning, TIME \u201913, pp. 125\u2013132. IEEE Computer Society, Washington (2013)","DOI":"10.1109\/TIME.2013.23"},{"key":"302_CR21","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of $$\\mu $$ \u03bc crl. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.) Algebra of Communicating Processes: Proceedings of ACP94, the First Workshop on the Algebra of Communicating Processes, Utrecht, The Netherlands, 16\u201317 May 1994, pp. 26\u201362. Springer, London (1995)","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"302_CR22","doi-asserted-by":"publisher","unstructured":"Henzinger, T., Manna, Z., Pnueli, A.: Timed transition systems. In: de\u00a0Bakker, J., Huizing, C., de\u00a0Roever, W., Rozenberg, G. (eds): Real-Time: Theory in Practice, Volume 600 of Lecture Notes in Computer Science, pp. 226\u2013251. Springer. doi: 10.1007\/BFb0031995 (1992)","DOI":"10.1007\/BFb0031995"},{"issue":"2","key":"302_CR23","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"302_CR24","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2008.04.050","volume":"212","author":"T Hoare","year":"2008","unstructured":"Hoare, T., O\u2019Hearn, P.: Separation logic semantics for communicating processes. Electron. Notes Theor. Comput. Sci. 212, 3\u201325 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"302_CR25","doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H., Larsen, K.: The use of static constructs in a modal process logic. In: Meyer, A., Taitslin, M. (eds.) Logic at Botik \u201989, Lecture Notes in Computer Science, vol. 363, pp. 163\u2013180. Springer, Berlin (1989)","DOI":"10.1007\/3-540-51237-3_14"},{"key":"302_CR26","unstructured":"I.\u00a0O. for Standardization. Information processing systems-open systems interconnection-LOTOS\u2014a formal description technique based on the temporal ordering of observational behaviour. International standard. ISO (1989)"},{"key":"302_CR27","doi-asserted-by":"publisher","unstructured":"Larsen, K., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed) Fundamentals of Computation Theory, Volume 965 of Lecture Notes in Computer Science, pp. 62\u201388. Springer. doi: 10.1007\/3-540-60249-6_41 (1995)","DOI":"10.1007\/3-540-60249-6_41"},{"issue":"3","key":"302_CR28","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R Milner","year":"1983","unstructured":"Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25(3), 267\u2013310 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"302_CR29","volume-title":"Communication and Concurrency","author":"R Milner","year":"1995","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall International, Upper Saddle River (1995)"},{"key":"302_CR30","doi-asserted-by":"crossref","unstructured":"Mousavi, M.R., Reniers, M.A., Basten, T., Chaudron, M.R.V.: PARS: a process algebra with resources and schedulers. In: Larsen, K.G., Niebert, P. (eds) Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6\u20137, 2003. Revised Papers, Volume 2791 of Lecture Notes in Computer Science, pp. 134\u2013150. Springer (2003)","DOI":"10.1007\/978-3-540-40903-8_11"},{"issue":"1\u20132","key":"302_CR31","doi-asserted-by":"crossref","first-page":"119","DOI":"10.3233\/FI-2011-416","volume":"108","author":"J-B Raclet","year":"2011","unstructured":"Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundam. Inform. 108(1\u20132), 119\u2013149 (2011)","journal-title":"Fundam. Inform."},{"key":"302_CR32","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1997)"},{"key":"302_CR33","unstructured":"Roscoe, A.W.: On the expressiveness of CSP. https:\/\/www.cs.ox.ac.uk\/files\/1383\/expressive.pdf (2011)"},{"issue":"8","key":"302_CR34","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1093\/comjnl\/39.8.701","volume":"39","author":"E Sekerinski","year":"1996","unstructured":"Sekerinski, E., Sere, K.: A theory of prioritizing composition. Comput. J. 39(8), 701\u2013712 (1996)","journal-title":"Comput. J."},{"key":"302_CR35","unstructured":"The Coq development team. The Coq proof assistant reference manual. LogiCal Project. Version 8.4 (2013)"},{"key":"302_CR36","doi-asserted-by":"crossref","unstructured":"van Breugel, F., Chechik, M. (eds): CONCUR 2008\u2014Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19\u201322, 2008. Proceedings, Volume 5201 of Lecture Notes in Computer Science. Springer (2008)","DOI":"10.1007\/978-3-540-85361-9"},{"issue":"2","key":"302_CR37","first-page":"274","volume":"2","author":"C Verhoef","year":"1995","unstructured":"Verhoef, C.: A congruence theorem for structured operational semantics with predicates and negative premises. Nord. J. Comput. 2(2), 274\u2013302 (1995)","journal-title":"Nord. J. Comput."},{"key":"302_CR38","first-page":"1","volume-title":"Handbook of Logic in Computer Science. Chapter Models for Concurrency","author":"G Winskel","year":"1995","unstructured":"Winskel, G., Nielsen, M.: Handbook of Logic in Computer Science. Chapter Models for Concurrency, vol. 4, pp. 1\u2013148. Oxford University Press, Oxford (1995)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-017-0302-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0302-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0302-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,12]],"date-time":"2020-10-12T21:13:05Z","timestamp":1602537185000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-017-0302-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,18]]},"references-count":38,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["302"],"URL":"https:\/\/doi.org\/10.1007\/s00236-017-0302-9","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2017,7,18]]}}}