{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:40:29Z","timestamp":1725550829303},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_7","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"81-96","source":"Crossref","is-referenced-by-count":16,"title":["A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems"],"prefix":"10.1007","author":[{"given":"Radu","family":"Mateescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"issue":"1","key":"7_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":"H. R. Andersen. Model checking and boolean graphs. TCS, 126(1):3\u201330, 1994.","journal-title":"TCS"},{"key":"7_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-18088-5_8","volume-title":"ICALP\u201987","author":"J. C. M. Baeten","year":"1987","unstructured":"J. C. M. Baeten and R. J. van Glabbeek. Another Look at Abstraction in Process Algebra. In ICALP\u201987, Lncs 267, pp. 84\u201394."},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201991","author":"A. Bouajjani","year":"1991","unstructured":"A. Bouajjani, J-C. Fernandez, S. Graf, C. Rodr\u00edguez, and J. Sifakis. Safety for Branching Time Semantics. In ICALP\u201991, Lncs 510."},{"issue":"2","key":"7_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Trans. on Prog. Lang. and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"key":"7_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-54233-7_129","volume-title":"ICALP\u201991","author":"R. Cleaveland","year":"1991","unstructured":"R. Cleaveland and B. Steffen. Computing behavioural relations, logically. In ICALP\u201991, Lncs 510, pp. 127\u2013138."},{"key":"7_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/3-540-55179-4_6","volume-title":"CAV\u201991","author":"R. Cleaveland","year":"1992","unstructured":"R. Cleaveland and B. Steffen. A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. In CAV\u201991, Lncs 575, pp. 48\u201358."},{"issue":"3","key":"7_CR7","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s100090050031","volume":"2","author":"X. Du","year":"1999","unstructured":"X. Du, S. A. Smolka, and R. Cleaveland. Local Model Checking and Protocol Analysis. Springer STTT Journal, 2(3):219\u2013241, 1999.","journal-title":"STTT Journal"},{"key":"7_CR8","unstructured":"E. A. Emerson and C-L. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In LICS\u201986, pp. 267\u2013278."},{"key":"7_CR9","unstructured":"A. Fantechi, S. Gnesi, and G. Ristori. From ACTL to Mu-Calculus. In ERCIM\u201992 Ws. on Theory and Practice in Verification (Pisa, Italy), IEI-CNR, pp. 3\u201310, 1992."},{"key":"7_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"CAV\u201996","author":"J.-C. Fernandez","year":"1996","unstructured":"J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP (C\u00c6SAR\/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In CAV\u201996, Lncs 1102, pp. 437\u2013440."},{"key":"7_CR11","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"J.-C. Fernandez","year":"1996","unstructured":"J-C. Fernandez, C. Jard, Th. J\u00e9ron, L. Nedelka, and C. Viho. Using On-the-Fly Verification Techniques for the Generation of Test Suites. In CAV\u201996, Lncs 1102."},{"key":"7_CR12","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201991","author":"J.-C. Fernandez","year":"1992","unstructured":"J-C. Fernandez and L. Mounier. \u201cOn the Fly\u201d Verification of Behavioural Equivalences and Preorders. In CAV\u201991, Lncs 575."},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer","year":"1979","unstructured":"M. J. Fischer and R. E. Ladner. Propositional Dynamic Logic of Regular Programs. J. of Comp. and System Sciences, (18):194\u2013211, 1979.","journal-title":"J. of Comp. and System Sciences"},{"key":"7_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"TACAS\u201998","author":"H. Garavel","year":"1998","unstructured":"H. Garavel. OPEN\/C\u00c6SAR: An Open Software Architecture for Verification, Simulation, and Testing. In TACAS\u201998, Lncs 1384, pp. 68\u201384."},{"key":"7_CR15","volume-title":"Verification of Modal Properties Using Boolean Equation Systems","author":"A. Mader","year":"1997","unstructured":"A. Mader. Verification of Modal Properties Using Boolean Equation Systems. VERSAL 8, Bertz Verlag, Berlin, 1997."},{"key":"7_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/3-540-46419-0_18","volume-title":"TACAS\u201900","author":"R. Mateescu","year":"2000","unstructured":"R. Mateescu. Efficient Diagnostic Generation for Boolean Equation Systems. In TACAS\u201900, Lncs 1785, pp. 251\u2013265."},{"key":"7_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/3-540-46002-0_20","volume-title":"TACAS\u201902","author":"R. Mateescu","year":"2002","unstructured":"R. Mateescu. Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. In TACAS\u201902, Lncs 2280, pp. 281\u2013295."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"R. Mateescu and M. Sighireanu. Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Science of Comp. Programming, 2002. To appear.","DOI":"10.1016\/S0167-6423(02)00094-1"},{"key":"7_CR19","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, 1989."},{"key":"7_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Concurrency","author":"R. Nicola De","year":"1990","unstructured":"R. De Nicola and F. W. Vaandrager. Action versus State based Logics for Transition Systems. In Semantics of Concurrency, Lncs 469, pp. 407\u2013419."},{"key":"7_CR21","volume-title":"CS R9021","author":"R. Nicola De","year":"1990","unstructured":"R. De Nicola, U. Montanari, and F. Vaandrager. Back and Forth Bisimulations. CS R9021, CWI, Amsterdam, May 1990."},{"key":"7_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Th. Comp. Sci.","author":"D. Park","year":"1981","unstructured":"D. Park. Concurrency and Automata on Infinite Sequences. In Th. Comp. Sci., Lncs 104, pp. 167\u2013183."},{"key":"7_CR23","unstructured":"R. J. van Glabbeek and W. P. Weijland. Branching-Time and Abstraction in Bisimulation Semantics. In Proc. IFIP 11th World Computer Congress, 1989."},{"key":"7_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/3-540-49519-3_18","volume-title":"FMCAD\u201998","author":"B. Yang","year":"1998","unstructured":"B. Yang, R.E. Bryant, D. R. O\u2019Hallaron, A. Biere, O. Condert, G. Janssen, R.K. Ranjan, and F. Somenzi. A Performance Study of BDD-Based Model-Checking. In FMCAD\u201998, Lncs 1522, pp. 255\u2013289."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:44:14Z","timestamp":1558982654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}