4
4.0
Jun 30, 2018
06/18
by
Christoph Haase
texts
eye 4
favorite 0
comment 0
It is shown that for any fixed $i>0$, the $\Sigma_{i+1}$-fragment of Presburger arithmetic, i.e., its restriction to $i+1$ quantifier alternations beginning with an existential quantifier, is complete for $\mathsf{\Sigma}^{\mathsf{EXP}}_{i}$, the $i$-th level of the weak EXP hierarchy, an analogue to the polynomial-time hierarchy residing between $\mathsf{NEXP}$ and $\mathsf{EXPSPACE}$. This result completes the computational complexity landscape for Presburger arithmetic, a line of research...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1401.5266
7
7.0
Jun 30, 2018
06/18
by
Christoph Haase; Simon Halfon
texts
eye 7
favorite 0
comment 0
This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Although it is folklore that reachability in ZVASS is NP-complete, it turns out that despite their naturalness, from a complexity point of view this class has received little attention in the literature. We fill this gap by...
Topics: Computing Research Repository, Formal Languages and Automata Theory
Source: http://arxiv.org/abs/1406.2590
22
22
Jun 28, 2018
06/18
by
Christoph Haase; Piotr Hofman
texts
eye 22
favorite 0
comment 0
We show that the language equivalence problem for regular and context-free commutative grammars is coNEXP-complete. In addition, our lower bound immediately yields further coNEXP-completeness results for equivalence problems for communication-free Petri nets and reversal-bounded counter automata. Moreover, we improve both lower and upper bounds for language equivalence for exponent-sensitive commutative grammars.
Topics: Computing Research Repository, Formal Languages and Automata Theory, Logic in Computer Science
Source: http://arxiv.org/abs/1506.07774
9
9.0
Jun 26, 2018
06/18
by
Christoph Haase; Stefan Kiefer
texts
eye 9
favorite 0
comment 0
We show that the Kth largest subset problem and the Kth largest m-tuple problem are in PP and hard for PP under polynomial-time Turing reductions. Several problems from the literature were previously shown NP-hard via reductions from those two problems, and by our main result they become PP-hard as well. We also provide complementary PP-upper bounds for some of them.
Topics: Computational Complexity, Computing Research Repository
Source: http://arxiv.org/abs/1501.06729
7
7.0
Jun 30, 2018
06/18
by
Christoph Haase; Stefan Kiefer
texts
eye 7
favorite 0
comment 0
Given Markov chains and Markov decision processes (MDPs) whose transitions are labelled with non-negative integer costs, we study the computational complexity of deciding whether the probability of paths whose accumulated cost satisfies a Boolean combination of inequalities exceeds a given threshold. For acyclic Markov chains, we show that this problem is PP-complete, whereas it is hard for the PosSLP problem and in PSPACE for general Markov chains. Moreover, for acyclic and general MDPs, we...
Topics: Computational Complexity, Discrete Mathematics, Computing Research Repository, Logic in Computer...
Source: http://arxiv.org/abs/1409.8228
36
36
Jun 29, 2018
06/18
by
Christoph Haase; Stefan Kiefer; Markus Lohrey
texts
eye 36
favorite 0
comment 0
A cost Markov chain is a Markov chain whose transitions are labelled with non-negative integer costs. A fundamental problem on this model, with applications in the verification of stochastic systems, is to compute information about the distribution of the total cost accumulated in a run. This includes the probability of large total costs, the median cost, and other quantiles. While expectations can be computed in polynomial time, previous work has demonstrated that the computation of cost...
Topics: Formal Languages and Automata Theory, Discrete Mathematics, Computational Complexity, Computing...
Source: http://arxiv.org/abs/1601.04661
5
5.0
Jun 28, 2018
06/18
by
Dmitry Chistikov; Christoph Haase; Simon Halfon
texts
eye 5
favorite 0
comment 0
We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on them. Those grammars can alternatively be viewed as an extension of communication-free Petri nets. Our main results are that reachability and coverability are inter-reducible and both NP-complete. In particular, this class of commutative grammars enjoys semi-linear reachability sets. We also show that the inclusion...
Topics: Formal Languages and Automata Theory, Computing Research Repository
Source: http://arxiv.org/abs/1511.04893
59
59
Sep 21, 2013
09/13
by
Christoph Haase; Sylvain Schmitz; Philippe Schnoebelen
texts
eye 59
favorite 0
comment 0
We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a priority embedding, a well-quasi-ordering that has not previously been used in well-structured systems. We then show how Priority Channel Systems can compute Fast-Growing...
Source: http://arxiv.org/abs/1301.5500v2
1
1.0
Jan 13, 2022
01/22
by
Michael Blondin; Christoph Haase; Philip Offtermatt
data
eye 1
favorite 0
comment 0
This data set contains a set of benchmark instances for Petri net reachability and coverability, which were used to evaluate the TACAS'21 submission "Directed Reachability for Infinite-State Systems" (preprint available online (https://arxiv.org/abs/2010.07912)). This data set is published in order to allow authors of other tools for reachability in Petri nets to easily obtain a large set of benchmark instances, in particular including many reachability instances. See the enclosed...
Source: https://figshare.com/articles/dataset/Benchmark_Instances_for_Reachability_and_Coverability_in_Petri_Nets/14152007/1
4
4.0
Jun 28, 2018
06/18
by
Michael Blondin; Alain Finkel; Christoph Haase; Serge Haddad
texts
eye 4
favorite 0
comment 0
The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. A cornerstone of our approach is the efficient encoding of a...
Topics: Logic in Computer Science, Formal Languages and Automata Theory, Computing Research Repository
Source: http://arxiv.org/abs/1510.05724
5
5.0
Jun 29, 2018
06/18
by
Stefan Göller; Christoph Haase; Ranko Lazić; Patrick Totzke
texts
eye 5
favorite 0
comment 0
Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so...
Topics: Formal Languages and Automata Theory, Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1602.05547
3
3.0
Jun 30, 2018
06/18
by
Michael Blondin; Alain Finkel; Stefan Göller; Christoph Haase; Pierre McKenzie
texts
eye 3
favorite 0
comment 0
Determining the complexity of the reachability problem for vector addition systems with states (VASS) is a long-standing open problem in computer science. Long known to be decidable, the problem to this day lacks any complexity upper bound whatsoever. In this paper, reachability for two-dimensional VASS is shown PSPACE-complete. This improves on a previously known doubly exponential time bound established by Howell, Rosier, Huynh and Yen in 1986. The coverability and boundedness problems are...
Topics: Computational Complexity, Logic in Computer Science, Computing Research Repository, Formal...
Source: http://arxiv.org/abs/1412.4259
