4 Search Results for "Pavlogiannis, Andreas"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.124
Reachability in Bidirected Pushdown VASS

Authors: Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be bidirected if every transition (pushing/popping a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for bidirected PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension. For the special case of one-dimensional bidirected PVASS, we show reachability is in PSPACE, and in fact in polynomial time if the stack is polynomially bounded. Our results are in contrast to the directed setting, where decidability of reachability is a long-standing open problem already for one dimensional PVASS, and there is a PSPACE-lower bound already for one-dimensional PVASS with bounded stack. The reachability relation in the bidirected (stateless) case is a congruence over ℕ^d. Our upper bounds exploit saturation techniques over congruences. In particular, we show novel elementary-time constructions of semilinear representations of congruences generated by finitely many vector pairs. In the case of one-dimensional PVASS, we employ a saturation procedure over bounded-size counters. We complement our upper bound with a TOWER-hardness result for arbitrary dimension and k-EXPSPACE hardness in dimension 2k+6 using a technique by Lazić and Totzke to implement iterative exponentiations.
Cite as

Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. Reachability in Bidirected Pushdown VASS. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 124:1-124:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ganardi_et_al:LIPIcs.ICALP.2022.124,
  author =	{Ganardi, Moses and Majumdar, Rupak and Pavlogiannis, Andreas and Sch\"{u}tze, Lia and Zetzsche, Georg},
  title =	{{Reachability in Bidirected Pushdown VASS}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{124:1--124:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.124},
  URN =		{urn:nbn:de:0030-drops-164651},
  doi =		{10.4230/LIPIcs.ICALP.2022.124},
  annote =	{Keywords: Vector addition systems, Pushdown, Reachability, Decidability, Complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.42
Quantitative Verification on Product Graphs of Small Treewidth

Authors: Krishnendu Chatterjee, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

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^{-λ}).
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.FSTTCS.2021.42,
  author =	{Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  title =	{{Quantitative Verification on Product Graphs of Small Treewidth}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{42:1--42:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.42},
  URN =		{urn:nbn:de:0030-drops-155533},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.42},
  annote =	{Keywords: graph algorithms, algebraic paths, mean-payoff, initial credit for energy}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.16
Dynamic Data-Race Detection Through the Fine-Grained Lens

Authors: Rucha Kulkarni, Umang Mathur, and Andreas Pavlogiannis

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Data races are among the most common bugs in concurrency. The standard approach to data-race detection is via dynamic analyses, which work over executions of concurrent programs, instead of the program source code. The rich literature on the topic has created various notions of dynamic data races, which are known to be detected efficiently when certain parameters (e.g., number of threads) are small. However, the fine-grained complexity of all these notions of races has remained elusive, making it impossible to characterize their trade-offs between precision and efficiency. In this work we establish several fine-grained separations between many popular notions of dynamic data races. The input is an execution trace σ with 𝒩 events, 𝒯 threads and ℒ locks. Our main results are as follows. First, we show that happens-before HB races can be detected in O(𝒩⋅ min(𝒯, ℒ)) time, improving over the standard O(𝒩⋅ 𝒯) bound when ℒ = o(𝒯). Moreover, we show that even reporting an HB race that involves a read access is hard for 2-orthogonal vectors (2-OV). This is the first rigorous proof of the conjectured quadratic lower-bound in detecting HB races. Second, we show that the recently introduced synchronization-preserving races are hard to detect for 3-OV and thus have a cubic lower bound, when 𝒯 = Ω(𝒩). This establishes a complexity separation from HB races which are known to be strictly less expressive. Third, we show that lock-cover races are hard for 2-OV, and thus have a quadratic lower-bound, even when 𝒯 = 2 and ℒ = ω(log 𝒩). The similar notion of lock-set races is known to be detectable in O(𝒩⋅ ℒ) time, and thus we achieve a complexity separation between the two. Moreover, we show that lock-set races become hitting-set (HS)-hard when ℒ = Θ(𝒩), and thus also have a quadratic lower bound, when the input is sufficiently complex. To our knowledge, this is the first work that characterizes the complexity of well-established dynamic race-detection techniques, allowing for a rigorous comparison between them.
Cite as

Rucha Kulkarni, Umang Mathur, and Andreas Pavlogiannis. Dynamic Data-Race Detection Through the Fine-Grained Lens. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 16:1-16:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kulkarni_et_al:LIPIcs.CONCUR.2021.16,
  author =	{Kulkarni, Rucha and Mathur, Umang and Pavlogiannis, Andreas},
  title =	{{Dynamic Data-Race Detection Through the Fine-Grained Lens}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{16:1--16:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.16},
  URN =		{urn:nbn:de:0030-drops-143931},
  doi =		{10.4230/LIPIcs.CONCUR.2021.16},
  annote =	{Keywords: dynamic analyses, data races, fine-grained complexity}
}
Document
DOI: 10.4230/LIPIcs.ESA.2016.28
Optimal Reachability and a Space-Time Tradeoff for Distance Queries in Constant-Treewidth Graphs

Authors: Krishnendu Chatterjee, Rasmus Rasmus Ibsen-Jensen, and Andreas Pavlogiannis

Published in: LIPIcs, Volume 57, 24th Annual European Symposium on Algorithms (ESA 2016)

Abstract
We consider data-structures for answering reachability and distance queries on constant-treewidth graphs with n nodes, on the standard RAM computational model with wordsize W=Theta(log n). Our first contribution is a data-structure that after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time; and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. The data-structure uses at all times O(n) space. Our second contribution is a space-time tradeoff data-structure for distance queries. For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing time that allows pair queries in O(n^{1-\epsilon} alpha(n)) time, where alpha is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space. The input graph G is not considered in the space complexity.
Cite as

Krishnendu Chatterjee, Rasmus Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Optimal Reachability and a Space-Time Tradeoff for Distance Queries in Constant-Treewidth Graphs. In 24th Annual European Symposium on Algorithms (ESA 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 57, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.ESA.2016.28,
  author =	{Chatterjee, Krishnendu and Rasmus Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  title =	{{Optimal Reachability and a Space-Time Tradeoff for Distance Queries in Constant-Treewidth Graphs}},
  booktitle =	{24th Annual European Symposium on Algorithms (ESA 2016)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-015-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{57},
  editor =	{Sankowski, Piotr and Zaroliagis, Christos},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2016.28},
  URN =		{urn:nbn:de:0030-drops-63797},
  doi =		{10.4230/LIPIcs.ESA.2016.28},
  annote =	{Keywords: Graph algorithms, Constant-treewidth graphs, Reachability queries, Distance queries}
}
  • Refine by Author
  • 4 Pavlogiannis, Andreas
  • 2 Chatterjee, Krishnendu
  • 1 Ganardi, Moses
  • 1 Ibsen-Jensen, Rasmus
  • 1 Kulkarni, Rucha
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Software testing and debugging
  • 1 Theory of computation → Graph algorithms analysis
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Models of computation
  • 1 Theory of computation → Parameterized complexity and exact algorithms
  • Show More...

  • Refine by Keyword
  • 1 Complexity
  • 1 Constant-treewidth graphs
  • 1 Decidability
  • 1 Distance queries
  • 1 Graph algorithms
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2021
  • 1 2016
  • 1 2022

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