Advertisement

Parallel Model Checking Algorithms for Linear-Time Temporal Logic

  • Jiri Barnat
  • Vincent Bloemen
  • Alexandre Duret-Lutz
  • Alfons Laarman
  • Laure Petrucci
  • Jaco van de Pol
  • Etienne Renault
Chapter

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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. [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. [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. [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. [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. [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. [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. [8]
    C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.Google Scholar
  9. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. ]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. [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. [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. [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. [23]
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677–691, Aug. 1986.Google Scholar
  24. [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. [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. [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. [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. [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. [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. [30]
    E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 2000.Google Scholar
  31. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [54]
    P. Godefroid. Using partial orders to improve automatic verification methods. In Computer-Aided Verification, pages 176–185. Springer, 1991.Google Scholar
  55. [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. [56]
    R. Greenlaw, H. J. Hoover, and W. L. Ruzzo. Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, 1995.Google Scholar
  57. [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. [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. [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. [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. [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. [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. [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. [64]
    A. Laarman. Scalable multi-core model checking. PhD thesis, University of Twente, 2014.Google Scholar
  65. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [79]
    I. Munro. Efficient determination of the transitive closure of a directed graph. Information Processing Letters, 1(2):56–58, 1971.Google Scholar
  80. [80]
    P. Purdom. A transitive closure algorithm. BIT Numerical Mathematics, 10(1): 76–94, 1970.Google Scholar
  81. [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. [82]
    J. H. Reif. Depth-first search is inherently sequential. Information Processing Letters, 20:229–234, 1985.Google Scholar
  83. [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. [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. [85]
    P. Sanders. Lastverteilungsalgorithmen für parallele Tiefensuche. number 463. In Fortschrittsberichte, Reihe 10. VDI. Verlag, 1997.Google Scholar
  86. [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. [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. [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. [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. [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. [91]
    R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146–160, 1972.Google Scholar
  92. [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. [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. [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. [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. [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. [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. [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.

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Jiri Barnat
    • 1
  • Vincent Bloemen
    • 2
  • Alexandre Duret-Lutz
    • 3
  • Alfons Laarman
    • 4
  • Laure Petrucci
    • 5
  • Jaco van de Pol
    • 6
  • Etienne Renault
    • 3
  1. 1.Masaryk UniversityBrnoCzech Republic
  2. 2.University of TwenteEnschedeThe Netherlands
  3. 3.LRDE, EpitaParisFrance
  4. 4.TU WienViennaAustria
  5. 5.LIPN, CNRSParisFrance
  6. 6.Formal Methods and ToolsUniversity of TwenteEnschedeThe Netherlands

Personalised recommendations