A Caltech Library Service

An Improvement of the Piggyback Algorithm for Parallel Model Checking

Filippidis, Ioannis and Holzmann, Gerard J. (2014) An Improvement of the Piggyback Algorithm for Parallel Model Checking. In: SPIN 2014. ACM , New York, NY, pp. 48-57. ISBN 978-1-4503-2452-6.

PDF - Accepted Version
See Usage Policy.


Use this Persistent URL to link to this item:


This paper extends the piggyback algorithm to enlarge the set of liveness properties it can verify. Its extension is motivated by an attempt to express in logic the counterexamples it can detect and relate them to bounded liveness. The original algorithm is based on parallel breadth-first search and piggybacking of accepting states that are deleted after counting a fixed number of transitions. The main improvement is obtained by renewing the counter of transitions when the same accepting states are visited in the negated property automaton. In addition, we describe piggybacking of multiple states in either sets (exact) or Bloom filters (lossy but conservative), and use of local searches that attempt to connect cycles fragmented among processing cores. Finally it is proved that accepting cycle detection is in NC in the size of the product automaton's entire state space, including unreachable states.

Item Type:Book Section
Related URLs:
URLURL TypeDescription
Filippidis, Ioannis0000-0003-4704-3334
Additional Information:© 2014 ACM, Inc. This work was partially supported by a Graduate Research Fellowship from the Jet Propulsion Laboratory, California Institute of Technology in 2013.
Funding AgencyGrant Number
JPL/Caltech Graduate Research FellowshipUNSPECIFIED
Subject Keywords:Piggyback algorithm, breadth-first search, linear temporal logic, SPIN
Record Number:CaltechAUTHORS:20140804-125108488
Persistent URL:
Official Citation:An improvement of the piggyback algorithm for parallel model checking Ioannis Filippidis, Gerard J. Holzmann Pages: 48-57 doi>10.1145/2632362.2632375
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:47907
Deposited By: Ruth Sustaita
Deposited On:04 Aug 2014 20:33
Last Modified:03 Oct 2019 06:58

Repository Staff Only: item control page