{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T10:47:11Z","timestamp":1772794031533,"version":"3.50.1"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2012,7,3]],"date-time":"2012-07-03T00:00:00Z","timestamp":1341273600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s00236-012-0161-3","type":"journal-article","created":{"date-parts":[[2012,7,2]],"date-time":"2012-07-02T10:32:43Z","timestamp":1341225163000},"page":"313-341","source":"Crossref","is-referenced-by-count":31,"title":["Abstract reduction in directed model checking CCS processes"],"prefix":"10.1007","volume":"49","author":[{"given":"Antonella","family":"Santone","sequence":"first","affiliation":[]},{"given":"Gigliola","family":"Vaglini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,7,3]]},"reference":[{"key":"161_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Wang, B.-Y.: \u201cNext\u201d heuristic for on-the-fly model checking. In: Proceedings of the 10th International Conference on Concurrency Theory (CONCUR\u201999). Lecture Notes in Computer Science, vol. 1664, pp. 98\u2013113 (1999)","DOI":"10.1007\/3-540-48320-9_9"},{"issue":"1","key":"161_CR2","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1093\/comjnl\/44.1.21","volume":"44","author":"G. Anastasi","year":"2001","unstructured":"Anastasi G., Bartoli A., De Francesco N.: Efficient verification of a multicast protocol for mobile computing. Comput. J. 44(1), 21\u201330 (2001)","journal-title":"Comput. J."},{"key":"161_CR3","doi-asserted-by":"crossref","unstructured":"Anastasi, G., Spadoni, F., Bartoli, A.: Group multicast in distributed mobile systems with unreliable wireless network. In: Proceedings of the 18th IEEE Symposium on Reliable Distributed Systems (SRDS\u201999), IEEE Computer Society, vol. 14, pp. 14\u201323 (1999)","DOI":"10.1109\/RELDIS.1999.805079"},{"key":"161_CR4","doi-asserted-by":"crossref","unstructured":"Arnold, A., Begay, D., Crubille, P.: Construction and Analysis of Transition Systems with MEC (Chapter 6). World Scientific, Singapore (1994)","DOI":"10.1142\/2505"},{"key":"161_CR5","doi-asserted-by":"crossref","unstructured":"Barbuti, R., De Francesco, N., Santone, A., Vaglini, G.: Selective mu-calculus: new modal operators for proving properties on reduced transition systems. In: Proceedings of FORTE X\/PSTV XVII\u201997, pp. 519\u2013534. Chapman & Hall, London (1997)","DOI":"10.1007\/978-0-387-35271-8_32"},{"issue":"3","key":"161_CR6","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1006\/jcss.1999.1660","volume":"59","author":"R. Barbuti","year":"1999","unstructured":"Barbuti R., De Francesco N., Santone A., Vaglini G.: Selective mu-calculus and formula-based equivalence of transition systems. J. Comput. Syst. Sci. 59(3), 537\u2013556 (1999)","journal-title":"J. Comput. Syst. Sci."},{"key":"161_CR7","unstructured":"Bertoli, P., Cimatti, A., Slaney, J., Thiebaux, S.: Solving power supply restoration problems with planning via symbolic model-checking. In: Proceedings of the Sixth International Conference on AI Planning and Scheduling (AIPS\u201902), AAAI Press, pp. 23\u201329 (2002)"},{"key":"161_CR8","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Proceedings of the 11th International Conference on Computer-Aided Verification (CAV\u201999). Lecture Notes in Computer Science, vol. 1633, pp. 222\u2013235 (1999)","DOI":"10.1007\/3-540-48683-6_21"},{"issue":"1","key":"161_CR9","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s10009-008-0093-y","volume":"11","author":"D. Bosnacki","year":"2009","unstructured":"Bosnacki D., Leue S., Lluch-Lafuente A.: Partial-order reduction for general state exploring algorithms. Int. J. Softw. Tools Technol. Transf. 11(1), 39\u201351 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"8","key":"161_CR10","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"161_CR11","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke E.M., Emerson E.A., Sistla A.P.: Automatic verification of finite-state concurrent systems using temporal logic verification. ACM Trans. Program. Lang. Syst. 8, 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"5","key":"161_CR12","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke E.M., Grumberg O., Long D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"161_CR13","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke E.M., Grumberg O., Peled D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"161_CR14","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Proceedings of the Eighth International Conference on Computer-Aided Verification (CAV\u201996). Lecture Notes in Computer Science, vol. 1102, pp. 394\u2013397 (1996)","DOI":"10.1007\/3-540-61474-5_87"},{"key":"161_CR15","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Proceedings of the 8th International SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science, vol. 2057, pp. 57\u201379 (2001)","DOI":"10.1007\/3-540-45139-0_5"},{"key":"161_CR16","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Trail-directed model checking. In: Proceedings of Computer Aided Verification (CAV) Workshops. Electronic Notes in Theoretical Computer Science, vol. 55 (2001)","DOI":"10.1016\/S1571-0661(04)00261-0"},{"key":"161_CR17","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp S., Lluch-Lafuente A., Leue S.: Directed explicit-state model checking in the validation of communication protocols. Int. J. Softw. Tools Technol. Transf. 5, 246\u2013267 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"161_CR18","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Reffel, F.: OBDDs in heuristic search. In: Proceedings of the 22nd Annual German Conference on Artificial Intelligence (KI\u201998). Lecture Notes in Computer Science, vol. 1504, pp. 81\u201392 (1998)","DOI":"10.1007\/BFb0095430"},{"key":"161_CR19","unstructured":"Edelkamp, S.: Symbolic pattern databases in heuristic search planning. In: Proceedings of the Sixth International Conference on AI Planning and Scheduling (AIPS\u201902), AAAI Press (2002)"},{"key":"161_CR20","unstructured":"Edelkamp, S., Lluch-Lafuente, A.: Abstraction databases in theory and model checking practice. In: ICAPS Workshop on Connecting Planning (2004)"},{"key":"161_CR21","unstructured":"Feng, Z., Hansen, E.: Symbolic heuristic search for factored Markov decision processes. In: Proceedings of the Eighteenth National Conference on Artificial Intelligence (AAAI\u201902), AAAI Press, pp. 455\u2013460 (2002)"},{"key":"161_CR22","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032 (1996)","DOI":"10.1007\/3-540-60761-7"},{"issue":"8","key":"161_CR23","doi-asserted-by":"crossref","first-page":"1397","DOI":"10.1016\/j.jcss.2006.03.003","volume":"72","author":"S. Gradara","year":"2006","unstructured":"Gradara S., Santone A., Villani M.L.: DELFIN+: an efficient deadlock detection tool for CCS processes. J. Comput. Syst. Sci. 72(8), 1397\u20131412 (2006)","journal-title":"J. Comput. Syst. Sci."},{"key":"161_CR24","doi-asserted-by":"crossref","unstructured":"Gradara, S., Santone, A., Villani, M.L.: Formal verification of concurrent systems via directed model checking. In: Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006). Electronic Notes in Theoretical Computer Science, vol. 185, pp. 93\u2013105 (2007)","DOI":"10.1016\/j.entcs.2007.05.031"},{"key":"161_CR25","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Proceedings of Computer Aided Verification (CAV), 1997. Lecture Notes in Computer Science, vol. 1254, pp. 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"161_CR26","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: Heuristic model checking for Java programs. In: Proceedings of the 9th International SPIN Workshop (SPIN\u201902). Lecture Notes in Computer Science, vol. 2318, pp. 242\u2013245 (2002)","DOI":"10.1007\/3-540-46017-9_21"},{"key":"161_CR27","doi-asserted-by":"crossref","unstructured":"Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. In: Proceedings of Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, vol. 1101, pp. 536\u2013550. Springer (1996)","DOI":"10.1007\/BFb0014338"},{"key":"161_CR28","doi-asserted-by":"crossref","unstructured":"Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Industrial Benefit and Advances in Formal Methods (FME\u201996), pp. 662\u2013681. Springer, Berlin (1996)","DOI":"10.1007\/3-540-60973-3_113"},{"key":"161_CR29","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"161_CR30","doi-asserted-by":"crossref","unstructured":"Jard, C., J\u00e9ron, T.: Bounded-memory algorithms for verification on-the-fly. In: Proceedings of the Third International Conference on Computer-Aided Verification (CAV\u201991). Lecture Notes in Computer Science, vol. 575, pp. 192\u2013201 (1991)","DOI":"10.1007\/3-540-55179-4_19"},{"key":"161_CR31","unstructured":"Jensen, R.M., Bryant, R.E., Veloso, M.M.: SetA*: an efficient bdd-based heuristic search algorithm. In: Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence (AAAI\/IAAI\u201902), AAAI Press, pp. 668\u2013673 (2002)"},{"key":"161_CR32","doi-asserted-by":"crossref","unstructured":"Kupferschmid, S., Wehrle, M.: Abstractions and pattern databases: the quest for succinctness and accuracy. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011). Lecture Notes in Computer Science, vol. 6605, pp. 276\u2013290 (2011)","DOI":"10.1007\/978-3-642-19835-9_26"},{"key":"161_CR33","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1995","unstructured":"Kurshan R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1995)"},{"key":"161_CR34","doi-asserted-by":"crossref","unstructured":"Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. ACM, pp. 126\u2013135 (1988)","DOI":"10.1145\/55483.55496"},{"key":"161_CR35","unstructured":"Lluch-Lafuente, A.: Symmetry reduction and heuristic search for error detection in model checking. In: Proceedings of Workshop of Model Checking and Artificial Intelligence (MoChArt-03) (2003)"},{"key":"161_CR36","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan K.: Symbolic Model Checking. Kluwer, Boston (1993)"},{"key":"161_CR37","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"161_CR38","doi-asserted-by":"crossref","unstructured":"Moller, M.O., Alur, R.: Heuristics for hierarchical partitioning with application to model checking. In: Proceedings of the 11th IFIP WG 10.5, Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201901). Lecture Notes in Computer Science, vol. 2144, pp. 71\u201385 (2001)","DOI":"10.1007\/3-540-44798-9_5"},{"key":"161_CR39","doi-asserted-by":"crossref","unstructured":"Parrow, J.: An introduction to the pi-calculus. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 479\u2013543. Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044482830-9\/50026-6"},{"key":"161_CR40","volume-title":"Heuristics: Intelligent Search Strategies for Computer Problem Solving","author":"J. Pearl","year":"1984","unstructured":"Pearl J.: Heuristics: Intelligent Search Strategies for Computer Problem Solving. Addison-Wesley, Reading (1984)"},{"key":"161_CR41","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all, on model-checking using representatives. In: Proceedings of the Fifth International Conference on Computer-Aided Verification (CAV\u201993). Lecture Notes in Computer Science, vol. 679, pp. 409\u2013423 (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"issue":"6","key":"161_CR42","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1109\/TSE.2003.1205179","volume":"29","author":"A. Santone","year":"2003","unstructured":"Santone A.: Heuristic search + local model checking in selective mu-calculus. IEEE Trans. Softw. Eng. 29(6), 510\u2013523 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1\u20132","key":"161_CR43","first-page":"111","volume":"70","author":"K.S. Seppi","year":"2006","unstructured":"Seppi K.S., Jones M., Lamborn P.: Guided Model Checking with a Bayesian Meta-heuristic. Fundam. Inform. 70(1\u20132), 111\u2013126 (2006)","journal-title":"Fundam. Inform."},{"key":"161_CR44","doi-asserted-by":"crossref","unstructured":"Stirling, C.: An Introduction to Modal and Temporal Logics for CCS. In: Concurrency: Theory, Language, and Architecture. Lecture Notes in Computer Science, vol. 391 (1989)","DOI":"10.1007\/BFb0013039"},{"key":"161_CR45","doi-asserted-by":"crossref","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, 161\u2013177 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"161_CR46","doi-asserted-by":"crossref","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Proceedings of the Second International Conference on Computer-Aided Verification (CAV\u201990). Lecture Notes in Computer Science, vol. 531, pp. 156\u2013165 (1990)","DOI":"10.1007\/BFb0023729"},{"key":"161_CR47","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: IEEE International Conference on Automated Software Engineering (ASE) (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"161_CR48","doi-asserted-by":"crossref","unstructured":"Wehrle, M., Kupferschmid, S.: Context-enhanced directed model checking. In: Proceedings of 17th International Workshop (SPIN10). Lecture Notes in Computer Science, vol. 6349, pp. 88\u2013105 (2010)","DOI":"10.1007\/978-3-642-16164-3_7"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-012-0161-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-012-0161-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-012-0161-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T01:57:52Z","timestamp":1743645472000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-012-0161-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,3]]},"references-count":48,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["161"],"URL":"https:\/\/doi.org\/10.1007\/s00236-012-0161-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,3]]}}}