Sieci Petriego stanowią jeden z podstawowych modeli systemów współbieżnych, i są szeroko stosowane wmodelowaniu rozproszonych systemów komputerowych a także układów biologicznych i chemicznych(ilustracja w załączonym pliku). Centralnym problemem algorytmicznym jest problem osiągalności: czy z danej konfiguracji początkowej możnaosiągnąć daną konfigurację końcową za pomocą sekwencji kroków sieci Petriego. Złożoność obliczeniowa tegoproblemu jest otwarta od lat 60tych, stanowiąc jeden z najważniejszych problemów otwartych formalnejweryfikacji. Rozstrzygalność została dowiedziona w roku 1981 (Mayr STOC'81), a obecnie najlepsze ograniczeniegórne to funkcja Ackermanna (Leroux, Schmitz LICS'19). Nie wiemy więc wciąż, czy problem jest pierwotnie rekurencyjny.

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 Ackermannian. We still don't know if the complexity of the problem is primitive recursive.

Analiza automatyczna systemów współbieżnych, grant NCN; Obliczenia symboliczne na obiektach definiowalnych w logice pierwszego rzędu, grant NCN

Automatic analysis of concurrent systems, NCN grant; Symbolic computations on first-order definable objects, NCN grant