CaltechAUTHORS
  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. http://resolver.caltech.edu/CaltechAUTHORS:20140804-125108488

[img]
Preview
PDF - Accepted Version
See Usage Policy.

439Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechAUTHORS:20140804-125108488

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.


Item Type:Book Section
Related URLs:
URLURL TypeDescription
http://dl.acm.org/citation.cfm?id=2632375&CFID=397844841&CFTOKEN=93157315PublisherArticle
http://dx.doi.org/10.1145/2632362.2632375DOIArticle
http://spinroot.com/gerard/pdf/spin_2014.pdfOrganizationArticle
ORCID:
AuthorORCID
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.
Funders:
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:http://resolver.caltech.edu/CaltechAUTHORS:20140804-125108488
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
Collection:CaltechAUTHORS
Deposited By: Ruth Sustaita
Deposited On:04 Aug 2014 20:33
Last Modified:13 May 2015 18:44

Repository Staff Only: item control page