arXiv Science⌕ Search

arXiv subjects

Łukasz Kamiński

Publications and source records attributed to Łukasz Kamiński.

7 recordsLinked to original sources

Symmetric two-counter machines

Counter machines are a particularly simple, Turing-complete model of computation. We study the expressive power of nondeterministic 2-counter machines which are symmetric, in that their set of update transitions is invariant under swapping of counters. Our model is an extension of symmetric 2-VASS, in that we allow modifying both counters within a single transition. As the main result we demonstrate a dramatic impact of symmetry: we show that symmetric 2-counter machines are not Turing-complete, by proving decidability of their reachability problem. We conjecture that the decidability extends to machines with 3 or more counters that are symmetric, meaning the set of update transitions is invariant under any permutation of counters. We leave this problem open for machines with 3 and more counters, while identifying a frontier of the impact of symmetry: we prove undecidability for 3-counter machines invariant under the cyclic permutation group of order 3.

cs.FL↗

Integer Reachability in Data VASS

Data Petri nets are an extension of plain Petri nets where, intuitively speaking, tokens carry data values, and transitions may perform equality tests on data values involved. Likewise, data vector addition systems with states (data VASS) are an extension of plain VASS, and equivalent to data Petri nets. The decidability status of the reachability problem in this model is an established and long-standing open question. In this paper we perform a major step towards resolving this question: we show decidability of the integer reachability problem, where the counters can drop below zero. Contrarily to plain VASS, where integer reachability reduces to integer linear programming, the setting of data VASS is significantly more complex, mostly due to the fact that the state spaces are not finite but orbit-finite (like in register automata). Our decision procedure combines an iterative refinement, resembling the KLM decomposition in plain VASS, with a termination argument via a novel way of bounding the number of data values appearing in the refinement. As corollaries, we deduce decidability of a number of decision problems concerning register automata and data Petri nets.

cs.FL↗

Reachability in Symmetric VASS

We investigate the reachability problem in symmetric vector addition systems with states (VASS), where transitions are invariant under a group of permutations of coordinates. One extremal case, the trivial groups, yields general VASS. In another extremal case, the symmetric groups, we show that the reachability problem can be solved in PSPACE, regardless of the dimension of input VASS (to be contrasted with Ackermannian complexity in general VASS). We also consider other groups, in particular alternating and cyclic ones. Furthermore, motivated by the open status of the reachability problem in data VASS, we estimate the gain in complexity when the group arises as a combination of the trivial and symmetric groups.

cs.FL↗

Reachability in 3-VAS

We settle the exact complexity of the reachability problem in (stateless) vector addition systems (VAS) in fixed low dimension. In dimensions 2-4 it has only been known to be sandwiched between NP and PSPACE. We prove PSPACE-hardness of the reachability problem for symmetric vector addition systems in dimension 3 (3-VAS), a restricted fragment of general 3-VAS. Combined with previously established PSPACE upper bounds, our result settles the complexity of the problem to be PSPACE-complete in 3-VAS and 4-VAS, as well as in their symmetric fragments.

cs.CL↗

Definable sets in Skolem arithmetic

In this note, we present a characterization of sets definable in Skolem arithmetic, i.e., the first-order theory of natural numbers with multiplication. This characterization allows us to prove the decidability of the theory. The idea is similar to that of Mostowski; however, our characterization is new, and the proof relies on different combinatorial tools. The main goal of this note is to provide a simpler decidability proof than those previously known.

math.LO↗

Bi-reachability in Petri nets with data

We investigate Petri nets with data, an extension of plain Petri nets where tokens carry values from an infinite data domain, and executability of transitions is conditioned by equalities between data values. We provide a decision procedure for the bi-reachability problem: given a Petri net and its two configurations, we ask if each of the configurations is reachable from the other. This pushes forward the decidability borderline, as the bi-reachability problem subsumes the coverability problem (which is known to be decidable) and is subsumed by the reachability problem (whose decidability status is unknown).

cs.CL↗

Comparative review of selected Internet communication protocols

With a large variety of communication methods and protocols, many software architects face the problem of choosing the best way for services to share information. For communication technology to be functional and practical, it should enable developers to define a complete set of CRUD methods for the processed data. The research team compared the most commonly used data transfer protocols and concepts in this paper: REST, WebSocket, gRPC GraphQL and SOAP. To do that, a set of web servers was implemented in Python, each using one of the examined technologies. Then, the team performed an automated benchmark measuring time and data transfer overhead for a set of defined operations: creating an entity, retrieving a list of 100 entities and fetching details of one entity. Tests were designed to avoid the results being interfered by database connection or docker-compose environment characteristics. The research team has concluded that gRPC was the most efficient and reliable data transfer method. On the other hand, GraphQL turned out to be the slowest communication method of all. Moreover, its server and client libraries caused the most problems with proper usage in a web server. SOAP did not participate in benchmarking due to limited compatibility with Python and a lack of popularity in modern web solutions.

cs.SE↗