Skip to main content
SpringerLink
Log in
Book cover

Handbook of Parallel Constraint Reasoning pp 457–507Cite as

Parallel Model Checking Algorithms for Linear-Time Temporal Logic

  • Chapter
  • First Online:

Abstract

Model checking is a fully automated, formal method for demonstrating absence of bugs in reactive systems. Here, bugs are violations of properties in Linear-time Temporal Logic (LTL). A fundamental challenge to its application is the exponential explosion in the number of system states. The current chapter discusses the use of parallelism in order to overcome this challenge. We reiterate the textbook automata-theoretic approach, which reduces the model checking problem to the graph problem of finding cycles. We discuss several parallel algorithms that attack this problem in various ways, each with different characteristics: Depth-first search (DFS) based algorithms rely on heuristics for good parallelization, but exhibit a low complexity and good on-the-fly behavior. Breadth-first search (BFS) based approaches, on the other hand, offer good parallel scalability and support distributed parallelism. In addition, we present various simpler model checking tasks, which still solve a large and important subset of the LTL model checking problem, and show how these can be exploited to yield more efficient algorithms. In particular, we provide simplified DFS-based search algorithms and show that the BFS-based algorithms exhibit optimal runtimes in certain cases.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   89.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas. Optimal dynamic partial order reduction. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, pages 373–384, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2544-8. https://doi.org/10.1145/2535838.2535845.

  2. V. Agarwal, F. Petrini, D. Pasetto, and D. A. Bader. Scalable Graph Exploration on Multicore Processors. In Proceedings of the 2010 ACM/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis, SC ’10, pages 1–11, Washington, DC, USA, 2010. IEEE Computer Society. ISBN 978-1-4244-7559-9. https://doi.org/10.1109/sc.2010.46.

  3. A. Aggarwal, R. J. Anderson, and M. Kao. Parallel depth-first search in general directed graphs. SIAM J. Comput., 19(2):397–409, 1990. https://doi.org/10.1137/0219025.

  4. R. Alur, S. Chaudhuri, K. Etessami, and P. Madhusudan. On-the-fly reachability and cycle detection for recursive state machines. In N. Halbwachs and L. Zuck, editors, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’05), volume 3440 of Lecture Notes in Computer Science, pages 61–76. Springer Berlin Heidelberg, April 2005.

    Google Scholar 

  5. R. Anderson and H. Woll. Wait-free Parallel Algorithms for the Union-find Problem. In Proceedings of the Twenty-third Annual ACM Symposium on Theory of Computing, STOC ’91, pages 370–380, New York, NY, USA, 1991. ACM. ISBN 0-89791-397-3. https://doi.org/10.1145/103418.103458.

  6. T. Babiak, M. Křetínský, V. Řehák, and J. Strejček. LTL to Büchi automata translation: Fast and more deterministic. In Proc. of the 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), volume 7214 of LNCS, pages 95–109. Springer, 2012.

    Google Scholar 

  7. T. Babiak, T. Badie, A. Duret-Lutz, M. Křetínský, and J. Strejček. Compositional approach to suspension and other improvements to LTL translation. In Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN’13), volume 7976 of Lecture Notes in Computer Science, pages 81–98. Springer, July 2013. https://doi.org/10.1007/978-3-642-39176-7_6.

  8. C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.

    Google Scholar 

  9. T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with SLAM. Commun. ACM, 54(7):68–76, 2011. https://doi.org/10.1145/1965724.1965743.

  10. J. Barnat, L. Brim, and P. Rockai. DiVinE 2.0: High-performance model checking. In Proceedings of the International Workshop on High Performance Computational Systems Biology (HiBi’09), pages 31–32. IEEE Computer Society Press, 2009.

    Google Scholar 

  11. J. Barnat, L. Brim, and P. Ročkai. A time-optimal on-the-fly parallel algorithm for model checking of weak LTL properties. In Proceedings of the 11th International Conference on Formal Engineering Methods (ICFEM’09), volume 5885 of LNCS, pages 407–425, Berlin, Heidelberg, 2009. Springer-Verlag.

    Google Scholar 

  12. J. Barnat, L. Brim, and P. Ročkai. Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer, 12(2):139–153, 2010.

    Google Scholar 

  13. J. Barnat, P. Bauch, L. Brim, and M. Cežka. Computing strongly connected components in parallel on cuda. In 2011 IEEE International Parallel Distributed Processing Symposium, pages 544–555, May 2011. https://doi.org/10.1109/IPDPS.2011.59.

  14. J. Barnat, L. Brim, V. Havel, J. Havlícek, J. Kriho, M. Lenco, P. Rockai, V. Still, and J. Weiser. Divine 3.0 - an explicit-state model checker for multithreaded C & C++ programs. In N. Sharygina and H. Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 863–868. Springer, 2013. ISBN 978-3-642-39798-1. https://doi.org/10.1007/978-3-642-39799-8_60.

  15. S. Ben-David, C. Eisner, D. Geist, and Y. Wolfsthal. Model checking at IBM. Formal Methods in System Design, 22(2):101–108, 2003. https://doi.org/10.1023/a:1022905120346.

  16. A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using sat procedures instead of bdds. In Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, DAC ’99, pages 317–320, New York, NY, USA, 1999. ACM. ISBN 1-58113-109-7. https://doi.org/10.1145/309847.309942.

  17. V. Bloemen and J. van de Pol. Multi-core SCC-Based LTL Model Checking. In R. Bloem and E. Arbel, editors, Hardware and Software: Verification and Testing: 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016, Proceedings, pages 18–33, Cham, 2016. Springer International Publishing. ISBN 978-3-319-49052-6. https://doi.org/10.1007/978-3-319-49052-6_2.

  18. V. Bloemen, A. Laarman, and J. van de Pol. Multi-core On-the-fly SCC Decomposition. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’16, pages 8:1–8:12, New York, NY, USA, 2016. ACM. ISBN 978-1-4503-4092-2. https://doi.org/10.1145/2851141.2851161.

  19. R. D. Blumofe and C. E. Leiserson. Scheduling multithreaded computations by work stealing. Journal of the ACM (JACM), 46(5):720–748, 1999.

    Google Scholar 

  20. D. Bošnački. A nested depth first search algorithm for model checking with symmetry reduction. In D. A. Peled and M. Y. Vardi, editors, Formal Techniques for Networked and Distributed Sytems, volume 2529 of LNCS, pages 65–80. Springer Berlin Heidelberg, 2002. ISBN 978-3-540-00141-6. https://doi.org/10.1007/3-540-36135-9_5.

  21. L. Brim, I. Černá, P. Moravec, and J. Šimša. Accepting predecessors are better than back edges in distributed LTL model-checking. In A. J. Hu and A. K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD’04), volume 3312 of Lecture Notes in Computer Science, pages 352–366. Springer, November 2004.

    Google Scholar 

  22. L. Brim, I. Černá, P. Moravec, and J. Šimša. How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. In Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005), pages 1–12, Lisboa, Portugal, 2005. TU Munchen.

    Google Scholar 

  23. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677–691, Aug. 1986.

    Google Scholar 

  24. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1–33,Washington, D.C., 1990. IEEE Computer Society Press.

    Google Scholar 

  25. I. Černá and R. Pelánek. Relating hierarchy of temporal properties to model checking. In B. Rovan and P. Vojtáă, editors, Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS’03), volume 2747 of Lecture Notes in Computer Science, pages 318–327, Bratislava, Slovak Republic, Aug. 2003. Springer-Verlag.

    Google Scholar 

  26. I. Černá and R. Pelánek. Distributed explicit fair cycle detection (set based approach). In T. Ball and S. Rajamani, editors, Proceedings of the 10th International SPIN Workshop on Model Checking of Software (SPIN’03), volume 2648 of Lecture Notes in Computer Science, pages 49–73. Springer Berlin Heidelberg, May 2003.

    Google Scholar 

  27. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-Guided Abstraction Refinement, pages 154–169. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000. ISBN 978-3-540-45047-4. https://doi.org/10.1007/10722167_15.

  28. E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7–34, 2001.

    Google Scholar 

  29. E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla. Symmetry reductions in model checking, pages 147–158. Springer, 1998. ISBN 978-3-540-69339-0. https://doi.org/10.1007/bfb0028741.

  30. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 2000.

    Google Scholar 

  31. C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis. Memory-efficient algorithm for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.

    Google Scholar 

  32. J.-M. Couvreur. On-the-fly verification of temporal logic. In J. M. Wing, J. Woodcock, and J. Davies, editors, Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM’99), volume 1708 of Lecture Notes in Computer Science, pages 253–271, Toulouse, France, Sept. 1999. Springer-Verlag. ISBN 3-540-66587-0.

    Google Scholar 

  33. J.-M. Couvreur, A. Duret-Lutz, and D. Poitrenaud. On-the-fly emptiness checks for generalized Büchi automata. In P. Godefroid, editor, Proceedings of the 12th International SPIN Workshop on Model Checking of Software (SPIN’05), volume 3639 of Lecture Notes in Computer Science, pages 143–158. Springer, Aug. 2005.

    Google Scholar 

  34. A. Deshpande, F. Herbreteau, B. Srivathsan, T. Tran, and I. Walukiewicz. Fast detection of cycles in timed automata. http://arXiv.org/abs/1410.4509 2014.

  35. E. W. Dijkstra. EWD 376: Finding the maximum strong components in a directed graph. http://www.cs.utexas.edu/users/EWD/ewd03xx/EWD376.PDF, May 1973.

  36. A. Duret-Lutz. Manipulating LTL formulas using Spot 1.0. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13), volume 8172 of Lecture Notes in Computer Science, pages 442–445, Hanoi, Vietnam, Oct. 2013. Springer. https://doi.org/10.1007/978-3-319-02444-8_31.

  37. A. Duret-Lutz. LTL translation improvements in Spot 1.0. International Journal on Critical Computer-Based Systems, 5(1/2):31–54, Mar. 2014. https://doi.org/10.1504/ijccbs.2014.059594.

  38. A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu. Spot 2.0—a framework for LTL and w-automata manipulation. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16), volume 9938 of Lecture Notes in Computer Science, pages 122–129. Springer, 2016.

    Google Scholar 

  39. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Property specification patterns for finite-state verification. In M. Ardis, editor, Proceedings of the 2ndWorkshop on Formal Methods in Software Practice (FMSP’98), pages 7–15, New York, Mar. 1998. ACM Press.

    Google Scholar 

  40. S. Edelkamp, A. L. Lafuente, and S. Leue. Directed explicit model checking with HSF-SPIN. In Proceedings of the 8th international Spin workshop on model checking of software (SPIN’01), volume 2057 of Lecture Notes in Computer Science, pages 57–79. Springer-Verlag, 2001.

    Google Scholar 

  41. E. A. Emerson and T. Wahl. Dynamic Symmetry Reduction, pages 382–396. Springer, 2005. ISBN 978-3-540-31980-1. https://doi.org/10.1007/978-3-540-31980-1_25.

  42. S. Evangelista, L. Petrucci, and S. Youcef. Parallel nested depth-first searches for LTL model checking. In Proceedings of the 9th international conference on Automated technology for verification and analysis (ATVA’11), volume 6996 of Lecture Notes in Computer Science, pages 381–396. Springer-Verlag, 2011.

    Google Scholar 

  43. S. Evangelista, A. Laarman, L. Petrucci, and J. van de Pol. Improved multi-core nested depth-first search. In Proceedings of the 10th international conference on Automated technology for verification and analysis (ATVA’12), volume 7561 of Lecture Notes in Computer Science, pages 269–283. Springer-Verlag, 2012.

    Google Scholar 

  44. K. Fisler, R. Fraer, G. Kamhi, M. Y. Vardi, and Z. Yang. Is there a best symbolic cycle-detection algorithm? In Proceedings of the fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), volume 2031 of LNCS, pages 420–434. Springer-Verlag, 2001.

    Google Scholar 

  45. L. Fix. Fifteen years of formal property verification in Intel. In O. Grumberg and H. Veith, editors, 25 Years of Model Checking - History, Achievements, Perspectives, volume 5000 of Lecture Notes in Computer Science, pages 139–144. Springer, 2008. ISBN 978-3-540-69849-4. https://doi.org/10.1007/978-3-540-69850-0_8.

  46. L. K. Fleischer, B. Hendrickson, and A. Pınar. On Identifying Strongly Connected Components in Parallel, pages 505–511. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000. ISBN 978-3-540-45591-2. https://doi.org/10.1007/3-540-45591-4_68.

  47. H. N. Gabow. Path-based depth-first search for strong and biconnected components. Information Processing Letters, 74(3-4):107–114, February 2000.

    Google Scholar 

  48. A. Gaiser and S. Schwoon. Comparison of algorithms for checking emptiness on Büchi automata. In P. Hlinený, V. Matyás, and T. Vojnar, editors, Procedings of Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS’09), volume 13 of OASICS. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, Germany, Nov. 2009.

    Google Scholar 

  49. P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of the 13th International Conference on Computer Aided Verification (CAV’01), volume 2102 of Lecture Notes in Computer Science, pages 53–65, Paris, France, 2001. Springer-Verlag.

    Google Scholar 

  50. P. Gastin, P. Moro, and M. Zeitoun. Minimization of counterexamples in SPIN. In S. Graf and L. Mounier, editors, Proceedings of the 11th International SPIN Workshop on Model Checking of Software (SPIN’04), volume 2989 of Lecture Notes in Computer Science, pages 92–108, Apr. 2004.

    Google Scholar 

  51. H. Gazit and G. L. Miller. An improved parallel algorithm that computes the BFS numbering of a directed graph. Inf. Process. Lett., 28(2):61–65, 1988. https://doi.org/10.1016/0020-0190(88)90164-0.

  52. J. Geldenhuys and A. Valmari. More efficient on-the-fly LTL verification with Tarjan’s algorithm. Theoretical Computer Science, 345(1):60–82, Nov. 2005. Conference paper selected for journal publication.

    Google Scholar 

  53. D. Giannakopoulou and F. Lerda. From states to transitions: Improving translation of LTL formulæ to Büchi automata. In D. Peled and M. Vardi, editors, Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE’02), volume 2529 of Lecture Notes in Computer Science, pages 308–326, Houston, Texas, Nov. 2002. Springer-Verlag.

    Google Scholar 

  54. P. Godefroid. Using partial orders to improve automatic verification methods. In Computer-Aided Verification, pages 176–185. Springer, 1991.

    Google Scholar 

  55. P. Godefroid, G. Holzmann, and D. Pirottin. State-space caching revisited. Formal Methods in System Design, 7(3):227–241, Nov. 1995.

    Google Scholar 

  56. R. Greenlaw, H. J. Hoover, and W. L. Ruzzo. Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, 1995.

    Google Scholar 

  57. X. He and Y. Yesha. A nearly optimal parallel algorithm for constructing depth first spanning trees in planar graphs. SIAM J. Comput., 17(3):486–491, 1988. https://doi.org/10.1137/0217028.

  58. G. Holzmann. Parallelizing the spin model checker. In A. Donaldson and D. Parker, editors, SPIN’12, volume 7385 of LNCS, pages 155–171. Springer, 2012. ISBN 978-3-642-31758-3. http://dx.doi.org/10.1007/978-3-642-31759-0_12.

  59. G. J. Holzmann, D. A. Peled, and M. Yannakakis. On nested depth first search. In J.-C. Grégoire, G. J. Holzmann, and D. A. Peled, editors, Proceedings of the 2nd Spin Workshop, volume 32 of DIMACS: Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, May 1996.

    Google Scholar 

  60. S. Hong, N. C. Rodia, and K. Olukotun. On fast parallel detection of strongly connected components (scc) in small-world graphs. In 2013 SC - International Conference for High Performance Computing, Networking, Storage and Analysis (SC), pages 1–11, Nov 2013. https://doi.org/10.1145/2503210.2503246.

  61. T. Junttila. On the Symmetry Reduction Method for Petri Nets and Similar Formalisms. PhD thesis, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2003.

    Google Scholar 

  62. G. Kant, A. Laarman, J. Meijer, J. Pol, S. Blom, and T. Dijk. LTSmin: Highperformance language-independent model checking. In C. T. Christel Baier, editor, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15), volume 9035 of Lecture Notes in Computer Science, pages 692–707. Springer-Berlin, 2015.

    Google Scholar 

  63. S. Katz and D. Peled. An efficient verification method for parallel and distributed programs, pages 489–507. Springer, 1989. ISBN 978-3-540-46147-0. https://doi.org/10.1007/bfb0013032.

  64. A. Laarman. Scalable multi-core model checking. PhD thesis, University of Twente, 2014.

    Google Scholar 

  65. A. Laarman and J. van de Pol. Variations on multi-core nested depth-first search. In PDMC’11, pages 13–28, 2011.

    Google Scholar 

  66. A. Laarman, R. Langerak, J. van de Pol, M. Weber, and A. Wijs. Multi-core nested depth-first search. In T. Bultan and P.-A. Hsiung, editors, Proceedings of the Automated Technology for Verification and Analysis, 9th International Symposium (ATVA’11), volume 6996 of Lecture Notes in Computer Science, pages 321–335, Taipei, Taiwan, October 2011. Springer.

    Google Scholar 

  67. A. Laarman, J. van de Pol, and M. Weber. Multi-core LTSmin: Marrying modularity and scalability. In M. Bobaru, K. Havelund, G. Holzmann, and R. Joshi, editors, NFM 2011, Pasadena, CA, USA, volume 6617 of LNCS, pages 506–511, Berlin, July 2011. Springer. https://doi.org/10.1007/978-3-642-20398-5\_40.

  68. A. Laarman, J. van de Pol, and M.Weber. Parallel Recursive State Compression for Free. In A. Groce and M. Musuvathi, editors, SPIN 2011, LNCS, pages 38–56, London, July 2011. Springer. http://doc.utwente.nl/77024/.

  69. A. W. Laarman and D. Faragó. Improved on-the-fly livelock detection. In G. Brat, N. Rungta, and A. Venet, editors, NFM 2013, volume 7871 of LNCS, pages 32–47. Springer, 2013. ISBN 978-3-642-38087-7. https://doi.org/10.1007/978-3-642-38088-4_3.

  70. A. W. Laarman and A. J. Wijs. Partial-Order Reduction for Multi-core LTL Model Checking. In E. Yahav, editor, HVC 2014, volume 8855 of LNCS, pages 267–283. Springer, 2014. ISBN 978-3-319-13337-9. https://doi.org/10.1007/978-3-319-13338-6_20.

  71. A. W. Laarman, J. C. van de Pol, and M. Weber. Boosting Multi-Core Reachability Performance with Shared Hash Tables. In N. Sharygina and R. Bloem, editors, FMCAD 2010. IEEE Computer Society, 2010. http://dl.acm.org/citation.cfm?id=1998496.1998541.

  72. T. Lai and S. Sahni. Anomalies in parallel branch-and-bound algorithms. Commun. ACM, 27(6):594–602, 1984. https://doi.org/10.1145/358080.358103.

  73. A. Lenharth, D. Nguyen, and K. Pingali. Parallel graph analytics. Commun. ACM, 59(5):78–87, Apr. 2016. ISSN 0001-0782. https://doi.org/10.1145/2901919.

  74. G. Lowe. Concurrent depth-first search algorithms based on Tarjan’s Algorithm. International Journal on Software Tools for Technology Transfer, pages 1–19, 2015. ISSN 1433-2779. https://doi.org/10.1007/s10009-015-0382-1.

  75. A. Lumsdaine, D. Gregor, B. Hendrickson, and J. Berry. Challenges in parallel graph processing. Parallel Processing Letters, 17(1):5–20, 2007. https://doi.org/10.1142/s0129626407002843.

  76. Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proceedings of the sixth annual ACM Symposium on Principles of distributed computing (PODC’90), pages 377–410, New York, NY, USA, 1990. ACM.

    Google Scholar 

  77. K. L. McMillan. Symbolic Model Checking, pages 25–60. Springer US, Boston, MA, 1993. ISBN 978-1-4615-3190-6. https://doi.org/10.1007/978-1-4615-3190-6_3.

  78. K. L. McMillan. Interpolation and SAT-Based Model Checking, pages 1–13. Springer, Berlin, Heidelberg, 2003. ISBN 978-3-540-45069-6. https://doi.org/10.1007/978-3-540-45069-6_1.

  79. I. Munro. Efficient determination of the transitive closure of a directed graph. Information Processing Letters, 1(2):56–58, 1971.

    Google Scholar 

  80. P. Purdom. A transitive closure algorithm. BIT Numerical Mathematics, 10(1): 76–94, 1970.

    Google Scholar 

  81. N. V. Rao and V. Kumar. Superlinear speedup in parallel state-space search. Foundations of Software Technology and Theoretical Computer Science, pages 161–174, 1988. http://dx.doi.org/10.1007/3-540-50517-2_79.

  82. J. H. Reif. Depth-first search is inherently sequential. Information Processing Letters, 20:229–234, 1985.

    Google Scholar 

  83. E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Three SCC-based emptiness checks for generalized Büchi automata. In K. McMillan, A. Middeldorp, and A. Voronkov, editors, Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’13), volume 8312 of Lecture Notes in Computer Science, pages 668–682. Springer, Dec. 2013. https://doi.org/10.1007/978-3-642-45221-5_44.

  84. E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Variations on parallel explicit model checking for generalized Büchi automata. International Journal on Software Tools for Technology Transfer (STTT), 19(6): 653-673, Apr. 2016.

    Google Scholar 

  85. P. Sanders. Lastverteilungsalgorithmen für parallele Tiefensuche. number 463. In Fortschrittsberichte, Reihe 10. VDI. Verlag, 1997.

    Google Scholar 

  86. W. Schudy. Finding strongly connected components in parallel using o(log2n) reachability queries. In Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures, SPAA ’08, pages 146–151, New York, NY, USA, 2008. ACM. ISBN 978-1-59593-973-9. https://doi.org/10.1145/1378533.1378560.

  87. S. Schwoon and J. Esparza. A note on on-the-fly verification algorithms. In N. Halbwachs and L. Zuck, editors, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’05), volume 3440 of Lecture Notes in Computer Science, Edinburgh, Scotland, Apr. 2005. Springer.

    Google Scholar 

  88. G. M. Slota, S. Rajamanickam, and K. Madduri. Bfs and coloring-based parallel algorithms for strongly connected components and related problems. In 2014 IEEE 28th International Parallel and Distributed Processing Symposium, pages 550–559, May 2014. https://doi.org/10.1109/IPDPS.2014.64.

  89. U. Stern and D. L. Dill. Combining state space caching and hash compaction. In Methoden des Entwurfs und der Verifikation digitaler Systeme, 4. GI/ITG/GME Workshop, pages 81–90. Shaker Verlag, 1996.

    Google Scholar 

  90. R. Tarjan. Depth-first search and linear graph algorithms. In Conference records of the 12th Annual IEEE Symposium on Switching and Automata Theory, pages 114–121. IEEE, Oct. 1971. Later republished [91].

    Google Scholar 

  91. R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146–160, 1972.

    Google Scholar 

  92. R. E. Tarjan. Efficiency of a good but not linear set union algorithm. Journal of the ACM (JACM), 22(2):215–225, Apr. 1975.

    Google Scholar 

  93. R. E. Tarjan and J. van Leeuwen. Worst-case analysis of set union algorithms. Journal of the ACM, 31(2):245–281, Mar. 1984.

    Google Scholar 

  94. H. Tauriainen. Nested emptiness search for generalized Büchi automata. In Proceedings of the 4th International Conference on Application of Concurrency to System Design (ACSD’04), pages 165–174. IEEE Computer Society, June 2004.

    Google Scholar 

  95. A. Valmari. Stubborn sets for reduced state space generation. In Proceedings of the 10th International Conference on Applications and Theory of Petri Nets (ICATPN’91), volume 618 of Lecture Notes in Computer Science, pages 491–515, London, UK, 1991. Springer-Verlag.

    Google Scholar 

  96. A. Valmari. The state explosion problem. In W. Reisig and G. Rozenberg, editors, Lectures on Petri Nets 1: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429–528. Springer-Verlag, 1998.

    Google Scholar 

  97. M. Y. Vardi. Automata-theoretic model checking revisited. In Proceedings of the 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’07), volume 4349 of Lecture Notes in Computer Science, Nice, France, Jan. 2007. Springer. Invited paper.

    Google Scholar 

  98. A. Wijs, J.-P. Katoen, and D. Bošnački. GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components, pages 310–326. Springer International Publishing, Cham, 2014. ISBN 978-3-319-08867-9. https://doi.org/10.1007/978-3-319-08867-9_20.

Download references

Author information

Authors and Affiliations

  1. Masaryk University, Brno, Czech Republic

    Jiri Barnat

  2. University of Twente, Enschede, The Netherlands

    Vincent Bloemen

  3. LRDE, Epita, Paris, France

    Alexandre Duret-Lutz & Etienne Renault

  4. TU Wien, Vienna, Austria

    Alfons Laarman

  5. LIPN, CNRS, Paris, France

    Laure Petrucci

  6. Formal Methods and Tools, University of Twente, Enschede, The Netherlands

    Jaco van de Pol

Authors
  1. Jiri Barnat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vincent Bloemen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexandre Duret-Lutz
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alfons Laarman
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Laure Petrucci
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Etienne Renault
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jiri Barnat .

Editor information

Editors and Affiliations

  1. Laboratoire d'informatique (LIX) de l'École polytechnique, Palaiseau, France

    Youssef Hamadi

  2. CRIL, CNRS UMR 8188, Université d'Artois, Lens, France

    Lakhdar Sais

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Barnat, J. et al. (2018). Parallel Model Checking Algorithms for Linear-Time Temporal Logic. In: Hamadi, Y., Sais, L. (eds) Handbook of Parallel Constraint Reasoning. Springer, Cham. https://doi.org/10.1007/978-3-319-63516-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63516-3_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63515-6

  • Online ISBN: 978-3-319-63516-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation