{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T21:37:01Z","timestamp":1775684221943,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540682356","type":"print"},{"value":"9783540682370","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_12","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"148-164","source":"Crossref","is-referenced-by-count":105,"title":["A Model Checking Language for Concurrent Value-Passing Systems"],"prefix":"10.1007","author":[{"given":"Radu","family":"Mateescu","sequence":"first","affiliation":[]},{"given":"Damien","family":"Thivolle","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"12_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H.R. Andersen","year":"1994","unstructured":"Andersen, H.R.: Model Checking and Boolean Graphs. TCS\u00a0126(1), 3\u201330 (1994)","journal-title":"TCS"},{"key":"12_CR2","unstructured":"ANSI. Small Computer System Interface-2. Standard X3.131-1994"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Flaisher, A., et al.: The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 211\u2013296. Springer, Heidelberg (2002)"},{"issue":"2\u20132","key":"12_CR4","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s10009-003-0114-9","volume":"5","author":"T. Arts","year":"2004","unstructured":"Arts, T., Benac Earle, C., Derrick, J.: Development of a Verified Erlang Program for Resource Locking. STTT\u00a05(2\u20132), 205\u2013220 (2004)","journal-title":"STTT"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H. Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 44\u201357. Springer, Heidelberg (2004)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"12_CR7","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"issue":"2","key":"12_CR8","first-page":"121","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. FMSD\u00a02(2), 121\u2013147 (1993)","journal-title":"FMSD"},{"key":"12_CR9","unstructured":"Dam, M.: Model Checking Mobile Processes (Full version). Research Report RR 94:1, Swedish Institute of Computer Science, Kista, Sweden (1994)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Vaandrager, F.W.: Action versus State Based Logics for Transition Systems. In: LITP 1990. Lncs, vol.\u00a0469, pp. 407\u2013419 (1990)","DOI":"10.1007\/3-540-53479-2_17"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: ICSE 1999, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"issue":"1","key":"12_CR12","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: Sometimes and Not Never Revisited: On Branching versus Linear Time Temporal Logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"12_CR13","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In: LICS 1986, pp. 267\u2013278 (1986)"},{"issue":"2","key":"12_CR14","first-page":"194","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional Dynamic Logic of Regular Programs. JCSS\u00a018(2), 194\u2013211 (1979)","journal-title":"JCSS"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, pp. 68\u201384. Springer, Heidelberg (1998)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-45614-7_23","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"H. Garavel","year":"2002","unstructured":"Garavel, H., Hermanns, H.: On Combining Functional Verification and Performance Evaluation Using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 410\u2013429. Springer, Heidelberg (2002)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-540-73368-3_18","volume-title":"Computer Aided Verification","author":"H. Garavel","year":"2007","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP\u00a02006: A Toolbox for the Construction and Analysis of Distributed Processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 158\u2013163. Springer, Heidelberg (2007)"},{"key":"12_CR18","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1016\/j.tcs.2005.06.016","volume":"343","author":"J.F. Groote","year":"2005","unstructured":"Groote, J.F., Willemse, T.A.C.: Parameterised Boolean Equation Systems. TCS\u00a0343, 332\u2013369 (2005)","journal-title":"TCS"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49253-4_8","volume-title":"Algebraic Methodology and Software Technology","author":"J.F. Groote","year":"1998","unstructured":"Groote, J.F., Mateescu, R.: Verification of Temporal Properties of Processes in a Setting with Data. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol.\u00a01548, pp. 74\u201390. Springer, Heidelberg (1998)"},{"issue":"1\u20132","key":"12_CR20","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/0304-3975(83)90097-X","volume":"27","author":"J.Y. Halpern","year":"1983","unstructured":"Halpern, J.Y., Reif, J.H.: The Propositional Dynamic Logic of Deterministic, Wellstructured Programs. TCS\u00a027(1\u20132), 127\u2013165 (1983)","journal-title":"TCS"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Hamaguchi, K., Hiraishi, H., Yajima, S.: Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity. In: CAV 1990. Lncs, vol.\u00a0531 (1990)","DOI":"10.1090\/dimacs\/003\/34"},{"key":"12_CR22","volume-title":"The SPIN Model Checker","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Reading (2003)"},{"key":"12_CR23","unstructured":"IEEE. PSL: Property Specification Language. Std. P1850, IEEE (2004)"},{"key":"12_CR24","unstructured":"ISO\/IEC. LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Int. Std. 8807, ISO \u2014 OSI, Gen\u00e8ve (1989)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11691617_8","volume-title":"Model Checking Software","author":"C. Joubert","year":"2006","unstructured":"Joubert, C., Mateescu, R.: Distributed On-the-Fly Model Checking and Test Case Generation. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 126\u2013145. Springer, Heidelberg (2006)"},{"key":"12_CR26","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 \u03bc-calculus. TCS\u00a027, 333\u2013354 (1983)","journal-title":"TCS"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/BFb0026106","volume-title":"CAAP \u201988","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G.: Proof Systems for Hennessy-Milner logic with Recursion. In: Dauchet, M., Nivat, M. (eds.) CAAP 1988. LNCS, vol.\u00a0299, pp. 215\u2013230. Springer, Heidelberg (1988)"},{"key":"12_CR28","volume-title":"VERSAL 8","author":"A. Mader","year":"1997","unstructured":"Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. In: VERSAL 8, Bertz Verlag, Berlin (1997)"},{"key":"12_CR29","unstructured":"Mateescu, R.: Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus. In: VMCAI 1998. University Ca\u2019Foscari of Venice (1998)"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/3-540-46419-0_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Mateescu","year":"2000","unstructured":"Mateescu, R.: Efficient Diagnostic Generation for Boolean Equation Systems. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 251\u2013265. Springer, Heidelberg (2000)"},{"issue":"1","key":"12_CR31","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10009-005-0194-9","volume":"8","author":"R. Mateescu","year":"2006","unstructured":"Mateescu, R.: C\u00c6SAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems. STTT\u00a08(1), 37\u201356 (2006)","journal-title":"STTT"},{"issue":"3","key":"12_CR32","first-page":"255","volume":"46","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. SCP\u00a046(3), 255\u2013281 (2003)","journal-title":"SCP"},{"key":"12_CR33","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"12_CR34","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: A Temporal Logic of Concurrent Programs. TCS\u00a013, 45\u201360 (1981)","journal-title":"TCS"},{"key":"12_CR35","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BF00265555","volume":"19","author":"J.-P. Queille","year":"1983","unstructured":"Queille, J.-P., Sifakis, J.: Fairness and Related Properties in Transition Systems \u2014 A Temporal Logic to Deal with Fairness. Acta Informatica\u00a019, 195\u2013220 (1983)","journal-title":"Acta Informatica"},{"key":"12_CR36","unstructured":"Rathke, J., Hennessy, M.: Local Model Checking for a Value-Based Modal \u03bc-calculus. Report 5\/96, Univ. of Sussex (1996)"},{"key":"12_CR37","first-page":"73","volume-title":"ASYNC 2007","author":"G. Sala\u00fcn","year":"2007","unstructured":"Sala\u00fcn, G., Serwe, W., Thonnart, Y., Vivet, P.: Formal Verification of CHP Specifications with CADP \u2014 Illustration on an Asynchronous Network-on-Chip. In: ASYNC 2007, pp. 73\u201382. IEEE, Los Alamitos (2007)"},{"key":"12_CR38","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3550-5","volume-title":"Modal and Temporal Properties of Processes","author":"C. Stirling","year":"2001","unstructured":"Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelberg (2001)"},{"key":"12_CR39","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R. Streett","year":"1982","unstructured":"Streett, R.: Propositional Dynamic Logic of Looping and Converse. Information and Control\u00a054, 121\u2013141 (1982)","journal-title":"Information and Control"},{"issue":"2","key":"12_CR40","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth First Search and Linear Graph Algorithms. SIAM J. of Computing\u00a01(2), 146\u2013160 (1972)","journal-title":"SIAM J. of Computing"},{"key":"12_CR41","unstructured":"Thomas, W.: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Lncs, vol.\u00a0354"},{"key":"12_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/3-540-55251-0_18","volume-title":"CAAP \u201992","author":"B. Vergauwen","year":"1992","unstructured":"Vergauwen, B., Lewi, J.: A Linear Algorithm for Solving Fixed-Point Equations on Transition Systems. In: Raoult, J.-C. (ed.) CAAP 1992. LNCS, vol.\u00a0581, pp. 322\u2013341. Springer, Heidelberg (1992)"},{"key":"12_CR43","unstructured":"Wolper, P.: A Translation from Full Branching Time Temporal Logic to One Letter Propositional Dynamic Logic with Looping. Unpublished manuscript (1982)"},{"issue":"1\/2","key":"12_CR44","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal Logic Can Be More Expressive. Information and Control\u00a056(1\/2), 72\u201399 (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T15:15:50Z","timestamp":1738250150000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_12","relation":{},"subject":[]}}