An absent factor of a string $w$ is a string $u$ which does not occur as a
contiguous substring (a.k.a. factor) inside $w$. We extend this well-studied
notion and define absent subsequences: a string $u$ is an absent subsequence of
a string $w$ if $u$ does not occur as subsequence (a.k.a. scattered factor)
inside $w$. Of particular interest to us are minimal absent subsequences, i.e.,
absent subsequences whose every subsequence is not absent, and shortest absent
subsequences, i.e., absent subsequences of minimal length. We show a series of
combinatorial and algorithmic results regarding these two notions. For
instance: we give combinatorial characterisations of the sets of minimal and,
respectively, shortest absent subsequences in a word, as well as compact
representations of these sets; we show how we can test efficiently if a string
is a shortest or minimal absent subsequence in a word, and we give efficient
algorithms computing the lexicographically smallest absent subsequence of each
kind; also, we show how a data structure for answering shortest absent
subsequence-queries for the factors of a given string can be efficiently
computed.
We investigate the complexity of the reachability problem for (deep) neural
networks: does it compute valid output given some valid input? It was recently
claimed that the problem is NP-complete for general neural networks and
specifications over the input/output dimension given by conjunctions of linear
inequalities. We recapitulate the proof and repair some flaws in the original
upper and lower bound proofs. Motivated by the general result, we show that
NP-hardness already holds for restricted classes of simple specifications and
neural networks. Allowing for a single hidden layer and an output dimension of
one as well as neural networks with just one negative, zero and one positive
weight or bias is sufficient to ensure NP-hardness. Additionally, we give a
thorough discussion and outlook of possible extensions for this direction of
research on neural network verification.
Synthesis consists in deciding whether a given labeled transition system (TS)
$A$ can be implemented by a net $N$ of type $\tau$. In case of a negative
decision, it may be possible to convert $A$ into an implementable TS $B$ by
applying various modification techniques, like relabeling edges that previously
had the same label, suppressing edges/states/events, etc. It may however be
useful to limit the number of such modifications to stay close to the original
problem, or optimize the technique. In this paper, we show that most of the
corresponding problems are NP-complete if $\tau$ corresponds to the type of
flip-flop nets or some flip-flop net derivatives.
Colored Petri nets offer a compact and user friendly representation of the
traditional P/T nets and colored nets with finite color ranges can be unfolded
into the underlying P/T nets, however, at the expense of an exponential
explosion in size. We present two novel techniques based on static analysis in
order to reduce the size of unfolded colored nets. The first method identifies
colors that behave equivalently and groups them into equivalence classes,
potentially reducing the number of used colors. The second method
overapproximates the sets of colors that can appear in places and excludes
colors that can never be present in a given place. Both methods are
complementary and the combined approach allows us to significantly reduce the
size of multiple colored Petri nets from the Model Checking Contest benchmark.
We compare the performance of our unfolder with state-of-the-art techniques
implemented in the tools MCC, Spike and ITS-Tools, and while our approach is
competitive w.r.t. unfolding time, it also outperforms the existing approaches
both in the size of unfolded nets as well as in the number of answered model
checking queries from the 2021 Model Checking Contest.