arXiv subjects

Filip Mazowiecki

Publications and source records attributed to Filip Mazowiecki.

At least 19 recordsLinked to original sources

arXiv2026

Representing One Letter Weighted Automata Over the Tropical Semiring

We consider weighted automata over the tropical semiring $\mathbb{Z}_\infty(min, +)$. Recently, it was shown that determinisation is decidable; in this paper we focus on the complexity when the alphabet is unary. In 2001, Lombardy showed this problem is decidable, a close inspection of his proof yields a coNP upper bound on the complexity. Earlier Gaubert showed that every weighted automaton in this setting can be effectively turned into an equivalent union of deterministic weighted automata. We prove Gaubert's result efficiently, presenting it as a generalisation of Chrobak's normal form for unary NFA. In particular, we prove that the equivalent union of deterministic weighted automata can be represented by a weighted automaton of quadratic size in the size of the original one, and this representation can be computed in polynomial time. Building on this, we show that determinisation, and even register minimisation (which generalises determinisation), is coNP-complete. We complete the paper with observations that the boundedness problem is also coNP-complete by reductions with determinisation. Lastly, we provide evidence that all of these problems are not FPT (by proving $coW_1$-hardness) when parametrised by the number of deterministic automata in the union.

cs.FL↗

arXiv2025

Soundness of reset workflow nets

Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability was shown decades ago, but their complexity was only identified recently. In this work, we are primarily interested in two popular variants: $1$-soundness and generalised soundness. Workflow nets have been extended with resets to model workflows that can, e.g., cancel actions. It has been known for a while that, for this extension, all variants of soundness, except possibly generalised soundness, are undecidable. We complete the picture by showing that generalised soundness is also undecidable for reset workflow nets. We then blur this undecidability landscape by identifying a property, coined ``$1$-in-between soundness'', which lies between $1$-soundness and generalised soundness. It reveals an unusual non-monotonic complexity behaviour: a decidable soundness property is in between two undecidable ones. This can be valuable in the algorithmic analysis of reset workflow nets, as our procedure yields an output of the form ``$1$-sound'' or ``not generalised sound'' which is always correct.

cs.FL↗

arXiv2025

Pumping-Like Results for Copyless Cost Register Automata and Polynomially Ambiguous Weighted Automata

In this work we consider two rich subclasses of weighted automata over fields: polynomially ambiguous weighted automata and copyless cost register automata. Primarily we are interested in understanding their expressiveness power. Over the field of rationals and $1$-letter alphabets, it is known that the two classes coincide; they are equivalent to linear recurrence sequences (LRS) whose exponential bases are roots of rationals. We develop a tool we call Pumping Sequence Families, which, by exploiting the simple single-letter behaviour of the models, yields two pumping-like results over arbitrary fields with unrestricted alphabets, one for each class. As a corollary of these results, we present examples proving that the two classes become incomparable over the field of rationals with unrestricted alphabets. We complement the results by analysing the zeroness and equivalence problems. For weighted automata (even unrestricted) these problems are well understood: there are polynomial time, and even NC$^2$ algorithms. For copyless cost register automata we show that the two problems are \textsc{PSpace}-complete, where the difficulty is to show the lower bound.

cs.FL↗

arXiv2025

Fine-Grained Complexity of Ambiguity Problems on Automata and Directed Graphs

In the field of computational logic, two classes of finite automata are considered fundamental: deterministic and nondeterministic automata (DFAs and NFAs). In a more fine-grained approach three natural intermediate classes were introduced, defined by restricting the number of accepting runs of the input NFA. The classes are called: unambiguous, finitely ambiguous, and polynomially ambiguous finite automata. It was observed that central problems, like equivalence, become tractable when the input NFA is restricted to some of these classes. This naturally brought interest into problems determining whether an input NFA belongs to the intermediate classes. Our first result is a nearly complete characterization of the fine-grained complexity of these problems. We show that the respective quadratic and cubic running times of Allauzen et al. are optimal under the Orthogonal Vectors hypothesis or the k-Cycle hypothesis, for alphabets with at least two symbols. In contrast, for unary alphabets we show that all aforementioned variants of ambiguity can be decided in almost linear time. Finally, we study determinisability of unambiguous weighted automata. We positively resolve a conjecture of Allauzen and Mohri, proving that their quadratic-time algorithm for verifying determinisability of unambiguous weighted automata is optimal, assuming the Orthogonal Vectors hypothesis or the k-Cycle hypothesis. We additionally show that for unary alphabets, this can be decided in linear time.

cs.FL↗

arXiv2024

The Tractability Border of Reachability in Simple Vector Addition Systems with States

Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. The central algorithmic challenge in VASS is the reachability problem: is there a run from a given starting state and counter values to a given target state and counter values? When the input is encoded in binary, reachability is computationally intractable: even in dimension one, it is NP-hard. In this paper, we comprehensively characterise the tractability border of the problem when the input is encoded in unary. For our main result, we prove that reachability is NP-hard in unary encoded 3-VASS, even when structure is heavily restricted to be a simple linear path scheme. This improves upon a recent result of Czerwi\'nski and Orlikowski (2022), in both the number of counters and expressiveness of the considered model, as well as answers open questions of Englert, Lazi\'c, and Totzke (2016) and Leroux (2021). The underlying graph structure of a simple linear path scheme (SLPS) is just a path with self-loops at each node. We also study the exceedingly weak model of computation that is SPLS with counter updates in {-1,0,+1}. Here, we show that reachability is NP-hard when the dimension is bounded by O(\alpha(k)), where \alpha is the inverse Ackermann function and k bounds the size of the SLPS. We complement our result by presenting a polynomial-time algorithm that decides reachability in 2-SLPS when the initial and target configurations are specified in binary. To achieve this, we show that reachability in such instances is well-structured: all loops, except perhaps for a constant number, are taken either polynomially many times or almost maximally. This extends the main result of Englert, Lazi\'c, and Totzke (2016) who showed the problem is in NL when the initial and target configurations are specified in unary.

cs.FL↗

arXiv2023

Acyclic Petri and Workflow Nets with Resets

In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition that only applies to the consumptions and productions, not the resets. The first class is acyclic Petri nets with resets, and we show that coverability is PSPACE-complete for them. This contrasts the known Ackermann-hardness for coverability in (not necessarily acyclic) Petri nets with resets. We prove that the reachability problem remains undecidable for acyclic Petri nets with resets. The second class concerns workflow nets, a practically motivated and natural subclass of Petri nets. Here, we show that both coverability and reachability in acyclic workflow nets with resets are PSPACE-complete. Without the acyclicity condition, reachability and coverability in workflow nets with resets are known to be equally hard as for Petri nets with resets, that being Ackermann-hard and undecidable, respectively.

cs.FL↗

arXiv2023

Determinisation and Unambiguisation of Polynomially-Ambiguous Rational Weighted Automata

We study the determinisation and unambiguisation problems of weighted automata over the rational field: Given a weighted automaton, can we determine whether there exists an equivalent deterministic, respectively unambiguous, weighted automaton? Recent results by Bell and Smertnig show that the problem is decidable, however they do not provide any complexity bounds. We show that both problems are in PSPACE for polynomially-ambiguous weighted automata.

cs.FL↗

arXiv2023

Monus semantics in vector addition systems with states

Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometimes useful to consider overapproximating semantics in which these problems can be decided more efficiently. We study an overapproximation, called monus semantics, that slightly relaxes the semantics of decrements: A key property of a vector addition systems is that in order to decrement a counter, this counter must have a positive value. In contrast, our semantics allows decrements of zero-valued counters: If such a transition is executed, the counter just remains zero. It turns out that if only a subset of transitions is used with monus semantics (and the others with classical semantics), then reachability is undecidable. However, we show that if monus semantics is used throughout, reachability remains decidable. In particular, we show that reachability for VASS with monus semantics is as hard as that of classical VASS (i.e. Ackermann-hard), while the zero-reachability and coverability are easier (i.e. EXPSPACE-complete and NP-complete, respectively). We provide a comprehensive account of the complexity of the general reachability problem, reachability of zero configurations, and coverability under monus semantics. We study these problems in general VASS, two-dimensional VASS, and one-dimensional VASS, with unary and binary counter updates.

cs.LO↗

arXiv2023

Coverability in VASS Revisited: Improving Rackoff's Bound to Obtain Conditional Optimality

Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodings (Lipton, '76). More precisely, Rosier and Yen later utilise Rackoff's bounding technique to show that if coverability holds then there is a run of length at most $n^{2^{\mathcal{O}(d \log d)}}$, where $d$ is the dimension and $n$ is the size of the given unary VASS. Earlier, Lipton showed that there exist instances of coverability in $d$-dimensional unary VASS that are only witnessed by runs of length at least $n^{2^{Ω(d)}}$. Our first result closes this gap. We improve the upper bound by removing the twice-exponentiated $\log(d)$ factor, thus matching Lipton's lower bound. This closes the corresponding gap for the exact space required to decide coverability. This also yields a deterministic $n^{2^{\mathcal{O}(d)}}$-time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic $n^{2^{o(d)}}$-time algorithm, conditioned upon the Exponential Time Hypothesis. When analysing coverability, a standard proof technique is to consider VASS with bounded counters. Bounded VASS make for an interesting and popular model due to strong connections with timed automata. Withal, we study a natural setting where the counter bound is linear in the size of the VASS. Here the trivial exhaustive search algorithm runs in $\mathcal{O}(n^{d+1})$-time. We give evidence to this being near-optimal. We prove that in dimension one this trivial algorithm is conditionally optimal, by showing that $n^{2-o(1)}$-time is required under the $k$-cycle hypothesis. In general fixed dimension $d$, we show that $n^{d-2-o(1)}$-time is required under the 3-uniform hyperclique hypothesis.

cs.FL↗

arXiv2023

Coverability in 2-VASS with One Unary Counter is in NP

Coverability in Petri nets finds applications in verification of safety properties of reactive systems. We study coverability in the equivalent model: Vector Addition Systems with States (VASS). A k-VASS can be seen as k counters and a finite automaton whose transitions are labelled with k integers. Counter values are updated by adding the respective transition labels. A configuration in this system consists of a state and k counter values. Importantly, the counters are never allowed to take negative values. The coverability problem asks whether one can traverse the k-VASS from the initial configuration to a configuration with at least the counter values of the target. In a well-established line of work on k-VASS, coverability in 2-VASS is already PSPACE-hard when the integer updates are encoded in binary. This lower bound limits the practicality of applications, so it is natural to focus on restrictions. In this paper we initiate the study of 2-VASS with one unary counter. Here, one counter receives binary encoded updates and the other receives unary encoded updates. Our main result is that coverability in 2-VASS with one unary counter is in NP. This improves upon the inherited state-of-the-art PSPACE upper bound. Our main technical contribution is that one only needs to consider runs in a certain compressed linear form.

cs.FL↗

arXiv2022

On Rational Recursive Sequences

We study the class of rational recursive sequences (ratrec) over the rational numbers. A ratrec sequence is defined via a system of sequences using mutually recursive equations of depth 1, where the next values are computed as rational functions of the previous values. An alternative class is that of simple ratrec sequences, where one uses a single recursive equation, however of depth k: the next value is defined as a rational function of k previous values. We conjecture that the classes ratrec and simple ratrec coincide. The main contribution of this paper is a proof of a variant of this conjecture where the initial conditions are treated symbolically, using a formal variable per sequence, while the sequences themselves consist of rational functions over those variables. While the initial conjecture does not follow from this variant, we hope that the introduced algebraic techniques may eventually be helpful in resolving the problem. The class ratrec strictly generalises a well-known class of polynomial recursive sequences (polyrec). These are defined like ratrec, but using polynomial functions instead of rational ones. One can observe that if our conjecture is true and effective, then we can improve the complexities of the zeroness and the equivalence problems for polyrec sequences. Currently, the only known upper bound is Ackermanian, which follows from results on polynomial automata. We complement this observation by proving a PSPACE lower bound for both problems for polyrec. Our lower bound construction also implies that the Skolem problem is PSPACE-hard for the polyrec class.

cs.FL↗

arXiv2022

Verifying generalised and structural soundness of workflow nets via relaxations

Workflow nets are a well-established mathematical formalism for the analysis of business processes arising from either modeling tools or process mining. The central decision problems for workflow nets are $k$-soundness, generalised soundness and structural soundness. Most existing tools focus on $k$-soundness. In this work, we propose novel scalable semi-procedures for generalised and structural soundness. This is achieved via integral and continuous Petri net reachability relaxations. We show that our approach is competitive against state-of-the-art tools.

cs.LO↗

arXiv2022

The boundedness and zero isolation problems for weighted automata over nonnegative rationals

We consider linear cost-register automata (equivalent to weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems of boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and to zero, respectively. In the general model both problems are undecidable so we focus on the copyless linear restriction. There, we show that the boundedness problem is decidable. As for the zero isolation problem we need to further restrict the class. We obtain a model, where zero isolation becomes equivalent to universal coverability of orthant vector addition systems (OVAS), a new model in the VAS family interesting on its own. In standard VAS runs are considered only in the positive orthant, while in OVAS every orthant has its own set of vectors that can be applied in that orthant. Assuming Schanuel's conjecture is true, we prove decidability of universal coverability for three-dimensional OVAS, which implies decidability of zero isolation in a model with at most three independent registers.

cs.FL↗

arXiv2022

The complexity of soundness in workflow nets

Workflow nets are a popular variant of Petri nets that allow for algorithmic formal analysis of business processes. The central decision problems concerning workflow nets deal with soundness, where the initial and final configurations are specified. Intuitively, soundness states that from every reachable configuration one can reach the final configuration. We settle the widely open complexity of the three main variants of soundness: classical, structural and generalised soundness. The first two are EXPSPACE-complete, and, surprisingly, the latter is PSPACE-complete, thus computationally simpler.

cs.LO↗

arXiv2021

Pumping lemmas for weighted automata

We present pumping lemmas for five classes of functions definable by fragments of weighted automata over the min-plus semiring, the max-plus semiring and the semiring of natural numbers. As a corollary we show that the hierarchy of functions definable by unambiguous, finitely-ambiguous, polynomially-ambiguous weighted automata, and the full class of weighted automata is strict for the min-plus and max-plus semirings.

cs.LO↗

arXiv2021

Affine Extensions of Integer Vector Addition Systems with States

We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine $\mathbb{Z}$-VASS with the finite-monoid property (afmp-$\mathbb{Z}$-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-$\mathbb{Z}$-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-$\mathbb{Z}$-VASS reduces to reachability in a $\mathbb{Z}$-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-$\mathbb{Z}$-VASS are semilinear, and in particular enables us to show that reachability in $\mathbb{Z}$-VASS with transfers and $\mathbb{Z}$-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine $\mathbb{Z}$-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine $\mathbb{Z}$-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine $\mathbb{Z}$-VASS with monogenic matrix monoid and undecidable reachability relation.

cs.LO↗

arXiv2021

Continuous One-Counter Automata

We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is decidable in the polynomial hierarchy for COCA with parametric counter updates and bound tests.

cs.FL↗

arXiv2020

Reachability in fixed dimension vector addition systems with states

The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional VASS. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14.

cs.FL↗