---
_id: '10629'
abstract:
- lang: eng
  text: "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.\r\nOur
    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^{-λ})."
alternative_title:
- LIPIcs
article_number: '42'
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Rasmus
  full_name: Ibsen-Jensen, Rasmus
  id: 3B699956-F248-11E8-B48F-1D18A9856A87
  last_name: Ibsen-Jensen
  orcid: 0000-0003-4783-0389
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
citation:
  ama: 'Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Quantitative verification on
    product graphs of small treewidth. In: <i>41st IARCS Annual Conference on Foundations
    of Software Technology and Theoretical Computer Science</i>. Vol 213. Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik; 2021. doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42">10.4230/LIPIcs.FSTTCS.2021.42</a>'
  apa: 'Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Quantitative
    verification on product graphs of small treewidth. In <i>41st IARCS Annual Conference
    on Foundations of Software Technology and Theoretical Computer Science</i> (Vol.
    213). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42">https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42</a>'
  chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
    “Quantitative Verification on Product Graphs of Small Treewidth.” In <i>41st IARCS
    Annual Conference on Foundations of Software Technology and Theoretical Computer
    Science</i>, Vol. 213. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
    <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42">https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42</a>.
  ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Quantitative verification
    on product graphs of small treewidth,” in <i>41st IARCS Annual Conference on Foundations
    of Software Technology and Theoretical Computer Science</i>, Virtual, 2021, vol.
    213.
  ista: 'Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Quantitative verification
    on product graphs of small treewidth. 41st IARCS Annual Conference on Foundations
    of Software Technology and Theoretical Computer Science. FSTTCS: Foundations of
    Software Technology and Theoretical Computer Science, LIPIcs, vol. 213, 42.'
  mla: Chatterjee, Krishnendu, et al. “Quantitative Verification on Product Graphs
    of Small Treewidth.” <i>41st IARCS Annual Conference on Foundations of Software
    Technology and Theoretical Computer Science</i>, vol. 213, 42, Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2021, doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42">10.4230/LIPIcs.FSTTCS.2021.42</a>.
  short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, 41st IARCS Annual Conference
    on Foundations of Software Technology and Theoretical Computer Science, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
conference:
  end_date: 2021-12-17
  location: Virtual
  name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
  start_date: 2021-12-15
date_created: 2022-01-16T23:01:28Z
date_published: 2021-11-29T00:00:00Z
date_updated: 2022-01-17T10:39:40Z
day: '29'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.FSTTCS.2021.42
file:
- access_level: open_access
  checksum: 71141acdeffa9056f24d6dbef952d254
  content_type: application/pdf
  creator: cchlebak
  date_created: 2022-01-17T10:36:08Z
  date_updated: 2022-01-17T10:36:08Z
  file_id: '10633'
  file_name: 2021_LIPIcs_Chatterjee.pdf
  file_size: 891566
  relation: main_file
  success: 1
file_date_updated: 2022-01-17T10:36:08Z
has_accepted_license: '1'
intvolume: '       213'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
publication: 41st IARCS Annual Conference on Foundations of Software Technology and
  Theoretical Computer Science
publication_identifier:
  isbn:
  - 978-3-9597-7215-0
  issn:
  - 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative verification on product graphs of small treewidth
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 213
year: '2021'
...
---
_id: '10630'
abstract:
- lang: eng
  text: In the Intersection Non-emptiness problem, we are given a list of finite automata
    A_1, A_2,… , A_m over a common alphabet Σ as input, and the goal is to determine
    whether some string w ∈ Σ^* lies in the intersection of the languages accepted
    by the automata in the list. We analyze the complexity of the Intersection Non-emptiness
    problem under the promise that all input automata accept a language in some level
    of the dot-depth hierarchy, or some level of the Straubing-Thérien hierarchy.
    Automata accepting languages from the lowest levels of these hierarchies arise
    naturally in the context of model checking. We identify a dichotomy in the dot-depth
    hierarchy by showing that the problem is already NP-complete when all input automata
    accept languages of the levels B_0 or B_{1/2} and already PSPACE-hard when all
    automata accept a language from the level B_1. Conversely, we identify a tetrachotomy
    in the Straubing-Thérien hierarchy. More precisely, we show that the problem is
    in AC^0 when restricted to level L_0; complete for L or NL, depending on the input
    representation, when restricted to languages in the level L_{1/2}; NP-complete
    when the input is given as DFAs accepting a language in L_1 or L_{3/2}; and finally,
    PSPACE-complete when the input automata accept languages in level L_2 or higher.
    Moreover, we show that the proof technique used to show containment in NP for
    DFAs accepting languages in L_1 or L_{3/2} does not generalize to the context
    of NFAs. To prove this, we identify a family of languages that provide an exponential
    separation between the state complexity of general NFAs and that of partially
    ordered NFAs. To the best of our knowledge, this is the first superpolynomial
    separation between these two models of computation.
acknowledgement: "We like to thank Lukas Fleischer and Michael Wehar for our discussions.
  This work started at the Schloss Dagstuhl Event 20483 Moderne Aspekte der Komplexitätstheorie
  in der Automatentheorie https://www.dagstuhl.de/20483.\r\n"
alternative_title:
- LIPIcs
article_number: '34'
article_processing_charge: No
arxiv: 1
author:
- first_name: Emmanuel
  full_name: Arrighi, Emmanuel
  last_name: Arrighi
- first_name: Henning
  full_name: Fernau, Henning
  last_name: Fernau
- first_name: Stefan
  full_name: Hoffmann, Stefan
  last_name: Hoffmann
- first_name: Markus
  full_name: Holzer, Markus
  last_name: Holzer
- first_name: Ismael R
  full_name: Jecker, Ismael R
  id: 85D7C63E-7D5D-11E9-9C0F-98C4E5697425
  last_name: Jecker
- first_name: Mateus
  full_name: De Oliveira Oliveira, Mateus
  last_name: De Oliveira Oliveira
- first_name: Petra
  full_name: Wolf, Petra
  last_name: Wolf
citation:
  ama: 'Arrighi E, Fernau H, Hoffmann S, et al. On the complexity of intersection
    non-emptiness for star-free language classes. In: <i>41st IARCS Annual Conference
    on Foundations of Software Technology and Theoretical Computer Science</i>. Vol
    213. Schloss Dagstuhl - Leibniz Zentrum für Informatik; 2021. doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2021.34">10.4230/LIPIcs.FSTTCS.2021.34</a>'
  apa: 'Arrighi, E., Fernau, H., Hoffmann, S., Holzer, M., Jecker, I. R., De Oliveira
    Oliveira, M., &#38; Wolf, P. (2021). On the complexity of intersection non-emptiness
    for star-free language classes. In <i>41st IARCS Annual Conference on Foundations
    of Software Technology and Theoretical Computer Science</i> (Vol. 213). Virtual:
    Schloss Dagstuhl - Leibniz Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2021.34">https://doi.org/10.4230/LIPIcs.FSTTCS.2021.34</a>'
  chicago: Arrighi, Emmanuel, Henning Fernau, Stefan Hoffmann, Markus Holzer, Ismael
    R Jecker, Mateus De Oliveira Oliveira, and Petra Wolf. “On the Complexity of Intersection
    Non-Emptiness for Star-Free Language Classes.” In <i>41st IARCS Annual Conference
    on Foundations of Software Technology and Theoretical Computer Science</i>, Vol.
    213. Schloss Dagstuhl - Leibniz Zentrum für Informatik, 2021. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2021.34">https://doi.org/10.4230/LIPIcs.FSTTCS.2021.34</a>.
  ieee: E. Arrighi <i>et al.</i>, “On the complexity of intersection non-emptiness
    for star-free language classes,” in <i>41st IARCS Annual Conference on Foundations
    of Software Technology and Theoretical Computer Science</i>, Virtual, 2021, vol.
    213.
  ista: 'Arrighi E, Fernau H, Hoffmann S, Holzer M, Jecker IR, De Oliveira Oliveira
    M, Wolf P. 2021. On the complexity of intersection non-emptiness for star-free
    language classes. 41st IARCS Annual Conference on Foundations of Software Technology
    and Theoretical Computer Science. FSTTCS: Foundations of Software Technology and
    Theoretical Computer Science, LIPIcs, vol. 213, 34.'
  mla: Arrighi, Emmanuel, et al. “On the Complexity of Intersection Non-Emptiness
    for Star-Free Language Classes.” <i>41st IARCS Annual Conference on Foundations
    of Software Technology and Theoretical Computer Science</i>, vol. 213, 34, Schloss
    Dagstuhl - Leibniz Zentrum für Informatik, 2021, doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2021.34">10.4230/LIPIcs.FSTTCS.2021.34</a>.
  short: E. Arrighi, H. Fernau, S. Hoffmann, M. Holzer, I.R. Jecker, M. De Oliveira
    Oliveira, P. Wolf, in:, 41st IARCS Annual Conference on Foundations of Software
    Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz Zentrum
    für Informatik, 2021.
conference:
  end_date: 2021-12-17
  location: Virtual
  name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
  start_date: 2021-12-15
date_created: 2022-01-16T23:01:29Z
date_published: 2021-11-29T00:00:00Z
date_updated: 2022-01-17T10:56:19Z
day: '29'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.FSTTCS.2021.34
ec_funded: 1
external_id:
  arxiv:
  - '2110.01279'
file:
- access_level: open_access
  checksum: d5a82ba893c3bc5da5914edbb3efb92b
  content_type: application/pdf
  creator: cchlebak
  date_created: 2022-01-17T10:49:03Z
  date_updated: 2022-01-17T10:49:03Z
  file_id: '10634'
  file_name: 2021_LIPIcs_Arrighi.pdf
  file_size: 844224
  relation: main_file
  success: 1
file_date_updated: 2022-01-17T10:49:03Z
has_accepted_license: '1'
intvolume: '       213'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '754411'
  name: ISTplus - Postdoctoral Fellowships
publication: 41st IARCS Annual Conference on Foundations of Software Technology and
  Theoretical Computer Science
publication_identifier:
  isbn:
  - 978-3-9597-7215-0
  issn:
  - 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: On the complexity of intersection non-emptiness for star-free language classes
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 213
year: '2021'
...