Radosław Piórkowski

Highlights Conference 2025 Conference Abstract

MSO Characterization of Register Automata Languages

• Radosław Piórkowski

Highlights Conference 2024 Conference Abstract

Cost register automata over min–plus semiring and their boundedness problem

• Radosław Piórkowski

Cost register automata (CRAs), like weighted automata, define functions of type $\Sigma^* \to \mathbb{K}$ for some semiring $\mathbb{K} = (K, \oplus, \otimes)$. They can be thought of as finite automata with an additional finite set $X$ of write-only registers holding values from $\mathbb{K}$: register values can be combined and updated with the operations $\oplus$ and $\otimes$, but no value tests are permitted. Compared to weighted automata, variants of CRAs draw a more nuanced undecidability frontier. In particular, linear CRAs (deterministic) are equally expressive as WAs (inherently nondeterministic), and many other natural classes of CRA are incomparable with known variants of weighted automata. The class of copyless linear CRAs over the min–plus semiring is a severely restricted yet still remarkably expressive one. Decidability of some of its standard decision problems has been established, a notable exception being the boundedness problem: "is the function given by a CRA bounded from above? ". We show it decidable for the class of two-register copyless linear CRAs. In my presentation, following an introduction to variants of CRAs, I will provide an overview of the challenges associated with boundedness and present the main ideas of our decidability proof. Authors: Andrei Draghici, Radosław Piórkowski, Andrew Ryzhikov

Highlights Conference 2023 Conference Abstract

Universal quantification in automatic structures: an ExpSpace-hard nut to crack

• Radosław Piórkowski

Automatic structures are structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular languages that the first-order theory of an automatic structure is decidable. While existential quantifiers can be eliminated in linear time by application of a homomorphism, universal quantifiers are commonly eliminated via the identity ∀x. Φ ≡ ¬(∃x. ¬Φ). If Φ is represented in the standard way as an NFA, a priori this approach results in a doubly exponential blow-up. However, the recent literature has shown that there are classes of automatic structures for which universal quantifiers can be eliminated without this blow-up when treated as first-class citizens and not resorting to double complementation. While existing lower bounds for some classes of automatic structures show that a singly exponential blow-up is unavoidable when eliminating a universal quantifier, it is not known whether there may be better approaches that avoid the naïve doubly exponential blow-up. We answer this question negatively. In my presentation, starting with a short introduction to the field of automatic structures, I will outline the construction of a family of NFA representing automatic relations for which the minimal NFA recognising the language after a universal projection step is doubly exponential, and deciding whether this language is empty is ExpSpace-complete. Keywords: automatic structures, universal projection, tiling problems, state complexityAuthors: Christoph Haase, R. P. Contributed talk given by Radosław Piórkowski

Highlights Conference 2020 Conference Abstract

Timed synthesis games

• Radosław Piórkowski

We study a generalisation of Büchi-Landweber games to the timed setting with an aim of solving the strategy synthesis problem for Player II. In our setting, that equals to constructing a timed automaton with an output – a timed controller. We show that for fixed number of clocks but *without* specifying the maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. This is an important technical novelty, since the related decidability results found in previous literature required both constants to be fixed. As an application of timed games, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata. This is a novel decision problem about timed automata which has not been studied before. During the presentation, I will briefly introduce our games and show, how our results can be used to solve the separability problem. This presentation is based on a paper by Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski.

I&C Journal 2020 Journal Article

WQO dichotomy for 3-graphs

• Sławomir Lasota
• Radosław Piórkowski

We investigate data-enriched models, like Petri nets with data, where executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems in such models may depend on the structure of data domain. According to the WQO Dichotomy Conjecture, if a data domain is homogeneous then it either exhibits a well quasi-order (in which case decidability follows by standard arguments), or essentially all the decision problems are undecidable for Petri nets over that data domain. We confirm the conjecture for data domains being 3-graphs (graphs with 2-colored edges). On the technical level, this result is a significant step towards classification of homogeneous 3-graphs, going beyond known classification results for homogeneous structures.

Highlights Conference 2018 Conference Abstract

Decidability in data Petri nets — a conjecture

• Radosław Piórkowski

ABSTRACT. We investigate data-enriched models, like Petri nets with data, where executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems in such models may depend on the structure of data domain. According to the WQO Dichotomy Conjecture, if a data domain is homogeneous then it either exhibits a well quasi-order (in which case decidability follows by standard arguments), or essentially all the decision problems are undecidable for Petri nets over that data domain. During the talk, we will present the context and state the conjecture. Our results concerning resolved special cases of the conjecture will be presented on the poster.