{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:55:13Z","timestamp":1740099313147,"version":"3.37.3"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030223472"},{"type":"electronic","value":"9783030223489"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-22348-9_8","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T13:04:54Z","timestamp":1561467894000},"page":"110-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["States and Events in KandISTI"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4648-4667","authenticated-orcid":false,"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0139-0421","authenticated-orcid":false,"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4562-8777","authenticated-orcid":false,"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,6,26]]},"reference":[{"issue":"5\u20136","key":"8_CR1","first-page":"83","volume":"16","author":"SA Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical considerations on modal logic. Acta Phil. Fennica 16(5\u20136), 83\u201394 (1963)","journal-title":"Acta Phil. Fennica"},{"key":"8_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"8_CR3","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"key":"8_CR4","volume-title":"Process Algebra, Cambridge Tracts in Theoretical Computer Science","author":"JCM Baeten","year":"1990","unstructured":"Baeten, J.C.M., Weijland, W.P.: Process Algebra, Cambridge Tracts in Theoretical Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)"},{"issue":"2","key":"8_CR5","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995)","journal-title":"J. ACM"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/3-540-48294-6_22","volume-title":"Static Analysis","author":"M M\u00fcller-Olm","year":"1999","unstructured":"M\u00fcller-Olm, M., Schmidt, D., Steffen, B.: Model-checking: a tutorial introduction. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330\u2013354. Springer, Heidelberg (1999). \n                      https:\/\/doi.org\/10.1007\/3-540-48294-6_22"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/Event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128\u2013147. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24756-2_8"},{"issue":"3","key":"8_CR8","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/s100090050030","volume":"2","author":"R Cleaveland","year":"1999","unstructured":"Cleaveland, R.: Pragmatics of model checking: an STTT special section. Int. J. Softw. Tools Technol. Transf. 2(3), 208\u2013218 (1999). \n                      https:\/\/doi.org\/10.1007\/s100090050030","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986). \n                      https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal Mu-Calculus. Form. Method. Sys. Design 2(2), 121\u2013147 (1993). \n                      https:\/\/doi.org\/10.1007\/BF01383878","journal-title":"Form. Method. Sys. Design"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, Mariangiola, Montanari, Ugo (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). \n                      https:\/\/doi.org\/10.1007\/3-540-11494-7_22"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings Symposium on Logic in Computer Science (LICS 1986), pp. 332\u2013344. IEEE (1986)","key":"8_CR12"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-56496-9_32","volume-title":"Computer Aided Verification","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal Mu-Calculus. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 410\u2013422. Springer, Heidelberg (1993). \n                      https:\/\/doi.org\/10.1007\/3-540-56496-9_32"},{"doi-asserted-by":"publisher","unstructured":"Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for CTL\n                      \n                        \n                      \n                      $$^*$$\n                      \n                        \n                          \n                            \n                            \u2217\n                          \n                        \n                      \n                    . In: Proceedings 10th Symposium on Logic in Computer Science (LICS 1995), pp. 388\u2013397. IEEE (1995). \n                      https:\/\/doi.org\/10.1109\/LICS.1995.523273","key":"8_CR14","DOI":"10.1109\/LICS.1995.523273"},{"issue":"3","key":"8_CR15","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255\u2013281 (2003). \n                      https:\/\/doi.org\/10.1016\/S0167-6423(02)00094-1","journal-title":"Sci. Comput. Program."},{"unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)","key":"8_CR16"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0084787","volume-title":"CONCUR \u201992","author":"O Burkart","year":"1992","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 123\u2013137. Springer, Heidelberg (1992). \n                      https:\/\/doi.org\/10.1007\/BFb0084787"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/3-540-56939-1_105","volume-title":"Automata, Languages and Programming","author":"H Hungar","year":"1993","unstructured":"Hungar, H., Steffen, B.: Local model checking for context-free processes. In: Lingas, A., Karlsson, R., Carlsson, S. (eds.) ICALP 1993. LNCS, vol. 700, pp. 593\u2013605. Springer, Heidelberg (1993). \n                      https:\/\/doi.org\/10.1007\/3-540-56939-1_105"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-15545-6_20","volume-title":"Software, Services, and Systems","author":"MH Beek ter","year":"2015","unstructured":"ter Beek, M.H., Gnesi, S., Mazzanti, F.: From EU projects to a family of model checkers. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 312\u2013328. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-15545-6_20"},{"issue":"2","key":"8_CR20","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"MH Beek ter","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119\u2013135 (2011). \n                      https:\/\/doi.org\/10.1016\/j.scico.2010.07.002","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"8_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2211616.2211619","volume":"21","author":"Alessandro Fantechi","year":"2012","unstructured":"Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A logical verification methodology for service-oriented computing. ACM Trans. Softw. Eng. Methodol. 21(3), 16:1\u201316:46 (2012). \n                      https:\/\/doi.org\/10.1145\/2211616.2211619","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-32759-9_36","volume-title":"FM 2012: Formal Methods","author":"MH Beek ter","year":"2012","unstructured":"ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450\u2013454. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-32759-9_36"},{"doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Using FMC for family-based analysis of software product lines. In: Proceedings 19th International Software Product Line Conference (SPLC 2015), pp. 432\u2013439. ACM (2015). \n                      https:\/\/doi.org\/10.1145\/2791060.2791118","key":"8_CR23","DOI":"10.1145\/2791060.2791118"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Systems of Concurrent Processes","author":"R Nicola De","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407\u2013419. Springer, Heidelberg (1990). \n                      https:\/\/doi.org\/10.1007\/3-540-53479-2_17"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-55179-4_5","volume-title":"Computer Aided Verification","author":"R Nicola De","year":"1992","unstructured":"De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action based framework for verifying logical and behavioural properties of concurrent systems. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 37\u201347. Springer, Heidelberg (1992). \n                      https:\/\/doi.org\/10.1007\/3-540-55179-4_5"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/3-540-48257-1_14","volume-title":"Applied Formal Methods \u2014 FM-Trends 98","author":"A Fantechi","year":"1999","unstructured":"Fantechi, A., Gnesi, S., Mazzanti, F., Pugliese, R., Tronci, E.: A symbolic model checker for ACTL. In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 228\u2013242. Springer, Heidelberg (1999). \n                      https:\/\/doi.org\/10.1007\/3-540-48257-1_14"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). \n                      https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"8_CR28","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-Calculus. Theoret. Comput. Sci. 27, 333\u2013354 (1983). \n                      https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theoret. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Lawford, M., Ostroff, J.S., Wonham, W.M.: Model reduction of modules for state-event temporal logics. In: Proceedings IFIP TC6 WG6.1 International Conference on Formal Description Techniques IX\/Protocol Specification, Testing and Verification XVI (FORTE\/PSTV\u201996). IFIP Conference Proceedings, vol. 69, pp. 263\u2013278. Chapman & Hall, Ltd. (1996)","key":"8_CR29","DOI":"10.1007\/978-0-387-35079-0_16"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1007\/3-540-56610-4_95","volume-title":"TAPSOFT\u201993: Theory and Practice of Software Development","author":"S Graf","year":"1993","unstructured":"Graf, S., Loiseaux, C.: Property preserving abstractions under parallel composition. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993. LNCS, vol. 668, pp. 644\u2013657. Springer, Heidelberg (1993). \n                      https:\/\/doi.org\/10.1007\/3-540-56610-4_95"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-74128-2_8","volume-title":"Model Checking and Artificial Intelligence","author":"C Pecheur","year":"2007","unstructured":"Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt 2006. LNCS (LNAI), vol. 4428, pp. 113\u2013128. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74128-2_8"},{"doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings 3rd Symposium on Logic in Computer Science (LICS 1988), pp. 203\u2013210. IEEE (1988). \n                      https:\/\/doi.org\/10.1109\/LICS.1988.5119","key":"8_CR32","DOI":"10.1109\/LICS.1988.5119"},{"key":"8_CR33","first-page":"94","volume":"95","author":"A Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., W\u0105sowski, A.: 20 years of modal and mixed specifications. Bull. EATCS 95, 94\u2013129 (2008)","journal-title":"Bull. EATCS"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-319-63121-9_3","volume-title":"Models, Algorithms, Logics and Tools","author":"J K\u0159et\u00ednsk\u00fd","year":"2017","unstructured":"K\u0159et\u00ednsk\u00fd, J.: 30 years of modal transition systems: survey of extensions and analysis. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 36\u201374. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63121-9_3"},{"key":"8_CR35","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/B978-044482830-9\/50022-9","volume-title":"Handbook of Process Algebra","author":"Julian Bradfield","year":"2001","unstructured":"Bradfield, J.C., Stirling, C.: Modal logics and \n                      \n                        \n                      \n                      $$\\mu $$\n                      \n                        \n                          \u03bc\n                        \n                      \n                    -Calculi: an introduction. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 293\u2013330. Elsevier (2001). \n                      https:\/\/doi.org\/10.1016\/B978-044482830-9\/50022-9"},{"key":"8_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-69108-1_20","volume-title":"Application and Theory of Petri Nets 1998","author":"E Kindler","year":"1998","unstructured":"Kindler, E., Vesper, T.: ESTL: a temporal logic for events and states. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, pp. 365\u2013384. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/3-540-69108-1_20"},{"key":"8_CR37","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-79707-4_11","volume-title":"Formal Methods for Industrial Critical Systems","author":"MH Beek ter","year":"2008","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: An action\/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 133\u2013148. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-79707-4_11"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/BFb0015727","volume-title":"Automata, Languages and Programming","author":"A Pnueli","year":"1985","unstructured":"Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15\u201332. Springer, Heidelberg (1985). \n                      https:\/\/doi.org\/10.1007\/BFb0015727"},{"issue":"1","key":"8_CR40","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/inco.1994.1028","volume":"110","author":"B Steffen","year":"1994","unstructured":"Steffen, B., Ing\u00f3lfsd\u00f3ttir, A.: Characteristic formulae for processes with divergence. Inf. Comput. 110(1), 149\u2013163 (1994). \n                      https:\/\/doi.org\/10.1006\/inco.1994.1028","journal-title":"Inf. Comput."},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-20401-2_18","volume-title":"Rigorous Software Engineering for Service-Oriented Systems","author":"S Gnesi","year":"2011","unstructured":"Gnesi, S., Mazzanti, F.: An abstract, on the fly framework for the verification of service-oriented systems. In: Wirsing, M., H\u00f6lzl, M. (eds.) Rigorous Software Engineering for Service-Oriented Systems. LNCS, vol. 6582, pp. 390\u2013407. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-20401-2_18"},{"doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Mazzanti, F., Gnesi, S.: CMC-UMC: a framework for the verification of abstract service-oriented properties. In: Proceedings 24th Symposium on Applied Computing (SAC 2009), pp. 2111\u20132117. ACM (2009). \n                      https:\/\/doi.org\/10.1145\/1529282.1529751","key":"8_CR42","DOI":"10.1145\/1529282.1529751"},{"issue":"2","key":"8_CR43","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.jlamp.2015.11.006","volume":"85","author":"MH Beek ter","year":"2016","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85(2), 287\u2013315 (2016). \n                      https:\/\/doi.org\/10.1016\/j.jlamp.2015.11.006","journal-title":"J. Log. Algebr. Meth. Program."},{"issue":"1","key":"8_CR44","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985). \n                      https:\/\/doi.org\/10.1145\/2455.2460","journal-title":"J. ACM"},{"key":"8_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-68237-0_12","volume-title":"FM 2008: Formal Methods","author":"R Mateescu","year":"2008","unstructured":"Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148\u2013164. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-68237-0_12"},{"doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Mazzanti, F.: VMC: recent advances and challenges ahead. In: Proceedings 18th International Software Product Line Conference (SPLC 2014), vol. 2, pp. 70\u201377. ACM (2014). \n                      https:\/\/doi.org\/10.1145\/2647908.2655969","key":"8_CR46","DOI":"10.1145\/2647908.2655969"},{"key":"8_CR47","series-title":"AINSC","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-642-19937-0_2","volume-title":"ISAmI 2011","author":"F Corno","year":"2011","unstructured":"Corno, F., Sanaullah, M.: Design time methodology for the formal verification of intelligent domotic environments. ISAmI 2011. AINSC, vol. 92, pp. 9\u201316. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-19937-0_2"},{"doi-asserted-by":"publisher","unstructured":"Corno, F., Sanaullah, M.: Formal verification of device state chart models. In: Proceedings 7th International Conference on Intelligent Environments (IE 2011), pp. 66\u201373. IEEE (2011). \n                      https:\/\/doi.org\/10.1109\/IE.2011.36","key":"8_CR48","DOI":"10.1109\/IE.2011.36"},{"key":"8_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-319-10702-8_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"F Mazzanti","year":"2014","unstructured":"Mazzanti, F., Spagnolo, G.O., Della Longa, S., Ferrari, A.: Deadlock avoidance in train scheduling: a model checking approach. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 109\u2013123. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-10702-8_8"},{"key":"8_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-319-06200-6_22","volume-title":"NASA Formal Methods","author":"F Mazzanti","year":"2014","unstructured":"Mazzanti, F., Spagnolo, G.O., Ferrari, A.: Designing a deadlock-free train scheduler: a model checking approach. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 264\u2013269. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-06200-6_22"},{"issue":"3","key":"8_CR51","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-018-0488-3","volume":"20","author":"F Mazzanti","year":"2018","unstructured":"Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Towards formal methods diversity in railways: an experience report with seven frameworks. Int. J. Softw. Tools Technol. Transf. 20(3), 263\u2013288 (2018). \n                      https:\/\/doi.org\/10.1007\/s10009-018-0488-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"publisher","unstructured":"Fantechi, A., Haxthausen, A.E., Nielsen, M.B.R.: Model checking geographically distributed interlocking systems using UMC. In: Proceedings 25th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2017), pp. 278\u2013286. IEEE (2017). \n                      https:\/\/doi.org\/10.1109\/PDP.2017.66","key":"8_CR52","DOI":"10.1109\/PDP.2017.66"},{"issue":"1","key":"8_CR53","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/s11235-016-0271-2","volume":"66","author":"F Paganelli","year":"2017","unstructured":"Paganelli, F., Ambra, T., Fantechi, A., Giuli, D.: Formalizing REST APIs for web-based communication and SIP interworking. Telecommun. Syst. 66(1), 75\u201393 (2017). \n                      https:\/\/doi.org\/10.1007\/s11235-016-0271-2","journal-title":"Telecommun. Syst."},{"issue":"16","key":"8_CR54","doi-asserted-by":"publisher","first-page":"2933","DOI":"10.1002\/sec.1220","volume":"8","author":"A Aldini","year":"2015","unstructured":"Aldini, A.: Modeling and verification of trust and reputation systems. Secur. Comm. Netw. 8(16), 2933\u20132946 (2015). \n                      https:\/\/doi.org\/10.1002\/sec.1220","journal-title":"Secur. Comm. Netw."},{"issue":"2","key":"8_CR55","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3155337","volume":"28","author":"Alessandro Aldini","year":"2018","unstructured":"Aldini, A.: Design and verification of trusted collective adaptive systems. ACM Trans. Model. Comput. Simul. 28(2), 9:1\u20139:27 (2018). \n                      https:\/\/doi.org\/10.1145\/3155337","journal-title":"ACM Transactions on Modeling and Computer Simulation"}],"container-title":["Lecture Notes in Computer Science","Models, Mindsets, Meta: The What, the How, and the Why Not?"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22348-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T13:19:56Z","timestamp":1561468796000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22348-9_8"}},"subtitle":["A Retrospective"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030223472","9783030223489"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22348-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"26 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}