Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published July 21, 2014 | Accepted Version
Book Section - Chapter Open

An Improvement of the Piggyback Algorithm for Parallel Model Checking

Abstract

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.

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.

Attached Files

Accepted Version - spin_2014.pdf

Files

spin_2014.pdf
Files (450.5 kB)
Name Size Download all
md5:7852e4faf671de366fd18f4b8be70b7e
450.5 kB Preview Download

Additional details

Created:
August 20, 2023
Modified:
October 26, 2023