Title: Exploiting Transition Locality in the Disk Based Mur$\varphi$ Verifier Authors: Giuseppe Della Penna Dip. di Informatica, Universit\`a di L'Aquila, Coppito 67100, L'Aquila, Italy dellapenna@di.univaq.it, Benedetto Intrigila Dip. di Informatica, Universit\`a di L'Aquila, Coppito 67100, L'Aquila, Italy intrigila@di.univaq.it, Enrico Tronci Dip. di Informatica Universit\`a di Roma ``La Sapienza'', Via Salaria 113, 00198 Roma, Italy tronci@dsi.uniroma1.it, Marisa Venturini Zilli Dip. di Informatica Universit\`a di Roma ``La Sapienza'', Via Salaria 113, 00198 Roma, Italy zilli@dsi.uniroma1.it Proceedings of: 4th International Conference on ``Formal Methods in Computer Aided Verification'' (FMCAD), 6-8 November 2002, Portland, Oregon, USA, Springer-Verlag Abstract The main obstruction to automatic verification of {\em Finite State Systems} is the huge amount of memory required to complete the verification task ({\em state explosion}). This motivates research on distributed as well as disk based verification algorithms. In this paper we present a disk based Breadth First {\em Explicit State Space Exploration} algorithm as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm exploits {\em transition locality} (i.e. the statistical fact that most transitions lead to unvisited states or to recently visited states) to decrease disk read accesses thus reducing the time overhead due to disk usage. A disk based verification algorithm for Mur$\varphi$ has been already proposed in the literature. To measure the time speed up due to locality exploitation we compared our algorithm with such previously proposed algorithm. Our experimental results show that our disk based verification algorithm is typically more than 10 times faster than such previously proposed disk based verification algorithm. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the (standard) Mur$\varphi$ verifier with enough memory to complete the verification task. Our experimental results show that even when using $1/10$ of the RAM needed to complete verification, our disk based algorithm is only between 1.4 and 5.3 times (3 times on average) slower than (RAM) Mur$\varphi$ with enough RAM memory to complete the verification task at hand. Using our disk based Mur$\varphi$ we were able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 gigabytes of RAM using RAM based Mur$\varphi$.