Document Open Access Logo

Quantitative Verification on Product Graphs of Small Treewidth

Authors Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.42.pdf
  • Filesize: 0.85 MB
  • 23 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
  • IST Austria, Klosterneuburg, Austria
Rasmus Ibsen-Jensen
  • University of Liverpool, UK
Andreas Pavlogiannis
  • Aarhus University, Denmark

Cite AsGet BibTex

Krishnendu Chatterjee, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Quantitative Verification on Product Graphs of Small Treewidth. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42

Abstract

Product graphs arise naturally in formal verification and program analysis. For example, the analysis of two concurrent threads requires the product of two component control-flow graphs, and for language inclusion of deterministic automata the product of two automata is constructed. In many cases, the component graphs have constant treewidth, e.g., when the input contains control-flow graphs of programs. We consider the algorithmic analysis of products of two constant-treewidth graphs with respect to three classic specification languages, namely, (a) algebraic properties, (b) mean-payoff properties, and (c) initial credit for energy properties. Our main contributions are as follows. Consider a graph G that is the product of two constant-treewidth graphs of size n each. First, given an idempotent semiring, we present an algorithm that computes the semiring transitive closure of G in time Õ(n⁴). Since the output has size Θ(n⁴), our algorithm is optimal (up to polylog factors). Second, given a mean-payoff objective, we present an O(n³)-time algorithm for deciding whether the value of a starting state is non-negative, improving the previously known O(n⁴) bound. Third, given an initial credit for energy objective, we present an O(n⁵)-time algorithm for computing the minimum initial credit for all nodes of G, improving the previously known O(n⁸) bound. At the heart of our approach lies an algorithm for the efficient construction of strongly-balanced tree decompositions of constant-treewidth graphs. Given a constant-treewidth graph G' of n nodes and a positive integer λ, our algorithm constructs a binary tree decomposition of G' of width O(λ) with the property that the size of each subtree decreases geometrically with rate (1/2 + 2^{-λ}).

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Verification by model checking
  • Theory of computation → Graph algorithms analysis
Keywords
  • graph algorithms
  • algebraic paths
  • mean-payoff
  • initial credit for energy

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Luca Aceto, A. Ingólfsdóttir, Mohammad Reza Mousavi, and M. A. Reniers. Algebraic properties for free! Bulletin of the European Association for Theoretical Computer Science, 99:81-103, 2009. Google Scholar
  2. Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs. J. Algorithms, 12(2):308-340, April 1991. Google Scholar
  3. C. Baier and J-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  4. Omer Berkman and Uzi Vishkin. Finding level-ancestors in trees. Journal of Computer and System Sciences, 48(2), 1994. Google Scholar
  5. Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, and Barbara Jobstmann. Better quality in synthesis through quantitative objectives. In Computer Aided Verification, pages 140-156, 2009. Google Scholar
  6. Hans L. Bodlaender. A partial k-arboretum of graphs with bounded treewidth. Theoretical Computer Science, 209(1-2):1-45, 1998. Google Scholar
  7. Hans L. Bodlaender and Torben Hagerup. Parallel algorithms with optimal speedup for bounded treewidth. In Zoltán Fülöp and Ferenc Gécseg, editors, Automata, Languages and Programming, pages 268-279, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  8. Mikołaj Bojańczyk and Michał Pilipczuk. Definability equals recognizability for graphs of bounded treewidth. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 407-416, New York, NY, USA, 2016. ACM. Google Scholar
  9. Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. Temporal specifications with accumulative values. ACM TOCL, 15(4):27:1-27:25, 2014. Google Scholar
  10. Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, and Nicolas Markey. Timed automata with observers under energy constraints. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC '10, pages 61-70, New York, NY, USA, 2010. ACM. Google Scholar
  11. Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Jiří Srba. Infinite runs in weighted timed automata with energy constraints. In Formal Modeling and Analysis of Timed Systems, volume 5215 of Lecture Notes in Computer Science, pages 33-47. Springer Berlin Heidelberg, 2008. Google Scholar
  12. Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In CONCUR 2014, pages 266-280, 2014. Google Scholar
  13. Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. Acta Informatica, 55(2):91-127, March 2018. Google Scholar
  14. Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, and Rohit Singh. Quantitative synthesis for concurrent programs. In Computer Aided Verification, pages 243-259, 2011. Google Scholar
  15. Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis. Optimal dyck reachability for data-dependence and alias analysis. PACMPL, 2(POPL):30:1-30:30, 2018. Google Scholar
  16. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Expressiveness and closure properties for quantitative languages. LMCS, 6(3), 2010. Google Scholar
  17. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM TOCL, 11(4):23, 2010. Google Scholar
  18. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In Peter Müller, editor, ETAPS (ESOP), volume 12075 of Lecture Notes in Computer Science, pages 112-140. Springer, 2020. Google Scholar
  19. Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Trans. Program. Lang. Syst., 40(3):9:1-9:43, 2018. URL: https://doi.org/10.1145/3210257.
  20. Krishnendu Chatterjee, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Faster algorithms for quantitative verification in constant treewidth graphs. In Daniel Kroening and Corina S. Păsăreanu, editors, Computer Aided Verification, pages 140-157, Cham, 2015. Springer International Publishing. Google Scholar
  21. Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 97-109, New York, NY, USA, 2015. ACM. Google Scholar
  22. Krishnendu Chatterjee, Andreas Pavlogiannis, and Yaron Velner. Quantitative interprocedural analysis. In Principles of Programming Languages, POPL 2015, pages 539-551, 2015. Google Scholar
  23. Shiva Chaudhuri and Christos D. Zaroliagis. Shortest Paths in Digraphs of Small Treewidth. Part I: Sequential Algorithms. Algorithmica, 27:212-226, 1995. Google Scholar
  24. Ravi Chugh, Jan W. Voung, Ranjit Jhala, and Sorin Lerner. Dataflow analysis for concurrent programs using datarace detection. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, 2008. Google Scholar
  25. Fan RK Chung. Separator theorems and their applications. Universität Bonn. Institut für Ökonometrie und Operations Research, 1988. Google Scholar
  26. Bruno Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and Computation, 85, 1990. Google Scholar
  27. Arnab De, Deepak D'Souza, and Rupesh Nasre. Dataflow analysis for datarace-free programs. In Proceedings of the 20th European Conference on Programming Languages and Systems: Part of the Joint European Conferences on Theory and Practice of Software, ESOP'11/ETAPS'11, pages 196-215. Springer-Verlag, 2011. Google Scholar
  28. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer, 1st edition, 2009. Google Scholar
  29. Manfred Droste and Ingmar Meinecke. Weighted automata and weighted MSO logics for average and long-time behaviors. Inf. Comput., 220:44-59, 2012. Google Scholar
  30. Michael Elberfeld, Andreas Jakoby, and Till Tantau. Logspace versions of the theorems of Bodlaender and Courcelle. In Proceedings of the 2010 IEEE 51st Annual Symposium on Foundations of Computer Science, FOCS '10, pages 143-152, USA, 2010. IEEE Computer Society. Google Scholar
  31. Uli Fahrenberg, Line Juhl, Kim G. Larsen, and Jiří Srba. Energy games in multiweighted automata. In Proceedings of the 8th International Conference on Theoretical Aspects of Computing, ICTAC'11, pages 95-115, Berlin, Heidelberg, 2011. Springer-Verlag. Google Scholar
  32. Azadeh Farzan and P. Madhusudan. Causal dataflow analysis for concurrent programs. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2007. Google Scholar
  33. J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer-Verlag, 1997. Google Scholar
  34. Robert W. Floyd. Algorithm 97: Shortest path. Communications of the ACM, 5(6):345, 1962. Google Scholar
  35. Fedor V. Fomin, Daniel Lokshtanov, MichałPilipczuk, Saket Saurabh, and Marcin Wrochna. Fully polynomial-time parameterized computations for graphs and matrices of low treewidth. In Proceedings of the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '17, pages 1419-1432, Philadelphia, PA, USA, 2017. Society for Industrial and Applied Mathematics. Google Scholar
  36. Dirk Grunwald and Harini Srinivasan. Data flow equations for explicitly parallel programs. In Proceedings of the Fourth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP, 1993. Google Scholar
  37. Jens Gustedt, OleA. Maehle, and JanArne Telle. The treewidth of java programs. In Algorithm Engineering and Experiments, volume 2409 of Lecture Notes in Computer Science, pages 86-97. Springer Berlin Heidelberg, 2002. Google Scholar
  38. C. A. Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent kleene algebra. In Proceedings of the 20th International Conference on Concurrency Theory, CONCUR 2009, pages 399-414, Berlin, Heidelberg, 2009. Springer-Verlag. Google Scholar
  39. Peter Jipsen. Concurrent kleene algebra with tests. In Peter Höfner, Peter Jipsen, Wolfram Kahl, and Martin Eric Müller, editors, Relational and Algebraic Methods in Computer Science, pages 37-48, Cham, 2014. Springer International Publishing. Google Scholar
  40. Line Juhl, Kim Guldstrand Larsen, and Jean-François Raskin. Optimal bounds for multiweighted and parametrised energy games. In Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors, Theories of Programming and Formal Methods, pages 244-255, Berlin, Heidelberg, 2013. Springer-Verlag. Google Scholar
  41. Vineet Kahlon, Nishant Sinha, Erik Kruus, and Yun Zhang. Static data race detection for concurrent programs with asynchronous calls. In Proceedings of the the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC/FSE '09, pages 13-22, 2009. Google Scholar
  42. Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi. Concurrent kleene algebra: Free model and completeness. In Amal Ahmed, editor, Programming Languages and Systems, pages 856-882, Cham, 2018. Springer International Publishing. Google Scholar
  43. Richard M. Karp. A characterization of the minimum cycle mean in a digraph. Discrete Mathematics, 1978. Google Scholar
  44. S. C. Kleene. Representation of events in nerve nets and finite automata. Automata Studies, 1956. Google Scholar
  45. Jens Knoop, Bernhard Steffen, and Jürgen Vollmer. Parallelism for free: Efficient and optimal bitvector analyses for parallel programs. ACM Trans. Program. Lang. Syst., 1996. Google Scholar
  46. J. Lagergren. Efficient parallel algorithms for tree-decomposition and related problems. In Proceedings [1990] 31st Annual Symposium on Foundations of Computer Science, pages 173-182 vol.1, 1990. Google Scholar
  47. Daniel J. Lehmann. Algebraic structures for transitive closure. Theoretical Computer Science, 1977. Google Scholar
  48. Jan Obdrzálek. Fast mu-calculus model checking when tree-width is bounded. In CAV, 2003. Google Scholar
  49. M.L. Puterman. Markov Decision Processes. John Wiley and Sons, 1994. Google Scholar
  50. Bruce A. Reed. Finding approximate separators and computing tree width quickly. In Proceedings of the Twenty-fourth Annual ACM Symposium on Theory of Computing, STOC '92, 1992. Google Scholar
  51. Thomas Reps, Susan Horwitz, and Mooly Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, New York, NY, USA, 1995. ACM. Google Scholar
  52. Neil Robertson and P.D Seymour. Graph minors. iii. planar tree-width. Journal of Combinatorial Theory, Series B, 36(1):49-64, 1984. Google Scholar
  53. Mikkel Thorup. All Structured Programs Have Small Tree Width and Good Register Allocation. Information and Computation, 142(2):159-181, 1998. Google Scholar
  54. Stephen Warshall. A Theorem on Boolean Matrices. J. ACM, 9(1):11-12, January 1962. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact