Fundamenta Informaticae - Volume 189, issue 3-4

Authors: Bell, Paul C. | Potapov, Igor | Schmitz, Sylvain | Totzke, Patrick

Article Type: Other

DOI: 10.3233/FI-222158

Citation: Fundamenta Informaticae, vol. 189, no. 3-4, pp. i-iii, 2022

Authors: Kosche, Maria | Koß, Tore | Manea, Florin | Siemer, Stefan

Article Type: Research Article

Abstract: 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. Show more

Keywords: Absent subsequence, Arch-factorization, Stringology, Subsequence, Subsequence-Universality

DOI: 10.3233/FI-222159

Citation: Fundamenta Informaticae, vol. 189, no. 3-4, pp. 199-240, 2022

Authors: Sälzer, Marco | Lange, Martin

Article Type: Research Article

Abstract: 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. Show more

Keywords: machine learning, computational complexity, formal specification and verification

DOI: 10.3233/FI-222160

Citation: Fundamenta Informaticae, vol. 189, no. 3-4, pp. 241-259, 2022

Authors: Devillers, Raymond | Tredup, Ronny

Article Type: Research Article

Abstract: Let us consider some class of (Petri) nets. The corresponding Synthesis problem consists in deciding whether a given labeled transition system (TS) A can be implemented by a net N of that class. 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 the considered class corresponds to so-called flip-flop nets or some flip-flop net derivatives. Show more

Keywords: Petri net, Boolean Types, Label-Splitting, Edge-Removal, Event-Removal, State-Removal, Synthesis, Complexity

DOI: 10.3233/FI-222161

Citation: Fundamenta Informaticae, vol. 189, no. 3-4, pp. 261-296, 2022

Authors: Bilgram, Alexander | Jensen, Peter G. | Pedersen, Thomas | Srba, Jiří | Taankvist, Peter H.

Article Type: Research Article

Abstract: Colored Petri nets offer a compact and user friendly representation of the traditional Place/Transition (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. Show more

DOI: 10.3233/FI-222162

Citation: Fundamenta Informaticae, vol. 189, no. 3-4, pp. 297-320, 2022