{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T21:40:02Z","timestamp":1750110002050,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662544570"},{"type":"electronic","value":"9783662544587"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54458-7_24","type":"book-chapter","created":{"date-parts":[[2017,3,15]],"date-time":"2017-03-15T09:22:57Z","timestamp":1489569777000},"page":"407-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Local Model Checking in a Logic for True Concurrency"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tommaso","family":"Padoan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,16]]},"reference":[{"key":"24_CR1","series-title":"EACTS Monographs","volume-title":"Unfoldings - A Partial order Approach to Model Checking","author":"J Esparza","year":"2008","unstructured":"Esparza, J., Heljanko, K.: Unfoldings - A Partial order Approach to Model Checking. EACTS Monographs. Springer, Heidelberg (2008)"},{"issue":"4\/5","key":"24_CR2","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s002360000041","volume":"37","author":"R van Glabbeek","year":"2001","unstructured":"van Glabbeek, R., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Inform. 37(4\/5), 229\u2013327 (2001)","journal-title":"Acta Inform."},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-53487-3_53","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"R Nicola","year":"1990","unstructured":"Nicola, R., Ferrari, G.L.: Observational logics and concurrency models. In: Nori, K.V., Veni Madhavan, C.E. (eds.) FSTTCS 1990. LNCS, vol. 472, pp. 301\u2013315. Springer, Heidelberg (1990). doi:10.1007\/3-540-53487-3_53"},{"key":"24_CR4","unstructured":"Bednarczyk, M.A.: Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences (1991)"},{"key":"24_CR5","unstructured":"Pinchinat, S., Laroussinie, F., Schnoebelen, P.: Logical characterization of truly concurrent bisimulation. Technical report 114, LIFIA-IMAG, Grenoble (1994)"},{"key":"24_CR6","series-title":"Time and Logic: A Computational Approach","first-page":"179","volume-title":"Branching Time and Partial Order in Temporal Logics","author":"W Penczek","year":"1995","unstructured":"Penczek, W.: Branching Time and Partial Order in Temporal Logics. Time and Logic: A Computational Approach, pp. 179\u2013228. UCL Press, London (1995)"},{"issue":"2","key":"24_CR7","first-page":"221","volume":"2","author":"M Nielsen","year":"1995","unstructured":"Nielsen, M., Clausen, C.: Games and logics for a noninterleaving bisimulation. Nordic J. Comput. 2(2), 221\u2013249 (1995)","journal-title":"Nordic J. Comput."},{"issue":"1","key":"24_CR8","first-page":"102","volume":"9","author":"J Bradfield","year":"2002","unstructured":"Bradfield, J., Fr\u00f6schle, S.: Independence-friendly modal logic and true concurrency. Nordic J. Comput. 9(1), 102\u2013117 (2002)","journal-title":"Nordic J. Comput."},{"issue":"2","key":"24_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129513000510","volume":"24","author":"I Phillips","year":"2014","unstructured":"Phillips, I., Ulidowski, I.: Event identifier logic. Math. Struct. Comput. Sci. 24(2), 1\u201351 (2014)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"4","key":"24_CR10","doi-asserted-by":"publisher","first-page":"24:1","DOI":"10.1145\/2629638","volume":"61","author":"P Baldan","year":"2014","unstructured":"Baldan, P., Crafa, S.: A logic for true concurrency. J. ACM 61(4), 24:1\u201324:36 (2014)","journal-title":"J. ACM"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Alur, R., Peled, D., Penczek, W.: Model-checking of causality properties. In: Proceedings of LICS 1995, pp. 90\u2013100. IEEE Computer Society (1995)","DOI":"10.1109\/LICS.1995.523247"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-04081-8_24","volume-title":"CONCUR 2009 - Concurrency Theory","author":"J Gutierrez","year":"2009","unstructured":"Gutierrez, J., Bradfield, J.: Model-checking games for fixpoint logics with partial order models. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 354\u2013368. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-04081-8_24"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-00596-1_5","volume-title":"Foundations of Software Science and Computational Structures","author":"J Gutierrez","year":"2009","unstructured":"Gutierrez, J.: Logics and bisimulation games for concurrency, causality and conflict. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 48\u201362. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-00596-1_5"},{"key":"24_CR14","unstructured":"Gutierrez, J.: On bisimulation and model-checking for concurrent systems with partial order semantics. Ph.D. thesis, University of Edinburgh (2011)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Madhusudan, P.: Model-checking trace event structures. In: Proceedings of LICS 2003, pp. 371\u2013380. IEEE Computer Society (2003)","DOI":"10.1109\/LICS.2003.1210077"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-17906-2_31","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"G Winskel","year":"1987","unstructured":"Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 325\u2013392. Springer, Heidelberg (1987). doi:10.1007\/3-540-17906-2_31"},{"key":"24_CR17","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/BF01178506","volume":"28","author":"E Best","year":"1991","unstructured":"Best, E., Devillers, R., Kiehn, A., Pomello, L.: Fully concurrent bisimulation. Acta Inform. 28, 231\u2013261 (1991)","journal-title":"Acta Inform."},{"key":"24_CR18","doi-asserted-by":"crossref","first-page":"357","DOI":"10.3233\/FI-1988-11404","volume":"11","author":"AM Rabinovich","year":"1988","unstructured":"Rabinovich, A.M., Trakhtenbrot, B.A.: Behaviour structures and nets. Fundam. Inform. 11, 357\u2013404 (1988)","journal-title":"Fundam. Inform."},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/BFb0013030","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"P Degano","year":"1989","unstructured":"Degano, P., Nicola, R., Montanari, U.: Partial orderings descriptions and observations of nondeterministic concurrent processes. In: Bakker, J.W., Roever, W.-P., Rozenberg, G. (eds.) REX 1988. LNCS, vol. 354, pp. 438\u2013466. Springer, Heidelberg (1989). doi:10.1007\/BFb0013030"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-54233-7_158","volume-title":"Automata, Languages and Programming","author":"W Vogler","year":"1991","unstructured":"Vogler, W.: Deciding history preserving bisimilarity. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 495\u2013505. Springer, Heidelberg (1991). doi:10.1007\/3-540-54233-7_158"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11419822_1","volume-title":"Formal Methods for Mobile Computing","author":"U Montanari","year":"2005","unstructured":"Montanari, U., Pistore, M.: History-dependent automata: an introduction. In: Bernardo, M., Bogliolo, A. (eds.) SFM-Moby 2005. LNCS, vol. 3465, pp. 1\u201328. Springer, Heidelberg (2005). doi:10.1007\/11419822_1"},{"issue":"1","key":"24_CR22","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C Stirling","year":"1991","unstructured":"Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. Theor. Comput. Sci. 89(1), 161\u2013177 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-45711-9_14","volume-title":"Formal and Natural Computing - Essays Dedicated to Grzegorz Rozenberg","author":"PS Thiagarajan","year":"2002","unstructured":"Thiagarajan, P.S.: Regular event structures and finite Petri Nets: a conjecture. In: Brauer, W., Ehrig, H., Karhum\u00e4ki, J., Salomaa, A. (eds.) Formal and Natural Computing - Essays Dedicated to Grzegorz Rozenberg. LNCS, vol. 2300, pp. 244\u2013253. Springer, Heidelberg (2002). doi:10.1007\/3-540-45711-9_14"},{"issue":"2","key":"24_CR24","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. Methods Syst. Des. 2(2), 121\u2013147 (1993)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-87531-4_12","volume-title":"Computer Science Logic","author":"G Fontaine","year":"2008","unstructured":"Fontaine, G.: Continuous fragment of the mu-calculus. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 139\u2013153. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-87531-4_12"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Carreiro, F., Facchini, A., Venema, Y., Zanasi, F.: Weak MSO: automata and expressiveness modulo bisimilarity. In: Henzinger, T.A., Miller, D. (eds.) Proceedings of CSL-LICS 2014, pp. 27:1\u201327:27. ACM Press (2014)","DOI":"10.1145\/2603088.2603101"},{"key":"24_CR27","first-page":"721","volume-title":"Handbook of Modal Logic","author":"J Bradfield","year":"2006","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 721\u2013756. Elsevier, New York (2006)"},{"key":"24_CR28","volume-title":"Handbook of Automated Reasoning","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Schlingloff, B.H.: Model checking. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"issue":"2","key":"24_CR29","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/S0890-5401(03)00064-6","volume":"184","author":"M Jurdzinski","year":"2003","unstructured":"Jurdzinski, M., Nielsen, M., Srba, J.: Undecidability of domino games and hhp-bisimilarity. Inf. Comput. 184(2), 343\u2013368 (2003)","journal-title":"Inf. Comput."},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/BFb0035386","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Penczek","year":"1997","unstructured":"Penczek, W.: Model-checking for a subclass of event structures. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 145\u2013164. Springer, Heidelberg (1997). doi:10.1007\/BFb0035386"},{"key":"24_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-61604-7_60","volume-title":"CONCUR \u201996: Concurrency Theory","author":"D Janin","year":"1996","unstructured":"Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263\u2013277. Springer, Heidelberg (1996). doi:10.1007\/3-540-61604-7_60"},{"issue":"1\u20132","key":"24_CR32","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1016\/S0304-3975(00)00034-7","volume":"258","author":"EA Emerson","year":"2001","unstructured":"Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model checking for the $$\\rm \\mu $$-calculus and its fragments. Theor. Comput. Sci. 258(1\u20132), 491\u2013522 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"24_CR33","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"R Streett","year":"1989","unstructured":"Streett, R., Emerson, E.A.: An automata theoretic decision procedure for the propositional mu-calculus. Inf. Comput. 81(3), 249\u2013264 (1989)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54458-7_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T21:23:10Z","timestamp":1750108990000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54458-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544570","9783662544587"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54458-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"16 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}