Skip Navigation



Journal of Logic and Computation Advance Access published online on February 17, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp003
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Barnat, J.
Right arrow Articles by Van De Pol, J.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Distributed Algorithms for SCC Decomposition

Jirí Barnat and Jakub Chaloupka

Department of Computer Science, Faculty of Informatics, Masaryk University Brno, Czech Republic.
E-mail: barnat{at}fi.muni.cz; xchalou1{at}fi.muni.cz

Jaco Van De Pol

Formal Methods and Tools, Department of EEMCS, University of Twente, The Netherlands.
E-mail: j.c.vandepol{at}ewi.utwente.nl

Received 29 February 2008.

We study existing parallel algorithms for the decomposition of a partitioned graph into its strongly connected components (SCCs). In particular, we identify several individual procedures that the algorithms are assembled from and show how to assemble a new and more efficient algorithm, called Recursive OBF (OBFR), to solve the decomposition problem. We also report on a thorough experimental study to evaluate the new algorithm. It shows that it is possible to perform SCC decomposition in parallel efficiently and that OBFR, if properly implemented, is the best choice in most cases.

Keywords: parallel algorithms; strongly connected components



References

  1. Amato N. Improved processor bounds for parallel algorithms for weighted directed graphs. Information Processing Letters (1993) 45:147–152.[CrossRef][Web of Science]
  2. Barnat J, Brim L, Cerná I, Moravec P, Rockai P, Simecek P. Divine – a tool for distributed verification. (2006) Springer Berlin/Heidelberg. 278–281. In Proceedings of Computer Aided Verification, Vol. 4144/2006 of Lecture Notes in Computer Science.
  3. Barnat J, Chaloupka J, van de Pol JC. Improved distributed algorithms for SCC decomposition. In: Participant proceedings of the Sixth International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2007) (2007) CTIT: University of Twente. 65–80.
  4. Barnat J, Moravec P. Parallel algorithms for finding SCCs in implicitly given graphs. (2007) Springer-Verlag. 316–330. In Proceedings of the 5th International Workshop on Parallel and Distributed Methods in Verification (PDMC 2006). Vol. 4346 of Lecture Notes in Computer Science.
  5. Behrmann G. A performance study of distributed timed automata reachability analysis. (2002) Elsevier Science Publishers. In Proceedings of the Workshop on Parallel and Distributed Model Checking. Vol. 68 of Electronic Notes in Theoretical Computer Science.
  6. Blom SCC, Calamé JR, Lisser B, Orzan S, Pang J, van de Pol JC, Torabi Dashti M, Wijs AJ. Distributed analysis with µcrl: a compendium of case studies. Grumberg O, Huth M, eds. (2007) Braga, Portugal, Berlin: Springer Verlag. 683–689. In Tools and Algorithms for the Construction and Analysis of Systems, Vol. 4424 of Lecture Notes in Computer Science.
  7. Blom SCC, Garavel H. The VLTS benchmark suite. (2003) (last accessed on 4 February, 2009). Available at: http://www.inrialpes.fr/vasy/cadp/resources/benchmark_bcg.html.
  8. Blom SCC, van de Pol JC. State space reduction by proving confluence. Brinksma E, Larsen KG, Larsen KG, eds. (2002) Springer. 596–609. In CAV, Vol. 2404 of Lecture Notes in Computer Science.
  9. Brim L, Cerná I, Moravec P, Simsa J. Accepting predecessors are better than back edges in distributed LTL model-checking. (2004) Springer-Verlag. 352–366. In Proceddings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD’04). Vol. 3312 of Lecture Notes in Computer Science.
  10. Caselli S, Conte G, Marenzoni P. Parallel state space exploration for GSPN models. De Michelis G, Diaz M, eds. (1995) Springer-Verlag. 181–200. In Applications and Theory of Petri Nets 1995, Vol. 935 of Lecture Notes in Computer Science.
  11. Ciardo G, Gluckman J, Nicol DM. Distributed state space generation of discrete-state stochastic models. INFORMS Journal of Computing (1997) 47:153–167.
  12. Ciesinski F, Baier C. LiQuor: a tool for qualitative and qualitative linear time analysis of reactive systems. In: IEEE Computer Society (2006) 3rd International Conference on the Quantitative Evaluation of Systems (QEST 2006), 131–132.
  13. Clarke EM, Grumberg O, Peled DA. Model Checking (1999) Cambridge, MA: The MIT Press.
  14. Cole R, Vishkin U. Faster optimal parallel prefix sums and list ranking. Information and Computation (1989) 81:334–352.[CrossRef][Web of Science]
  15. Cormen TH, Leiserson CE, Rivest RL. Introduction to Algorithms (1990) MIT Press.
  16. Fisler K, Fraer R, Kamhi G, Vardi MY, Yang Z. Is there a best symbolic cycle-detection algorithm? (2001) Springer. 420–434. In Proceedings of theTools and Algorithms for Construction and Analysis of Systems. Vol. 2031 of Lecture Notes in Computer Science.
  17. Fleischer LK, Hendrickson B, Pinar A. On identifying strongly connected components in parallel. (2000) Springer. 505–511. Vol. 1800 of Lecture Notes in Computer Science.
  18. Garavel H, Mateescu R, Smarandache IM. Parallel state space construction for model-checking. (2001) Springer-Verlag. 200–216. In Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN’01). Vol. 2057 of Lecture Notes in Computer Science.
  19. Gazit H, Miller GL. An improved parallel algorithm that computes the BFS numbering of a directed graph. Information Processing Letters (1988) 28:61–65.[CrossRef][Web of Science]
  20. McLendon W III, Hendrickson B, Plimpton SJ, Rauchwerger L. Finding strongly connected components in distributed graphs. Journal of Parallel Distribution Computation (2005) 65:901–910.[CrossRef]
  21. Lerda F, Sisto R. Distributed-memory model checking with SPIN. (1999) Springer-Verlag. In Proceedings of the 6th International SPINWorkshop on Model Checking of Software (SPIN’99). Vol. 1680 of Lecture Notes in Computer Science.
  22. Orzan S. On Distributed Verification and Verified Distribution (2004) Free University of Amsterdam. PhD Thesis.
  23. Reif JH. Depth-first search is inherently sequential. Information Processing Letters (1985) 20:229–234.[CrossRef][Web of Science]
  24. Stern U, Dill DL. Parallelizing the Mur{phi} verifier. Grumberg O, ed. (1997) Springer-Verlag. 256–267. In Proceedings of Computer Aided Verification (CAV’97), Vol. 1254 of Lecture Notes in Computer Science.
  25. Tarjan R. Depth first search and linear graph algorithms. SIAM Journal on computing (1972) 1:146–160.[CrossRef]

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Barnat, J.
Right arrow Articles by Van De Pol, J.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?