
We show that any onecounter automaton with $n$ states, if its language is
nonempty, accepts some word of length at most $O(n^2)$. This closes the gap
between the previously known upper bound of $O(n^3)$ and lower bound of
$\Omega(n^2)$. More generally, we prove a tight upper bound on the length of
shortest paths between arbitrary configurations in onecounter transition
systems (weaker bounds have previously appeared in the literature).

Following a recently considered generalization of linear equations to
unordered data vectors, we perform a further generalization to ordered data
vectors. These generalized equations naturally appear in the analysis of vector
addition systems (or Petri nets) extended with ordered data. We show that
nonnegativeinteger solvability of linear equations is computationally
equivalent (up to an exponential blowup) with the reachability problem for
(plain) vector addition systems. This high complexity is surprising, and
contrasts with NPcompleteness for unordered data vectors. Also surprisingly,
we achieve polynomial time complexity of the solvability problem when the
nonnegativeinteger restriction on solutions is dropped.

A vector addition system (VAS) with an initial and a final marking and
transition labels induces a language. In part because the reachability problem
in VAS remains far from being wellunderstood, it is difficult to devise
decision procedures for such languages. This is especially true for checking
properties that state the existence of infinitely many words of a particular
shape. Informally, we call these \emph{unboundedness properties}. We present a
simple set of axioms for predicates that can express unboundedness properties.
Our main result is that such a predicate is decidable for VAS languages as soon
as it is decidable for regular languages. Among other results, this allows us
to show decidability of (i)~separability by bounded regular languages,
(ii)~unboundedness of occurring factors from a language $K$ with mild
conditions on $K$, and (iii)~universality of the set of factors.

We consider averageenergy games, where the goal is to minimize the longrun
average of the accumulated energy. While several results have been obtained on
these games recently, decidability of averageenergy games with a lowerbound
constraint on the energy level (but no upper bound) remained open; in
particular, so far there was no known upper bound on the memory that is
required for winning strategies.
By reducing averageenergy games with lowerbounded energy to infinitestate
meanpayoff games and analyzing the density of lowenergy configurations, we
show an almost tight doublyexponential upper bound on the necessary memory,
and that the winner of averageenergy games with lowerbounded energy can be
determined in doublyexponential time. We also prove EXPSPACEhardness of this
problem.
Finally, we consider multidimensional extensions of all types of
averageenergy games: without bounds, with only a lower bound, and with both a
lower and an upper bound on the energy. We show that the fullybounded version
is the only case to remain decidable in multiple dimensions.

Data vectors generalise finite multisets: they are finitely supported
functions into a commutative monoid. We study the question if a given data
vector can be expressed as a finite sum of others, only assuming that 1) the
domain is countable and 2) the given set of base vectors is finite up to
permutations of the domain.
Based on a succinct representation of the involved permutations as integer
linear constraints, we derive that positive instances can be witnessed in a
bounded subset of the domain.
For data vectors over a group we moreover study when a data vector is
reversible, that is, if its inverse is expressible using only nonnegative
coefficients. We show that if all base vectors are reversible then the
expressibility problem reduces to checking membership in finitely generated
subgroups. Moreover, checking reversibility also reduces to such membership
tests.
These questions naturally appear in the analysis of counter machines extended
with unordered data: namely, for data vectors over $(\mathbb{Z}^d,+)$
expressibility directly corresponds to checking state equations for Coloured
Petri nets where tokens can only be tested for equality. We derive that in this
case, expressibility is in NP, and in P for reversible instances. These upper
bounds are tight: they match the lower bounds for standard integer vectors
(over singleton domains).

Onecounter nets (OCN) are finite automata equipped with a counter that can
store nonnegative integer values, and that cannot be tested for zero.
Equivalently, these are exactly 1dimensional vector addition systems with
states. We show that both strong and weak simulation preorder on OCN are
PSPACEcomplete.

We study the computational and descriptional complexity of the following
transformation: Given a onecounter automaton (OCA) A, construct a
nondeterministic finite automaton (NFA) B that recognizes an abstraction of the
language L(A): its (1) downward closure, (2) upward closure, or (3) Parikh
image.
For the Parikh image over a fixed alphabet and for the upward and downward
closures, we find polynomialtime algorithms that compute such an NFA. For the
Parikh image with the alphabet as part of the input, we find a quasipolynomial
time algorithm and prove a completeness result: we construct a sequence of OCA
that admits a polynomialtime algorithm iff there is one for all OCA.
For all three abstractions, it was previously unknown if appropriate NFA of
subexponential size exist.

We show that the language equivalence problem for regular and contextfree
commutative grammars is coNEXPcomplete. In addition, our lower bound
immediately yields further coNEXPcompleteness results for equivalence problems
for communicationfree Petri nets and reversalbounded counter automata.
Moreover, we improve both lower and upper bounds for language equivalence for
exponentsensitive commutative grammars.

OneCounter nets (OCN) consist of a nondeterministic finite control and a
single integer counter that cannot be fully tested for zero. They form a
natural subclass of both OneCounter Automata, which allow zerotests and Petri
Nets/VASS, which allow multiple such weak counters.
The trace inclusion problem has recently been shown to be undecidable for
OCN. In this paper, we contrast the complexity of two natural restrictions
which imply decidability.
First, we show that trace inclusion between an OCN and a deterministic OCN is
NLcomplete, even with arbitrary binaryencoded initial countervalues as part
of the input. Secondly, we show Ackermannian completeness of for the trace
universality problem of nondeterministic OCN. This problem is equivalent to
checking trace inclusion between a finite and a OCNprocess.

Onecounter nets (OCN) are Petri nets with exactly one unbounded place. They
are equivalent to a subclass of onecounter automata with only a weak test for
zero. We show that weak simulation preorder is decidable for OCN and that weak
simulation approximants do not converge at level omega, but only at omega^2. In
contrast, other semantic relations like weak bisimulation are undecidable for
OCN, and so are weak (and strong) trace inclusion.

Energy games are a wellstudied class of 2player turnbased games on a
finite graph where transitions are labeled with integer vectors which represent
changes in a multidimensional resource (the energy). One player tries to keep
the cumulative changes nonnegative in every component while the other tries to
frustrate this. We consider generalized energy games played on infinite game
graphs induced by pushdown automata (modelling recursion) or their subclass of
onecounter automata. Our main result is that energy games are decidable in the
case where the game graph is induced by a onecounter automaton and the energy
is onedimensional. On the other hand, every further generalization is
undecidable: Energy games on onecounter automata with a 2dimensional energy
are undecidable, and energy games on pushdown automata are undecidable even if
the energy is onedimensional. Furthermore, we show that energy games and
simulation games are interreducible, and thus we additionally obtain several
new (un)decidability results for the problem of checking simulation preorder
between pushdown automata and vector addition systems.

Onecounter nets (OCN) are Petri nets with exactly one unbounded place. They
are equivalent to a subclass of onecounter automata with just a weak test for
zero. Unlike many other semantic equivalences, strong and weak simulation
preorder are decidable for OCN, but the computational complexity was an open
problem. We show that both strong and weak simulation preorder on OCN are
PSPACEcomplete.

This paper is about reachability analysis in a restricted subclass of
multipushdown automata. We assume that the control states of an automaton are
partially ordered, and all transitions of an automaton go downwards with
respect to the order. We prove decidability of the reachability problem, and
computability of the backward reachability set. As the main contribution, we
identify relevant subclasses where the reachability problem becomes
NPcomplete. This matches the complexity of the same problem for
communicationfree vector addition systems, a special case of stateless
multipushdown automata.

This paper explores the well known approximation approach to decide weak
bisimilarity of Basic Parallel Processes. We look into how different refinement
functions can be used to prove weak bisimilarity decidable for certain
subclasses. We also show their limitations for the general case. In particular,
we show a lower bound of {\omega} \ast {\omega} for the approximants which
allow weak steps and a lower bound of {\omega} + {\omega} for the approximants
that allow sequences of actions. The former lower bound negatively answers the
open question of Jan\v{c}ar and Hirshfeld.

Timed automata and register automata are wellknown models of computation
over timed and data words respectively. The former has clocks that allow to
test the lapse of time between two events, whilst the latter includes registers
that can store data values for later comparison. Although these two models
behave in appearance differently, several decision problems have the same
(un)decidability and complexity results for both models. As a prominent
example, emptiness is decidable for alternating automata with one clock or
register, both with nonprimitive recursive complexity. This is not by chance.
This work confirms that there is indeed a tight relationship between the two
models. We show that a run of a timed automaton can be simulated by a register
automaton, and conversely that a run of a register automaton can be simulated
by a timed automaton. Our results allow to transfer complexity and decidability
results back and forth between these two kinds of models. We justify the
usefulness of these reductions by obtaining new results on register automata.