95 results on '"Mazowiecki, Filip"'
Search Results
2. Acyclic Petri and Workflow Nets with Resets
- Author
-
Chistikov, Dmitry, Czerwiński, Wojciech, Hofman, Piotr, Mazowiecki, Filip, and Sinclair-Banks, Henry
- Subjects
Computer Science - Formal Languages and Automata Theory ,Computer Science - Logic in Computer Science - Abstract
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., Comment: Preprint for FSTTCS'23 containing 28 pages and 7 figures
- Published
- 2023
3. Monus semantics in vector addition systems with states
- Author
-
Baumann, Pascal, Madnani, Khushraj, Mazowiecki, Filip, and Zetzsche, Georg
- Subjects
Computer Science - Logic in Computer Science ,Computer Science - Formal Languages and Automata Theory - Abstract
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.
- Published
- 2023
4. Coverability in VASS Revisited: Improving Rackoff's Bound to Obtain Conditional Optimality
- Author
-
Künnemann, Marvin, Mazowiecki, Filip, Schütze, Lia, Sinclair-Banks, Henry, and Węgrzycki, Karol
- Subjects
Computer Science - Formal Languages and Automata Theory ,Computer Science - Computational Complexity - Abstract
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^{\Omega(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., Comment: Preprint for ICALP'23 containing 25 pages and 10 figures
- Published
- 2023
5. Coverability in 2-VASS with One Unary Counter is in NP
- Author
-
Mazowiecki, Filip, Sinclair-Banks, Henry, and Węgrzycki, Karol
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
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., Comment: Preprint for FoSSaCS'23 containing 20 pages and 7 figures
- Published
- 2023
6. On Rational Recursive Sequences
- Author
-
Clemente, Lorenzo, Donten-Bury, Maria, Mazowiecki, Filip, and Pilipczuk, Michał
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
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.
- Published
- 2022
7. Verifying generalised and structural soundness of workflow nets via relaxations
- Author
-
Blondin, Michael, Mazowiecki, Filip, and Offtermatt, Philip
- Subjects
Computer Science - Logic in Computer Science - Abstract
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., Comment: Accepted at CAV 2022
- Published
- 2022
8. The boundedness and zero isolation problems for weighted automata over nonnegative rationals
- Author
-
Czerwiński, Wojciech, Lefaucheux, Engel, Mazowiecki, Filip, Purser, David, and Whiteland, Markus A.
- Subjects
Computer Science - Formal Languages and Automata Theory ,Computer Science - Logic in Computer Science - Abstract
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., Comment: Full versions of the LICS 2022 paper
- Published
- 2022
9. The complexity of soundness in workflow nets
- Author
-
Blondin, Michael, Mazowiecki, Filip, and Offtermatt, Philip
- Subjects
Computer Science - Logic in Computer Science - Abstract
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., Comment: 16 pages, 6 figures
- Published
- 2022
10. Fast Termination and Workflow Nets
- Author
-
Hofman, Piotr, Mazowiecki, Filip, Offtermatt, Philip, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Enea, Constantin, editor, and Lal, Akash, editor
- Published
- 2023
- Full Text
- View/download PDF
11. Continuous One-Counter Automata
- Author
-
Blondin, Michael, Leys, Tim, Mazowiecki, Filip, Offtermatt, Philip, and Pérez, Guillermo A.
- Subjects
Computer Science - Formal Languages and Automata Theory ,Computer Science - Logic in Computer Science - Abstract
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.
- Published
- 2021
12. Let's Agree to Degree: Comparing Graph Convolutional Networks in the Message-Passing Framework
- Author
-
Geerts, Floris, Mazowiecki, Filip, and Pérez, Guillermo A.
- Subjects
Computer Science - Machine Learning ,Statistics - Machine Learning - Abstract
In this paper we cast neural networks defined on graphs as message-passing neural networks (MPNNs) in order to study the distinguishing power of different classes of such models. We are interested in whether certain architectures are able to tell vertices apart based on the feature labels given as input with the graph. We consider two variants of MPNNS: anonymous MPNNs whose message functions depend only on the labels of vertices involved; and degree-aware MPNNs in which message functions can additionally use information regarding the degree of vertices. The former class covers a popular formalisms for computing functions on graphs: graph neural networks (GNN). The latter covers the so-called graph convolutional networks (GCNs), a recently introduced variant of GNNs by Kipf and Welling. We obtain lower and upper bounds on the distinguishing power of MPNNs in terms of the distinguishing power of the Weisfeiler-Lehman (WL) algorithm. Our results imply that (i) the distinguishing power of GCNs is bounded by the WL algorithm, but that they are one step ahead; (ii) the WL algorithm cannot be simulated by "plain vanilla" GCNs but the addition of a trade-off parameter between features of the vertex and those of its neighbours (as proposed by Kipf and Welling themselves) resolves this problem., Comment: 22 pages
- Published
- 2020
13. On polynomial recursive sequences
- Author
-
Cadilhac, Michaël, Mazowiecki, Filip, Paperman, Charles, Pilipczuk, Michał, and Sénizergues, Géraud
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
We study the expressive power of polynomial recursive sequences, a nonlinear extension of the well-known class of linear recursive sequences. These sequences arise naturally in the study of nonlinear extensions of weighted automata, where (non)expressiveness results translate to class separations. A typical example of a polynomial recursive sequence is b_n=n!. Our main result is that the sequence u_n=n^n is not polynomial recursive.
- Published
- 2020
14. The monitoring problem for timed automata
- Author
-
Grez, Alejandro, Mazowiecki, Filip, Pilipczuk, Michał, Puppis, Gabriele, and Riveros, Cristian
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
We study a variant of the classical membership problem in automata theory, which consists of deciding whether a given input word is accepted by a given automaton. We do so under a different perspective, that is, we consider a dynamic version of the problem, called monitoring problem, where the automaton is fixed and the input is revealed as in a stream, one symbol at a time following the natural order on positions. The goal here is to design a dynamic data structure that can be queried about whether the word consisting of symbols revealed so far is accepted by the automaton, and that can be efficiently updated when the next symbol is revealed. We provide complexity bounds for this monitoring problem, by considering timed automata that process symbols interleaved with timestamps. The main contribution is that monitoring of a one-clock timed automaton, with all its components but the clock constants fixed, can be done in amortised constant time per input symbol.
- Published
- 2020
15. Pumping lemmas for weighted automata
- Author
-
Chattopadhyay, Agnishom, Mazowiecki, Filip, Muscholl, Anca, and Riveros, Cristian
- Subjects
Computer Science - Logic in Computer Science - Abstract
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.
- Published
- 2020
- Full Text
- View/download PDF
16. Reachability in fixed dimension vector addition systems with states
- Author
-
Czerwiński, Wojciech, Lasota, Sławomir, Lazić, Ranko, Leroux, Jérôme, and Mazowiecki, Filip
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
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.
- Published
- 2020
17. Dynamic Data Structures for Timed Automata Acceptance
- Author
-
Grez, Alejandro, Mazowiecki, Filip, Pilipczuk, Michał, Puppis, Gabriele, and Riveros, Cristian
- Published
- 2022
- Full Text
- View/download PDF
18. Affine Extensions of Integer Vector Addition Systems with States
- Author
-
Blondin, Michael, Haase, Christoph, Mazowiecki, Filip, and Raskin, Mikhail
- Subjects
Computer Science - Logic in Computer Science ,Computer Science - Computational Complexity - Abstract
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.
- Published
- 2019
- Full Text
- View/download PDF
19. A Robust Class of Linear Recurrence Sequences
- Author
-
Barloy, Corentin, Fijalkow, Nathanaël, Lhote, Nathan, and Mazowiecki, Filip
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
We introduce a subclass of linear recurrence sequences which we call poly-rational sequences because they are denoted by rational expressions closed under sum and product. We show that this class is robust by giving several characterisations: polynomially ambiguous weighted automata, copyless cost-register automata, rational formal series, and linear recurrence sequences whose eigenvalues are roots of rational numbers.
- Published
- 2019
20. Coverability in 2-VASS with One Unary Counter is in NP
- Author
-
Mazowiecki, Filip, primary, Sinclair-Banks, Henry, additional, and Węgrzycki, Karol, additional
- Published
- 2023
- Full Text
- View/download PDF
21. Reachability for Bounded Branching VASS
- Author
-
Mazowiecki, Filip and Pilipczuk, Michał
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
In this paper we consider the reachability problem for bounded branching VASS. Bounded VASS are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. This model gained a lot of attention in 2012 when Haase et al. showed its connections with timed automata. Later in 2013 Fearnley and Jurdzi\'{n}ski proved that the reachability problem in this model is PSPACE-complete even in dimension 1. Here, we investigate the complexity of the reachability problem when the model is extended with branching transitions, and we prove that the problem is EXPTIME-complete when the dimension is 2 or larger.
- Published
- 2019
22. The Reachability Problem for Petri Nets is Not Elementary
- Author
-
Czerwinski, Wojciech, Lasota, Slawomir, Lazic, Ranko, Leroux, Jerome, and Mazowiecki, Filip
- Subjects
Computer Science - Formal Languages and Automata Theory ,Computer Science - Logic in Computer Science - Abstract
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. Decidability was proved by Mayr in his seminal STOC 1981 work, and the currently best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from LICS 2019. We establish a non-elementary lower bound, i.e. that the reachability problem needs a tower of exponentials of time and space. Until this work, the best lower bound has been exponential space, due to Lipton in 1976. The new lower bound is a major breakthrough for several reasons. Firstly, it shows that the reachability problem is much harder than the coverability (i.e., state reachability) problem, which is also ubiquitous but has been known to be complete for exponential space since the late 1970s. Secondly, it implies that a plethora of problems from formal languages, logic, concurrent systems, process calculi and other areas, that are known to admit reductions from the Petri nets reachability problem, are also not elementary. Thirdly, it makes obsolete the currently best lower bounds for the reachability problems for two key extensions of Petri nets: with branching and with a pushdown stack., Comment: Final version of STOC'19
- Published
- 2018
23. A robust class of linear recurrence sequences
- Author
-
Barloy, Corentin, Fijalkow, Nathanaël, Lhote, Nathan, and Mazowiecki, Filip
- Published
- 2022
- Full Text
- View/download PDF
24. When is Containment Decidable for Probabilistic Automata?
- Author
-
Daviaud, Laure, Jurdziński, Marcin, Lazić, Ranko, Mazowiecki, Filip, Pérez, Guillermo A., and Worrell, James
- Subjects
Computer Science - Formal Languages and Automata Theory ,F.3.1 - Abstract
The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean automata. It is well known that both problems are undecidable. In this paper we provide a more refined view of these problems in terms of the degree of ambiguity of probabilistic automata. We show that a gap version of the emptiness problem (that is known be undecidable in general) becomes decidable for automata of polynomial ambiguity. We complement this positive result by showing that the emptiness problem remains undecidable even when restricted to automata of linear ambiguity. We then turn to finitely ambiguous automata. Here we show decidability of containment in case one of the automata is assumed to be unambiguous while the other one is allowed to be finitely ambiguous. Our proof of this last result relies on the decidability of the theory of real exponentiation, which has been shown, subject to Schanuel's Conjecture, by Macintyre and Wilkie.
- Published
- 2018
25. Weak Cost Register Automata are Still Powerful
- Author
-
Almagor, Shaull, Cadilhac, Michaël, Mazowiecki, Filip, and Pérez, Guillermo A.
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
We consider one of the weakest variants of cost register automata over a tropical semiring, namely copyless cost register automata over $\mathbb{N}$ with updates using $\min$ and increments. We show that this model can simulate, in some sense, the runs of counter machines with zero-tests. We deduce that a number of problems pertaining to that model are undecidable, in particular equivalence, disproving a conjecture of Alur et al. from 2012. To emphasize how weak these machines are, we also show that they can be expressed as a restricted form of linearly-ambiguous weighted automata., Comment: 16 pages
- Published
- 2018
26. Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations
- Author
-
Blondin, Michael, primary, Mazowiecki, Filip, additional, and Offtermatt, Philip, additional
- Published
- 2022
- Full Text
- View/download PDF
27. On Polynomial Recursive Sequences
- Author
-
Cadilhac, Michaël, Mazowiecki, Filip, Paperman, Charles, Pilipczuk, Michał, and Sénizergues, Géraud
- Published
- 2021
- Full Text
- View/download PDF
28. Eliminating Recursion from Monadic Datalog Programs on Trees
- Author
-
Mazowiecki, Filip, Ochremiak, Joanna, and Witkowski, Adam
- Subjects
Computer Science - Logic in Computer Science ,Computer Science - Databases - Abstract
We study the problem of eliminating recursion from monadic datalog programs on trees with an infinite set of labels. We show that the boundedness problem, i.e., determining whether a datalog program is equivalent to some nonrecursive one is undecidable but the decidability is regained if the descendant relation is disallowed. Under similar restrictions we obtain decidability of the problem of equivalence to a given nonrecursive program. We investigate the connection between these two problems in more detail.
- Published
- 2015
29. Copyless Cost-Register Automata: Structure, Expressiveness, and Closure Properties
- Author
-
Mazowiecki, Filip and Riveros, Cristian
- Subjects
Computer Science - Formal Languages and Automata Theory - Abstract
Cost register automata (CRA) and its subclass, copyless CRA, were recently proposed by Alur et al. as a new model for computing functions over strings. We study some structural properties, expressiveness, and closure properties of copyless CRA. We show that copyless CRA are strictly less expressive than weighted automata and are not closed under reverse operation. To find a better class we impose restrictions on copyless CRA, which ends successfully with a new robust computational model that is closed under reverse and other extensions.
- Published
- 2015
30. Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees
- Author
-
Charatonik, Witold, Kieroński, Emanuel, and Mazowiecki, Filip
- Subjects
Computer Science - Logic in Computer Science - Abstract
We consider the satisfiability problem for the two-variable fragment of first-order logic over finite unranked trees. We work with signatures consisting of some unary predicates and the binary navigational predicates child, right sibling, and their respective transitive closures. We prove that the satisfiability problem for the logic containing all these predicates is EXPSPACE-complete. Further, we consider the restriction of the class of structures to singular trees, i.e., we assume that at every node precisely one unary predicate holds. We observe that the full logic and even for unordered trees remain EXPSPACE-complete over finite singular trees, but the complexity decreases for some weaker logics. Namely, the logic with one binary predicate, descendant is NEXPTIME-complete, and its guarded version is PSPACE-complete over finite singular trees, even though both these logics are EXPSPACE-complete over arbitrary finite trees.
- Published
- 2013
31. Continuous One-counter Automata
- Author
-
Blondin, Michael, primary, Leys, Tim, additional, Mazowiecki, Filip, additional, Offtermatt, Philip, additional, and Pérez, Guillermo, additional
- Published
- 2023
- Full Text
- View/download PDF
32. On Rational Recursive Sequences
- Author
-
Clemente, Lorenzo, Donten-Bury, Maria, Mazowiecki, Filip, and Pilipczuk, Michał
- Subjects
FOS: Computer and information sciences ,Formal Languages and Automata Theory (cs.FL) ,Theory of computation → Formal languages and automata theory ,equivalence problem ,Computer Science - Formal Languages and Automata Theory ,zeroness problem ,recursive sequences ,polynomial automata - Abstract
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., LIPIcs, Vol. 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023), pages 24:1-24:21
- Published
- 2023
- Full Text
- View/download PDF
33. Monadic Datalog and Regular Tree Pattern Queries
- Author
-
Mazowiecki, Filip, Murlak, Filip, Witkowski, Adam, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Csuhaj-Varjú, Erzsébet, editor, Dietzfelbinger, Martin, editor, and Ésik, Zoltán, editor
- Published
- 2014
- Full Text
- View/download PDF
34. Weak Cost Register Automata Are Still Powerful
- Author
-
Almagor, Shaull, primary, Cadilhac, Michaël, additional, Mazowiecki, Filip, additional, and Pérez, Guillermo A., additional
- Published
- 2018
- Full Text
- View/download PDF
35. The boundedness and zero isolation problems for weighted automata over nonnegative rationals
- Author
-
Czerwiński, Wojciech, primary, Lefaucheux, Engel, additional, Mazowiecki, Filip, additional, Purser, David, additional, and Whiteland, Markus, additional
- Published
- 2022
- Full Text
- View/download PDF
36. The complexity of soundness in workflow nets
- Author
-
Blondin, Michael, primary, Mazowiecki, Filip, additional, and Offtermatt, Philip, additional
- Published
- 2022
- Full Text
- View/download PDF
37. The Reachability Problem for Petri Nets Is Not Elementary.
- Author
-
CZERWIŃSKI, WOJCIECH, LASOTA, SŁAWOMIR, LAZIĆ, RANKO, LEROUX, JÉRÔME, and MAZOWIECKI, FILIP
- Subjects
PETRI nets ,COMPUTER logic ,DATABASES ,COMPUTER science ,FORMAL languages - Abstract
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modeling and analysis of hardware, software, and database systems, as well as chemical, biological, and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. Decidability was proved by Mayr in his seminal STOC 1981 work, and, currently, the best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from Symposium on Logic in Computer Science 2019. We establish a non-elementary lower bound, i.e., that the reachability problem needs a tower of exponentials of time and space. Until this work, the best lower bound has been exponential space, due to Lipton in 1976. The new lower bound is a major breakthrough for several reasons. Firstly, it shows that the reachability problem is much harder than the coverability (i.e., state reachability) problem, which is also ubiquitous but has been known to be complete for exponential space since the late 1970s. Secondly, it implies that a plethora of problems from formal languages, logic, concurrent systems, process calculi, and other areas, which are known to admit reductions from the Petri nets reachability problem, are also not elementary. Thirdly, it makes obsolete the current best lower bounds for the reachability problems for two key extensions of Petri nets: with branching and with a pushdown stack. We develop a construction that uses arbitrarily large pairs of values with ratio R to provide zero testable counters that are bounded by R. At the heart of our proof is then a novel gadget, the so-called factorial amplifier that, assuming availability of counters that are zero testable and bounded by k, guarantees to produce arbitrarily large pairs of values whose ratio is exactly the factorial of k. Repeatedly composing the factorial amplifier with itself by means of the former construction enables us to compute, in linear time, Petri nets that simulate Minsky machines whose counters are bounded by a tower of exponentials, which yields the non-elementary lower bound. By refining this scheme further, we, in fact, already establish hardness for h-exponential space for Petri nets with h + 13 counters. [ABSTRACT FROM AUTHOR]
- Published
- 2021
- Full Text
- View/download PDF
38. Complexity of Two-Variable Logic on Finite Trees
- Author
-
Benaim, Saguy, Benedikt, Michael, Charatonik, Witold, Kieroński, Emanuel, Lenhardt, Rastislav, Mazowiecki, Filip, Worrell, James, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Fomin, Fedor V., editor, Freivalds, Rūsiņš, editor, Kwiatkowska, Marta, editor, and Peleg, David, editor
- Published
- 2013
- Full Text
- View/download PDF
39. When are emptiness and containment decidable for probabilistic automata?
- Author
-
Daviaud, Laure, primary, Jurdziński, Marcin, additional, Lazić, Ranko, additional, Mazowiecki, Filip, additional, Pérez, Guillermo A., additional, and Worrell, James, additional
- Published
- 2021
- Full Text
- View/download PDF
40. Eliminating Recursion from Monadic Datalog Programs on Trees
- Author
-
Mazowiecki, Filip, primary, Ochremiak, Joanna, additional, and Witkowski, Adam, additional
- Published
- 2015
- Full Text
- View/download PDF
41. Pumping lemmas for weighted automata
- Author
-
Chattopadhyay, Agnishom, primary, Mazowiecki, Filip, additional, Muscholl, Anca, additional, and Riveros, Cristian, additional
- Published
- 2021
- Full Text
- View/download PDF
42. Affine Extensions of Integer Vector Addition Systems with States
- Author
-
Blondin, Michael, primary, Haase, Christoph, additional, Mazowiecki, Filip, additional, and Raskin, Mikhail, additional
- Published
- 2021
- Full Text
- View/download PDF
43. Continuous One-Counter Automata
- Author
-
Blondin, Michael, primary, Leys, Tim, additional, Mazowiecki, Filip, additional, Offtermatt, Philip, additional, and Perez, Guillermo A., additional
- Published
- 2021
- Full Text
- View/download PDF
44. Monadic Datalog and Regular Tree Pattern Queries
- Author
-
Mazowiecki, Filip, primary, Murlak, Filip, additional, and Witkowski, Adam, additional
- Published
- 2014
- Full Text
- View/download PDF
45. The Reachability Problem for Petri Nets Is Not Elementary
- Author
-
Czerwiński, Wojciech, primary, Lasota, Sławomir, additional, Lazić, Ranko, additional, Leroux, JÉrôme, additional, and Mazowiecki, Filip, additional
- Published
- 2020
- Full Text
- View/download PDF
46. A Robust Class of Linear Recurrence Sequences
- Author
-
Barloy, Corentin, Fijalkow, Nathanaël, Lhote, Nathan, Mazowiecki, Filip, Fijalkow, Nathanaël, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Département d'Informatique [Bruxelles] (ULB), Faculté des Sciences [Bruxelles] (ULB), Université libre de Bruxelles (ULB)-Université libre de Bruxelles (ULB), University of Warwick [Coventry], and LaBRI (CNRS UMR 5800)
- Subjects
FOS: Computer and information sciences ,[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] ,Computational Theory and Mathematics ,Formal Languages and Automata Theory (cs.FL) ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,Computer Science - Formal Languages and Automata Theory ,Computer Science Applications ,Information Systems ,Theoretical Computer Science - Abstract
International audience; We introduce a subclass of linear recurrence sequences which we call poly-rational sequences because they are denoted by rational expressions closed under sum and product. We show that this class is robust by giving several characterisations: polynomially ambiguous weighted automata, copyless cost-register automata, rational formal series, and linear recurrence sequences whose eigenvalues are roots of rational numbers.
- Published
- 2020
47. Complexity of Two-Variable Logic on Finite Trees
- Author
-
Benaim, Saguy, primary, Benedikt, Michael, additional, Charatonik, Witold, additional, Kieroński, Emanuel, additional, Lenhardt, Rastislav, additional, Mazowiecki, Filip, additional, and Worrell, James, additional
- Published
- 2013
- Full Text
- View/download PDF
48. Weak Cost Register Automata are Still Powerful
- Author
-
Almagor, Shaull, primary, Cadilhac, Michaël, additional, Mazowiecki, Filip, additional, and Pérez, Guillermo A., additional
- Published
- 2020
- Full Text
- View/download PDF
49. Affine extensions of integer vector addition systems with states
- Author
-
Blondin, Michael, Haase, Christoph, Mazowiecki, Filip, and Wagner, Michael
- Subjects
000 Computer science, knowledge, general works ,Computer Science::Logic in Computer Science ,Computer Science ,Computer Science::Formal Languages and Automata Theory - Abstract
We study the reachability problem for affine 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 Z-VASS with the finite-monoid property (afmp-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-Z- VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-Z-VASS reduces to reachability in a Z-VASS whose control-states grow polynomially in the size of the matrix monoid. Our construction shows that reachability relations of afmp-Z-VASS are semilinear, and in particular enables us to show that reachability in Z-VASS with transfers and Z-VASS with copies is PSPACE-complete.
- Published
- 2018
50. The reachability problem for Petri nets is not elementary
- Author
-
Czerwiński, Wojciech, primary, Lasota, Sławomir, additional, Lazić, Ranko, additional, Leroux, Jérôme, additional, and Mazowiecki, Filip, additional
- Published
- 2019
- Full Text
- View/download PDF
Catalog
Discovery Service for Jio Institute Digital Library
For full access to our library's resources, please sign in.