8 papers
Regularity as seen by Alice and Bob
Omid Yaghoubi, Mikołaj Bojańczyk, Aliaume Lopez +1
The goal of this paper is to propose a unifying model for Nerode-style characterizations of regularity across functions with different output domains. Building on Hauser's work in…
Polyregular equivalence is undecidable in higher-order types
Mikołaj Bojańczyk, Grzegorz Fabiański, Rafał Stefański
It is open whether equivalence ( f = g ) is decidable for string-to-string polyregular functions. We consider their higher-order extension based on the λ-calculus definition of pol…
A Formally Verified Lightning Network
Grzegorz Fabiański, Rafał Stefański, Orfeas Stefanos Thyfronitis Litos
In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We…
Polyregular Model Checking
Aliaume Lopez, Rafał Stefański
We introduce a high-level language with Python-like syntax for string-to-string, polyregular, first-order definable transductions. This language features function calls, boolean va…
Monads, Comonads, and Transducers
Rafał Stefański
This paper proposes a definition of recognizable transducers over monads and comonads, which bridges two important ongoing efforts in the current research on regularity. The first…
The single-use restriction for register automata and transducers over infinite alphabets
Rafał Stefański
This thesis studies the single-use restriction for register automata and transducers over infinite alphabets. The restriction requires that a read-access to a register should have…
Function spaces for orbit-finite sets
Mikołaj Bojańczyk, Lê Thành Dũng Nguyên, Rafał Stefański
Orbit-finite sets are a generalisation of finite sets, and as such support many operations allowed for finite sets, such as pairing, quotienting, or taking subsets. However, they d…
Extensions of -Regular Languages
Mikołaj Bojańczyk, Edon Kelmendi, Rafał Stefański +1
We consider extensions of monadic second order logic over -words, which are obtained by adding one language that is not -regular. We show that if the added language has a…