{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:13:36Z","timestamp":1725491616717},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540744061"},{"type":"electronic","value":"9783540744078"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-74407-8_9","type":"book-chapter","created":{"date-parts":[[2007,8,18]],"date-time":"2007-08-18T10:30:48Z","timestamp":1187433048000},"page":"120-135","source":"Crossref","is-referenced-by-count":24,"title":["Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems"],"prefix":"10.1007","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[]},{"given":"Bas","family":"Ploeger","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]},{"given":"Tim A. C.","family":"Willemse","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"9_CR1","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"9_CR2","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. Theoretical Computer Science\u00a0126(1), 3\u201330 (1994)","journal-title":"Theoretical Computer Science"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-60045-0_47","volume-title":"Computer Aided Verification","author":"H.R. Andersen","year":"1995","unstructured":"Andersen, H.R., Vergauwen, B.: Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 142\u2013154. Springer, Heidelberg (1995)"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(96)00034-8","volume":"58","author":"T. Basten","year":"1996","unstructured":"Basten, T.: Branching bisimilarity is an equivalence indeed! Information Processing Letters\u00a058, 141\u2013147 (1996)","journal-title":"Information Processing Letters"},{"key":"9_CR5","first-page":"25","volume":"14","author":"T. Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks\u00a014, 25\u201359 (1987)","journal-title":"Computer Networks"},{"key":"9_CR6","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence checking for infinite systems using parameterized boolean equation systems. CS-Report 07-14, Technische Universiteit Eindhoven (2007)","DOI":"10.1007\/978-3-540-74407-8_9"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-54233-7_129","volume-title":"Automata, Languages and Programming","author":"R. Cleaveland","year":"1991","unstructured":"Cleaveland, R., Steffen, B.: Computing behavioural relations, logically. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) Automata, Languages and Programming. LNCS, vol.\u00a0510, pp. 127\u2013138. Springer, Heidelberg (1991)"},{"issue":"1","key":"9_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-006-0004-3","volume":"29","author":"W. Fokkink","year":"2006","unstructured":"Fokkink, W., Pang, J., van de Pol, J.: Cones and foci: A mechanical framework for protocol verification. Formal Methods in System Design\u00a029(1), 1\u201331 (2006)","journal-title":"Formal Methods in System Design"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"R. Glabbeek van","year":"1993","unstructured":"van Glabbeek, R.: The Linear Time - Branching Time Spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 66\u201381. Springer, Heidelberg (1993)"},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. Glabbeek van","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM\u00a043, 555\u2013600 (1996)","journal-title":"Journal of the ACM"},{"key":"9_CR12","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)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/BFb0014338","volume-title":"Algebraic Methodology and Software Technology","author":"J.F. Groote","year":"1996","unstructured":"Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol.\u00a01101, pp. 536\u2013550. Springer, Heidelberg (1996)"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"1151","DOI":"10.1016\/B978-044482830-9\/50035-7","volume-title":"Handbook of Process Algebra","author":"J.F. Groote","year":"2001","unstructured":"Groote, J.F., Reniers, M.: Algebraic process verification. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 1151\u20131208. Elsevier, Amsterdam (2001)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/BFb0032063","volume-title":"Automata, Languages and Programming","author":"J.F. Groote","year":"1990","unstructured":"Groote, J.F., Vaandrager, F.W.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M.S. (ed.) Automata, Languages and Programming. LNCS, vol.\u00a0443, pp. 626\u2013638. Springer, Heidelberg (1990)"},{"issue":"3","key":"9_CR16","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.scico.2004.08.002","volume":"56","author":"J.F. Groote","year":"2005","unstructured":"Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Science of Computer Programming\u00a056(3), 251\u2013273 (2005)","journal-title":"Science of Computer Programming"},{"issue":"3","key":"9_CR17","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. Theoretical Computer Science\u00a0343(3), 332\u2013369 (2005)","journal-title":"Theoretical Computer Science"},{"key":"9_CR18","unstructured":"Kwak, H., Choi, J., Lee, I., Philippou, A.: Symbolic weak bisimulation for value-passing calculi. Technical Report, MS-CIS-98-22, Department of Computer and Information Science, University of Pennsylvania (1998)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-61604-7_47","volume-title":"CONCUR \u201996: Concurrency Theory","author":"H. Lin","year":"1996","unstructured":"Lin, H.: Symbolic transition graph with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 50\u201365. Springer, Heidelberg (1996)"},{"issue":"3","key":"9_CR20","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI Quarterly\u00a02(3), 219\u2013246 (1989)","journal-title":"CWI Quarterly"},{"key":"9_CR21","unstructured":"Mader, A.: Verification of modal properties using boolean equation systems. PhD Thesis, VERSAL 8, Bertz Verlag, Berlin (1997)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/3-540-36577-X_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R.: A generic on-the-fly solver for alternation-free boolean equation systems. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 81\u201396. Springer, Heidelberg (2003)"},{"key":"9_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980)"},{"key":"9_CR24","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"issue":"1","key":"9_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes (Part I\/II). Information and Computation\u00a0100(1), 1\u201377 (1992)","journal-title":"Information and Computation"},{"issue":"6","key":"9_CR26","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM Journal of Computing\u00a016(6), 973\u2013989 (1987)","journal-title":"SIAM Journal of Computing"},{"issue":"2","key":"9_CR27","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics\u00a05(2), 285\u2013309 (1955)","journal-title":"Pacific Journal of Mathematics"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/11562436_8","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"D. Zhang","year":"2005","unstructured":"Zhang, D., Cleaveland, R.: Fast generic model-checking for data-based systems. In: Wang, F. (ed.) FORTE 2005. LNCS, vol.\u00a03731, pp. 83\u201397. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2007 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74407-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T03:57:01Z","timestamp":1556769421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74407-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540744061","9783540744078"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74407-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}