{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:50:15Z","timestamp":1778914215504,"version":"3.51.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2004,7,6]],"date-time":"2004-07-06T00:00:00Z","timestamp":1089072000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2004,8]]},"DOI":"10.1007\/s10009-004-0149-6","type":"journal-article","created":{"date-parts":[[2004,7,5]],"date-time":"2004-07-05T07:35:07Z","timestamp":1089012907000},"page":"320-341","source":"Crossref","is-referenced-by-count":30,"title":["Exploiting transition locality in automatic verification of finite-state concurrent systems"],"prefix":"10.1007","volume":"6","author":[{"given":"Giuseppe","family":"Della Penna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benedetto","family":"Intrigila","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marisa","family":"Venturini Zilli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,7,6]]},"reference":[{"key":"149_CR1","unstructured":"A user guide to hytech: http:\/\/www.eecs.berkeley.edu\/\u223ctah\/HyTech"},{"key":"149_CR2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/32.489079","volume":"22","author":"Alur","year":"1996","unstructured":"Alur R, Henzinger TA, Ho PH (1996) Automatic symbolic verification of embedded systems. IEEE Trans Softw Eng 22:2\u201311","journal-title":"IEEE Trans Softw Eng"},{"key":"149_CR3","doi-asserted-by":"crossref","unstructured":"Bryant R (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C-35(8):677\u2013691","DOI":"10.1109\/TC.1986.1676819"},{"key":"149_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"key":"149_CR5","unstructured":"Cached murphi Web page: http:\/\/www.dsi.uniroma1.it\/\u223ctronci\/cached.murphi.html"},{"key":"149_CR6","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1016\/0041-5553(68)90115-8","volume":"8","author":"Chernikova","year":"1968","unstructured":"Chernikova NV (1968) Algorithm for discovering the set of all solutions of a linear programming problem. USSR Comput Math Math Phys 8(6):282\u2013293","journal-title":"USSR Comput Math Math Phys"},{"key":"149_CR7","doi-asserted-by":"crossref","unstructured":"Dill DL, Drexler AJ, Hu AJ, Yang CH (1992) Protocol verification as a hardware design aid. In: Proceedings of the IEEE international conference on computer design: VLSI in computers and processors, pp 522\u2013525","DOI":"10.1109\/ICCD.1992.276232"},{"key":"149_CR8","unstructured":"Godefroid P, Holzmann GJ, Pirottin D (1992) State space caching revisited. In: Bochmann GV, Probst D (eds) Proceedings of the 4th international workshop on computer aided verification (CAV), Montreal. Lecture notes in computer science, vol 663. Springer, Berlin Heidelberg New York, pp 178\u2013191"},{"key":"149_CR9","doi-asserted-by":"crossref","unstructured":"Halbwachs N (1993) Delay analysis in synchronous programs. In: Courcoubetis C (ed) Proceedings of Computer Aided Verification (CAV). Lecture notes in computer science, vol 697. Springer, Berlin Heidelberg New York, pp 333\u2013346","DOI":"10.1007\/3-540-56922-7_28"},{"key":"149_CR10","doi-asserted-by":"crossref","unstructured":"Halbwachs N, Raymond P, Proy Y-E (1994) Verification of linear hybrid systems by means of convex approximation. In: LeCharlier B (ed) Proceedings of the symposium on static analysis (SAS). Lecture notes in computer science, vol 864. Springer, Berlin Heidelberg New York, pp 223\u2013237","DOI":"10.1007\/3-540-58485-4_43"},{"key":"149_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Ho P-H, Wong-Toi H (1995) Hytech: the next generation. In: Proceedings of the 16th annual IEEE real-time systems symposium (RTSS). IEEE, New York, pp 56\u201365","DOI":"10.1109\/REAL.1995.495196"},{"key":"149_CR12","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"Henzinger","year":"1997","unstructured":"Henzinger TA, Ho P-H, Wong-Toi H (1997) Hytech: a model checker for hybrid systems. Int J Softw Tools Technol Transfer 1:110\u2013122","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"149_CR13","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (1985) Tracing protocols. AT&T Tech J 64(10):2413\u20132433","DOI":"10.1002\/j.1538-7305.1985.tb00010.x"},{"key":"149_CR14","doi-asserted-by":"crossref","first-page":"683","DOI":"10.1109\/TSE.1987.233206","volume":"13","author":"Holzmann","year":"1987","unstructured":"Holzmann GJ (1987) Automated protocol validation in argos, assertion proving and scatter searching. IEEE Trans Softw Eng 13(6):683\u2013697","journal-title":"IEEE Trans Softw Eng"},{"key":"149_CR15","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The spin model checker. IEEE Trans Softw Eng 23(5):279\u2013295","journal-title":"IEEE Trans Softw Eng"},{"key":"149_CR16","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1023\/A:1008696026254","volume":"13","author":"Holzmann","year":"1998","unstructured":"Holzmann GJ (1998) An analysis of bitstate hashing. Formal Methods Sys Des 13(3):289\u2013307","journal-title":"Formal Methods Sys Des"},{"key":"149_CR17","doi-asserted-by":"crossref","unstructured":"Holzmann GJ, Peled D (1995) An improvement in formal verification. In: Proceedings of the FORTE conference, Proceedings of IFIP. Chapman & Hall, London, 6:197\u2013211","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"149_CR18","doi-asserted-by":"crossref","unstructured":"Hu AJ, York G, Dill DL (1994) New techniques for efficient verification with implicitily conjoined bdds. In: Proceedings of the 31st IEEE conference on design automation, pp 276\u2013282","DOI":"10.1145\/196244.196377"},{"key":"149_CR19","unstructured":"Ip CN, Dill DL (1993) Better verification through symmetry. In: Agnew D, Claesen L, Camposano R (eds) Proceedings of the 11th international conference on: computer hardware description languages and their applications. Elsevier, Amsterdam, pp 97\u2013111"},{"key":"149_CR20","doi-asserted-by":"crossref","unstructured":"Ip CN, Dill DL (1993) Efficient verification of symmetric concurrent systems. In: Proceedings of the IEEE international conference on computer design: VLSI in computers and processors, pp 230\u2013234","DOI":"10.1109\/ICCD.1993.393375"},{"key":"149_CR21","doi-asserted-by":"crossref","unstructured":"Larsen KG, Pettersson P, Yi W (1997) Uppaal: Status and developments. In: Grumberg O (ed) Proceedings of CAV97, June 1997. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 456\u2013459","DOI":"10.1007\/3-540-63166-6_47"},{"key":"149_CR22","doi-asserted-by":"crossref","unstructured":"Liaw H-T, Lin C-S (1992) On the obdd-representation of general boolean functions. IEEE Trans Comput C-41(6):661\u2013664","DOI":"10.1109\/12.144618"},{"key":"149_CR23","unstructured":"Murphi Web page: http:\/\/sprout.stanford.edu\/dill\/murphi.html"},{"key":"149_CR24","unstructured":"Papoulis A (1965) Probability, random variables and stochastic processes. McGraw-Hill Series in System Sciences"},{"key":"149_CR25","first-page":"a","volume":"architecture","author":"Patterson","year":"1996","unstructured":"Patterson DA, Hennessy JL (1996) Computer architecture: a quantitative approach. Morgan Kaufmann, San Francisco","journal-title":"Computer"},{"key":"149_CR26","unstructured":"Della Penna G, Intrigila B, Melatti I, Minichino M, Ciancamerla E, Parisse A, Tronci E, Zilli MV (2003) Automatic verification of a turbogas control system with the mur\u03d5 verifier. In: Pnueli A, Maler O (eds) Proceedings of the 6th international workshop Hybrid Systems: Computation and Control (HSCC), Prague, Czech Republic, April 2003. Lecture notes in computer science, vol 2623. Springer, Berlin Heidelberg New York, pp 141\u2013155"},{"key":"149_CR27","doi-asserted-by":"crossref","unstructured":"Della Penna G, Intrigila B, Tronci E, Venturini Zilli M (2002) Exploiting transition locality in the disk based mur\u03d5 verifier. In: Aagaard MD, O\u2019Leary JW (eds) Proceedings of the 4th international conference on formal methods in computer aided design (FMCAD), Portland, OR, November 2002. Lecture notes in computer science, vol 2517. Springer, Berlin Heidelberg New York, pp 202\u2013219","DOI":"10.1007\/3-540-36126-X_13"},{"key":"149_CR28","first-page":"270","volume":"2","author":"Puri","year":"2000","unstructured":"Puri A, Holzmann GJ (2000) A minimized automaton representation of reachable states. Int J Softw Tools Technol Transfer 2(3):270\u2013278","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"149_CR29","doi-asserted-by":"crossref","unstructured":"Ranjan RK, Sanghavi JV, Brayton RK, Sangiovanni-Vincentelli A (1996) Binary decision diagrams on network of workstations. In: Proceedings of the IEEE international conference on computer design, pp 358\u2013364","DOI":"10.1109\/ICCD.1996.563579"},{"key":"149_CR30","doi-asserted-by":"crossref","unstructured":"Sanghavi JV, Ranjan RK, Brayton RK, Sangiovanni-Vincentelli A (1996) High performance bdd package by exploiting memory hierarchy. In: Proceedings of the 33rd IEEE conference on design automation, pp 635\u2013640","DOI":"10.1109\/DAC.1996.545652"},{"key":"149_CR31","unstructured":"Smv Web page: http:\/\/www.cs.cmu.edu\/\u223cmodelcheck\/"},{"key":"149_CR32","unstructured":"Spin Web page: http:\/\/spinroot.com"},{"key":"149_CR33","doi-asserted-by":"crossref","unstructured":"Stern U, Dill D (1997) Parallelizing the mur\u03d5 verifier. In: Grumberg O (ed) Proceedings of the 9th international conference on computer aided verification, Haifa, Israel. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 256\u2013267","DOI":"10.1007\/3-540-63166-6_26"},{"key":"149_CR34","unstructured":"Stern U, Dill D (1998) Using magnetic disk instead of main memory in the mur\u03d5 verifier. In: Hu AJ, Vardi MY (eds) Proceedings of the 10th international conference on computer aided verification, Vancouver, BC, Canada. Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 172\u2013183"},{"key":"149_CR35","doi-asserted-by":"crossref","unstructured":"Stern U, Dill DL (1995) Improved probabilistic verification by hash compaction. In: Camurati P, Eveking H (eds) Proceedings of the IFIP WG 10.5 advanced research working conference on correct hardware design and verification methods (CHARME). Lecture notes in computer science, vol 987. Springer, Berlin Heidelberg New York, pp 206\u2013224","DOI":"10.1007\/3-540-60385-9_13"},{"key":"149_CR36","doi-asserted-by":"crossref","unstructured":"Stern U, Dill DL (1996) A new scheme for memory-efficient probabilistic verification. In: Gotzhein R, Bredereke J (eds) Proceedings of the IFIP TC6\/WG6.1 joint international conference on formal description techniques for distributed systems and communication protocols, and Protocol specification, testing, and verification, Proceedings of IFIP, vol 69. Kluwer, Dordrecht, pp 333\u2013348","DOI":"10.1007\/978-0-387-35079-0_21"},{"key":"149_CR37","unstructured":"Steven Ulrich web page: http:\/\/verify.stanford.edu\/uli\/research.html"},{"key":"149_CR38","doi-asserted-by":"crossref","unstructured":"Stornetta T, Brewer F (1996) Implementation of an efficient parallel bdd package. In: Proceedings of the 33rd annual conference on design automation. ACM Press, New York, pp 641\u2013644","DOI":"10.1109\/DAC.1996.545653"},{"key":"149_CR39","doi-asserted-by":"crossref","unstructured":"Tronci E, Della Penna G, Intrigila B, Venturini Zilli M (2001) Exploiting transition locality in automatic verification. In: Margaria T, Melham T (eds) Proceedings of the IFIP WG 10.5 advanced research working conference on correct hardware design and verification methods (CHARME), September 2001. Lecture notes in computer science, vol 2144. Springer, Berlin Heidelberg New York, pp 259\u2013274","DOI":"10.1007\/3-540-44798-9_22"},{"key":"149_CR40","unstructured":"Tronci E, Della Penna G, Intrigila B, Venturini Zilli M (2001) A probabilistic approach to space-time trading in automatic verification of concurrent systems. In: Proceedings of the 8th IEEE Asia-Pacific conference on software engineering (APSEC), Macau SAR, China, December 2001. IEEE Press, New York, pp 317\u2013324"},{"key":"149_CR41","unstructured":"Uppaal web page: http:\/\/www.docs.uu.se\/docs\/rtmv\/uppaal\/"},{"key":"149_CR42","doi-asserted-by":"crossref","unstructured":"Wolper P, Leroy D (1993) Reliable hashing without collision detection. In: Courcoubetis C (ed) Proceedings of the 5th international conference on computer aided verification, Elounda, Greece. Lecture notes in computer science, vol 697. Springer, Berlin Heidelberg New York, pp 59\u201370","DOI":"10.1007\/3-540-56922-7_6"},{"key":"149_CR43","unstructured":"German S, private communication"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0149-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0149-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0149-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:19Z","timestamp":1559100319000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0149-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,7,6]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["149"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0149-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,7,6]]}}}