{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:18:48Z","timestamp":1740028728603,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":78,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434771"},{"type":"electronic","value":"9783540460176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46017-9_4","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:13Z","timestamp":1269897133000},"page":"14-21","source":"Crossref","is-referenced-by-count":3,"title":["Abstraction in Software Model Checking: Principles and Practice"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Dams","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,23]]},"reference":[{"key":"4_CR1","unstructured":"Nina Amla, Robert P. Kurshan, and Kedar S. Namjoshi. AutoAbs: Syntax-directed program abstraction, 2002. Submitted."},{"key":"4_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-58201-0_82","volume-title":"Automata, Languages and Programming","author":"A. Aziz","year":"1994","unstructured":"Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. Equivalences for fair Kripke structures. In Serge Abiteboul and Eli Shamir, editors, Automata, Languages and Programming, number 820 in LNCS, pages 364\u2013375, Springer-Verlag, Berlin, 1994."},{"key":"4_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-58179-0_65","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1994","unstructured":"Adnan Aziz, Thomas R. Shiple, Vigyan Singhal, and Alberto L. Sangiovanni-Vincentelli. Formula-dependent equivalence for compositional CTL model checking. In David L. Dill, editor, Computer Aided Verification, number 818 in LNCS, pages 324\u2013337, Springer-Verlag, Berlin, 1994."},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Journal of Theoretical Computer Science, 59:115\u2013131, 1988.","journal-title":"Journal of Theoretical Computer Science"},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-54233-7_126","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"1991","unstructured":"A. Bouajjani, J.C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching time semantics. In J. Leach Albert, B. Monien, and M. Rodr\u00edguez Artalejo, editors, Automata, Languages and Programming, number 510 in LNCS, pages 76\u201392, Springer-Verlag, NewYork, 1991."},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18:247\u2013269, 1992.","journal-title":"Science of Computer Programming"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Glenn Bruns and Patrice Godefroid. Model checking partial state spaces with 3-valued temporal logics. In Halbwachs and Peled [HP99], pages 274\u2013287.","DOI":"10.1007\/3-540-48683-6_25"},{"issue":"1","key":"4_CR8","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1023\/A:1008697817793","volume":"6","author":"R. Bharadwaj","year":"1999","unstructured":"Ramesh Bharadwaj and Constance L. Heitmeyer. Model checking complete requirements specifications using abstraction. Automated Software Engineering: An International Journal, 6(1):37\u201368, January 1999.","journal-title":"Automated Software Engineering: An International Journal"},{"key":"4_CR9","unstructured":"G. Brat, K. Havelund, S. Park, and W. Visser. Model checking programs. In IEEE International Conference on Automated Software Engineering (ASE), 2000."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Hu and Vardi [HV98], pages 319\u2013331.","DOI":"10.1007\/BFb0028755"},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/3-540-45352-0_24","volume-title":"Verifying universal properties of parameterized networks","author":"K. Baukus","year":"2000","unstructured":"Kai Baukus, Yassine Lakhnech, and Karsten Stahl. Verifying universal properties of parameterized networks. In M. Joseph, editor, Proceedings of the Sixth International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT2000, number 1926 in LNCS, pages 291\u2013303, Springer, Berlin, 2000."},{"issue":"5","key":"4_CR12","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/381694.378846","volume":"36","author":"T. Ball","year":"2001","unstructured":"Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Automatic predicate abstraction of C programs. SIGPLAN Notices, 36(5):203\u2013213, 2001.","journal-title":"SIGPLAN Notices"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. Relative completeness of abstraction refinement for software model checking. To appear in TACAS 2002.","DOI":"10.1007\/3-540-46002-0_12"},{"key":"4_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BFb0036900","volume-title":"Automata, Languages and Programming","author":"S. D. Brookes","year":"1983","unstructured":"Stephen D. Brookes and William C. Rounds. Behavioural equivalence relations induced by programming logics. In J. Diaz, editor, Automata, Languages and Programming, number 154 in LNCS, pages 97\u2013108, Springer-Verlag, Berlin, 1983."},{"key":"4_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Thomas Ball and Sriram K. Rajamani. Automatically validating temporal safety properties of interfaces. In Matthew Dwyer, editor, Model Checking Software, number 2057 in LNCS, pages 103\u2013122, Springer, Berlin, 2001."},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J. Buchi","year":"1960","unstructured":"J. Buchi. Weak second-order arithmetic and finite automata. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 6:66\u201392, 1960.","journal-title":"Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik"},{"key":"4_CR17","volume-title":"Cambridge Tracts in Theoretical Computer Science","author":"J.C.M. Baeten","year":"1990","unstructured":"J.C.M. Baeten and W.P. Weijland. Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1990."},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACMSymp. on Principles of Programming Languages, pages 238\u2013252, LosAngeles, California, 1977.","DOI":"10.1145\/512950.512973"},{"key":"4_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/3-540-44685-0_30","volume-title":"Efficient multiple-valued model-checking using lattice representations","author":"M. Chechik","year":"2001","unstructured":"Marsha Chechik, Benet Devereux, Steve Easterbrook, Albert Y. C. Lai, and Victor Petrovykh. Efficient multiple-valued model-checking using lattice representations. In K. G. Larsen and M. Nielsen, editors, International Conference on Concurrency Theory, number 2154 in LNCS, pages 441\u2013455, Springer, Berlin, 2001."},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In Emerson and Sistla [ES00], pages 154\u2013169.","DOI":"10.1109\/TIME.2003.1214874"},{"issue":"5","key":"4_CR21","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR22","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, Cambridge, Mass., 1999."},{"key":"4_CR23","unstructured":"Ching-Tsun Chou. A simple treatment of property preservation via simulation. Technical Report 950014, Comp. Sc. Dept., University of California at Los Angeles, March 1995."},{"key":"4_CR24","unstructured":"R. Cleaveland, S. P. Iyer, and D. Yankelevich. Abstractions for preserving all CTL* formulae. Technical Report 94-03, Dept. of Comp. Sc., North Carolina State University, Raleigh, NC 27695, April 1994."},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Michael Colon and Henny Sipma. Synthesis of linear ranking functions. In Margaria and Yi [MY01], pages 67\u201381.","DOI":"10.1007\/3-540-45319-9_6"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Michael Colon and Tomas E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In Hu and Vardi [HV98], pages 293\u2013304.","DOI":"10.1007\/BFb0028753"},{"key":"4_CR27","unstructured":"Dennis Ren\u00e9 Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, P.O. Box 513, 5600MB Eindhoven, The Netherlands, July 1996."},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Satyaki Das, David L. Dill, and Seungjoon Park. Experience with predicate abstraction. In Halbwachs and Peled [HP99], pages 160\u2013171.","DOI":"10.1007\/3-540-48683-6_16"},{"key":"4_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/3-540-56922-7_39","volume-title":"Computer Aided Verification","author":"D. Dams","year":"1993","unstructured":"Dennis Dams, Rob Gerth, and Orna Grumberg. Generation of reduced models for checking fragments of CTL. In Costas Courcoubetis, editor, Computer Aided Verification, number 697 in LNCS, pages 479\u2013490, Springer-Verlag, Berlin, 1993."},{"key":"4_CR30","unstructured":"Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems: Abstractions preserving \u2200CTL*, \u2203CTL* and CTL*. In E.-R. Olderog, editor, Proceedings of the IFIP WG2.1\/WG2.2\/WG2.3Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), IFIP Transactions, Amsterdam, June 1994. North-Holland\/Elsevier."},{"key":"4_CR31","unstructured":"Dennis Dams, Rob Gerth, and Orna Grumberg. Fair model checking of abstractions (extended abstract). In Michael Leuschel, Andreas Podelski, C.R. Ramakrishnan, and Ulrich Ultes-Nitsche, editors, Proceedings of theWorkshop on Verification and Computational Logic (VCL\u20192000), number DSSE-TR-2000-6, University of Southampton, July 2000."},{"key":"4_CR32","unstructured":"Dennis Dams, Rob Gerth, and Orna Grumberg. A heuristic for the automatic generation of ranking functions. In Ganesh Gopalakrishnan, editor, Workshop on Advances in Verification (WAVe\u201900), pages 1\u20138, School of Computing, university of Utah, July 2000."},{"key":"4_CR33","series-title":"Lect Notes Comput Sci","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","year":"1999","unstructured":"Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink, editors. Theoretical and Practical Aspects of SPIN Model Checking, number 1680 in LNCS, Springer, Berlin, 1999."},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Dennis Dams, William Hesse, and Gerard Holzmann. Abstracting C with abC, 2002. Submitted.","DOI":"10.1007\/3-540-45657-0_43"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Matthew Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, and Hongjun Zheng. Tool-supported program abstraction for finite-state verification. In Proceedings of the 23rd International Conference on Software Engineering, Toronto, Canada, May 12\u201319 2001. ICSE 2001, IEEE Computer Society.","DOI":"10.1109\/ICSE.2001.919092"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Maria del Mar Gallardo and Pedro Merino. A framework for automatic construction of abstract promela models. In Dams et al. [DGLM99], pages 184\u2013199.","DOI":"10.1007\/3-540-48234-2_15"},{"key":"4_CR37","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/BF00264365","volume":"24","author":"R. Nicola De","year":"1987","unstructured":"Rocco De Nicola. Extensional equivalences for transition systems. Acta Informatica, 24:211\u2013237, 1987.","journal-title":"Acta Informatica"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Rocco De Nicola and Frits Vaandrager. Three logics for branching bisimulation. In 1990 IEEE Fifth Annual Symposium on Logic in Computer Science, pages 118\u2013129, Los Alamitos, CA, 1990. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1990.113739"},{"key":"4_CR39","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification","year":"2000","unstructured":"E. Allen Emerson and A. Prasad Sistla, editors. Computer Aided Verification, number 1855 in LNCS, Springer, Berlin, 2000."},{"issue":"3\u20134","key":"4_CR40","first-page":"335","volume":"15","author":"M. Fitting","year":"1991","unstructured":"Melvin Fitting. Many-valued modal logics. Fundamenta Informaticae, 15(3\u20134):335\u20133, 1991.","journal-title":"Fundamenta Informaticae"},{"key":"4_CR41","series-title":"Lect Notes Comput Sci","volume-title":"Many-valued modal logics II","author":"M. C. Fitting","year":"1992","unstructured":"Melvin C. Fitting. Many-valued modal logics II. In A. Nerode and M. Taitslin, editors, Proc. LFCS\u201992, number 620 in LNCS. Springer-Verlag, 1992."},{"key":"4_CR42","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"Abstraction-based model checking using modal transition systems","author":"P. Godefroid","year":"2001","unstructured":"Patrice Godefroid, Michael Huth, and Radha Jagadeesan. Abstraction-based model checking using modal transition systems. In K. G. Larsen and M. Nielsen, editors, International Conference on Concurrency Theory, number 2154 in LNCS, pages 426\u2013440, Springer, Berlin, 2001."},{"key":"4_CR43","volume-title":"ACM Monograph Series","author":"A. Ginzburg","year":"1968","unstructured":"A. Ginzburg. Algebraic Theory of Automata. ACM Monograph Series. Academic Press, NewYork\/London, 1968."},{"key":"4_CR44","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/BFb0084794","volume-title":"CONCUR\u2019 92","author":"U. Goltz","year":"1992","unstructured":"Ursula Goltz, Ruurd Kuiper, and Wojciech Penczek. Propositional temporal logics and equivalences. In W.R. Cleaveland, editor, CONCUR\u2019 92, number 630 in LNCS, pages 222\u2013236, Springer-Verlag, Berlin, 1992."},{"key":"4_CR45","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"Incompleteness, counterexamples and refinements in abstract model-checking","author":"R. Giacobazzi","year":"2001","unstructured":"R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples and refinements in abstract model-checking. In P. Cousot, editor, Proc. of The 8th International Static Analysis Symposium, SAS\u201901, volume 2126 of Lecture Notes in Computer Science, pages 356\u2013373. Springer-Verlag, 2001."},{"key":"4_CR46","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-13345-3_20","volume-title":"A modal characterization of observational congruence on finite terms of CCS","author":"S. Graf","year":"1984","unstructured":"S. Graf and J. Sifakis. A modal characterization of observational congruence on finite terms of CCS. In Jan Paredaens, editor, Proc. of the Eleventh International Colloquium on Automata Languages and Programming (ICALP), number 172 in LNCS, pages 222\u2013234, Springer-Verlag, Berlin, 1984."},{"key":"4_CR47","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Computer Aided Verification, number 1254 in LNCS, pages 72\u201383, Springer, Berlin, 1997."},{"key":"4_CR48","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/BFb0032063","volume-title":"Automata, Languages and Programming","author":"J. F. Groote","year":"1990","unstructured":"Jan Friso Groote and Frits Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In M. S. Paterson, editor, Automata, Languages and Programming, number 443 in LNCS, pages 626\u2013638, Springer-Verlag, New York, 1990."},{"key":"4_CR49","unstructured":"R. J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). In G. X. Ritter, editor, Information Processing 89, pages 613\u2013618, Amsterdam, 1989. North-Holland."},{"issue":"4","key":"4_CR50","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026599015809","volume":"13","author":"J. Hatcliff","year":"2000","unstructured":"John Hatcliff, Matthew B. Dwyer, and Hongjun Zheng. Slicing software for model construction. Higher-Order and Symbolic Computation, 13(4):315\u2013353, 2000.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"4_CR51","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/BFb0055332","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"C. L. Heitmeyer","year":"1998","unstructured":"Constance L. Heitmeyer. On the need for practical formal methods. In A.P. Ravn and H. Rischel, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, number 1486 in LNCS, pages 18\u201326, Springer, Berlin, 1998."},{"key":"4_CR52","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Michael Huth, Radha Jagadeesan, and David A. Schmidt. Modal transition systems: A foundation for three-valued program analysis. In D. Sands, editor, Programming Languages and Systems, number 2028 in LNCS, pages 155\u2013169, Springer, Berlin, 2001."},{"key":"4_CR53","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-10003-2_79","volume-title":"On observing nondeterminism and concurrency","author":"M. Hennessy","year":"1980","unstructured":"Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In J.W. de Bakker and J. van Leeuwen, editors, Proc. of the Seventh International Colloquium on Automata Languages and Programming (ICALP), number 85 in LNCS, pages 299\u2013309, Springer-Verlag, Berlin, 1980."},{"key":"4_CR54","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann. From code to models. In Proc. 2nd Int. Conf. on Applications of Concurrency to System Design, pages 3\u201310, Newcastle upon Tyne, U.K., June 2001.","DOI":"10.1109\/CSD.2001.981759"},{"key":"4_CR55","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/B978-0-12-417750-5.50022-1","volume-title":"Theory of Machines and Computations","author":"J. Hopcroft","year":"1971","unstructured":"John Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Zvi Kohavi and Azaria Paz, editors, Theory of Machines and Computations, pages 189\u2013196, Academic Press, NewYork, 1971."},{"key":"4_CR56","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification","year":"1999","unstructured":"Nicolas Halbwachs and Doron Peled, editors. Computer Aided Verification, number 1633 in LNCS, Springer, Berlin, 1999."},{"key":"4_CR57","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann and Margaret H. Smith. An automated verification method for distributed systems software based on model extraction. IEEE Trans. on Software Engineering, 28(4), April 2002.","DOI":"10.1109\/TSE.2002.995426"},{"key":"4_CR58","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J. E. Hopcroft","year":"1979","unstructured":"John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Massachusetts, 1979."},{"key":"4_CR59","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028725","volume-title":"Computer Aided Verification","author":"A. J. Hu","year":"1998","unstructured":"Alan J. Hu and Moshe Y. Vardi, editors. Computer Aided Verification, number 1427 in LNCS, Springer, Berlin, 1998."},{"key":"4_CR60","unstructured":"Peter Kelb. Abstraktionstechniken f\u00fcr automatische Verifikationsmethoden. PhD thesis, Carl von Ossietzky University of Oldenburg, Germany, December 1995."},{"key":"4_CR61","series-title":"Lect Notes Comput Sci","first-page":"307","volume-title":"Verification by augmented abstraction: The automata-theoretic view","author":"Y. Kesten","year":"1999","unstructured":"Y. Kesten, A. Pnueli, and M. Vardi. Verification by augmented abstraction: The automata-theoretic view. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL-99), LNCS, pages 307\u2013321, Springer, Berlin, 1999."},{"key":"4_CR62","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P.C. Kanellakis","year":"1990","unstructured":"P.C. Kanellakis and S.A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86:43\u201368, 1990.","journal-title":"Information and Computation"},{"key":"4_CR63","doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"4_CR64","doi-asserted-by":"crossref","unstructured":"Y. Lakhnech, S. Bensalem, S. Berezin, and S. Owre. Incremental verification by abstraction. In Margaria and Yi [MY01], pages 98\u2013112.","DOI":"10.1007\/3-540-45319-9_8"},{"key":"4_CR65","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:11\u201344, January 1995.","journal-title":"Formal Methods in System Design"},{"key":"4_CR66","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen and Bent Thomsen. Amodal process logic. In 1988 IEEE Symposium on Logic in Computer Science, pages 203\u2013210, Computer Society Press,Washington, 1988.","DOI":"10.1109\/LICS.1988.5119"},{"key":"4_CR67","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Second International Joint Conference on Artificial Intelligence, pages 481\u2013489, British Computer Society, London, 1971."},{"key":"4_CR68","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"R. Milner. A Calculus of Communicating Systems. Number 92 in LNCS. Springer-Verlag, Berlin, 1980."},{"key":"4_CR69","series-title":"Lect Notes Comput Sci","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2001","unstructured":"Tiziana Margaria and Wang Yi, editors. Tools and Algorithms for the Construction and Analysis of Systems, number 2031 in LNCS, Springer, Berlin, 2001."},{"key":"4_CR70","doi-asserted-by":"crossref","unstructured":"Kedar S. Namjoshi and Robert P. Kurshan. Syntactic program transformations for automatic abstraction. In Emerson and Sistla [ES00], pages 435\u2013449.","DOI":"10.1007\/10722167_33"},{"key":"4_CR71","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-48236-9","volume-title":"Theoretical Computer Science","author":"F. Nielson","year":"1999","unstructured":"Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer, Berlin, 1999. Par81. D. Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer Science, number 104 in LNCS, pages 167\u2013183, Springer-Verlag, Berlin, 1981."},{"issue":"6","key":"4_CR72","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM Journal of Computation, 16(6):973\u2013989, 1987.","journal-title":"SIAM Journal of Computation"},{"key":"4_CR73","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-49059-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 99)","author":"V. Rusu","year":"1999","unstructured":"Vlad Rusu and Eli Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. In W. Rance Cleaveland, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 99), number 1579 in LNCS, pages 178\u2013192, Springer, Berlin, 1999."},{"key":"4_CR74","doi-asserted-by":"crossref","unstructured":"K. Stahl, K. Baukus, Y. Lakhnech, and M. Steffen. Divide, abstract, and model-check. In Dams et al. [DGLM99].","DOI":"10.1007\/3-540-48234-2_5"},{"key":"4_CR75","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Temporal Logic in Specification","author":"C. Stirling","year":"1989","unstructured":"Colin Stirling. Comparing linear and branching time temporal logics. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Temporal Logic in Specification, number 398 in LNCS, pages 1\u201320, Springer-Verlag, Berlin, 1989."},{"issue":"5","key":"4_CR76","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1093\/logcom\/4.5.811","volume":"4","author":"J. Benthem van","year":"1994","unstructured":"Johan van Benthem, Jan van Eijck, and Vera Stebletsova. Modal logic, transition systems and processes. Journal of Logic and Computation, 4(5):811\u2013855, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"4_CR77","unstructured":"R.J. van Glabbeek. Comparative Concurrency Semantics and Refinement of Actions. PhD thesis, Free University of Amsterdam\/Center for Math. and Comp. Sc., Amsterdam, 1990."},{"key":"4_CR78","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"590","DOI":"10.1007\/3-540-48119-2_33","volume-title":"FM\u201999-Formal Methods","author":"A. Wong","year":"1999","unstructured":"Andre Wong and Marsha Chechik. Formal modeling in a commercial setting: A case study. In FM\u201999-Formal Methods, number 1708 in LNCS, pages 590\u2013607, Springer, Berlin, 1999."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46017-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:11:37Z","timestamp":1739992297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46017-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434771","9783540460176"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/3-540-46017-9_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}