Formal Languages and Automata Theory
The zone abstraction, widely adopted for its notable practical efficiency, is the de facto standard in the verification of Timed Automata (TA). Nonetheless, region-based abstractions have been shown to outperform zones in specific…
I propose a class of non-positional numeral systems where numbers are represented by Dyck words, with the systems arising from a recursive extension of prime factorization. After describing two proper subsets of the Dyck language capable of…
For a fixed regular language $L$, the enumeration of $L$-infixes is the following task: we are given an input word $w = a_1 \cdots a_n$ and we must enumerate the infixes of $w$ that belong to $L$, i.e., the pairs $i \leq j$ such that $a_i…
The intersection of two context-free languages is not generally context-free, but no geometric criterion has characterized when it remains so. The crossing gap (max(i'-i, j'-j) for two crossing push-pop arcs) is the natural candidate. We…
We propose a new method, that we coined the ``morphism-trick'', to integrate custom implementations of vector-Jacobian products in automatic differentiation softwares, applicable to a wide range of semiring-based computations. Our approach…
Global protocols specify distributed, message-passing protocols from a birds-eye view, and are used as a specification for synthesizing local implementations. Implementability asks whether a given global protocol admits a distributed…
The theory of finite automata concerns itself with words in a free monoid together with concatenation and without further structure. There are, however, important applications which use alphabets which are structured in some sense. We…
Global protocol specifications are the starting point of top-down verification methodologies, and serve as a blueprint for synthesizing local specifications that guarantee the correctness of distributed implementations. In this work, we…
We present a passive automata learning algorithm that can extract automata from recurrent networks with very large or even infinite alphabets. Our method combines overapproximations from the field of Abstract Interpretation and passive…
Recently, a new paradigm was introduced in automata theory. The main idea is to classify regular languages according to their propensity to be sorted, establishing a deep connection between automata theory and data compression [J. ACM…
We introduce Controlled Stochastic Activity Networks (Controlled SANs), a formal extension of classical Stochastic Activity Networks that integrates explicit control actions into a unified semantic framework for modeling distributed…
Assembly Theory, as developed by Cronin and co-workers, assigns to an object an assembly index: the minimal number of binary join operations required to build at least one copy of the object from a specified set of basic building blocks,…
This paper proposes a generalized framework for cellular automata using the language of category theory, extending the classical definition beyond set-theoretic constraints. For an arbitrary category $\mathscr{C}$ with products, we define…
Serious games have proven to be effective tools for screening cognitive impairments and supporting diagnosis in patients with neurodegenerative diseases like Alzheimer's and Parkinson's. They also offer cognitive training benefits.…
A separator is a countable dense subset of $[0,1)$, and a separator enumerator is a naming scheme that assigns a real number in $[0,1)$ to each finite word so that the set of all named values is a separator. Mayordomo introduced separator…
A central decision problem in Petri net theory is reachability asking whether a given marking can be reached from the initial marking. Related is the covering problem (or sub-marking reachbility), which decides whether there is a reachable…
The theory of free-choice Petri nets is an established field, initiated in the 1970s by Commoner and Hack at MIT. We revisit well-formed free-choice nets (those admitting markings that are both live and bounded) and provide a new…
Synthesis automatically generates a process model from a behavioural specification. When the target model is a Petri net, we address synthesis through region theory. Researchers have studied region-based synthesis extensively for…
In this paper, we introduce monoidal rewriting systems (MRS), an abstraction of string rewriting in which reductions are defined over an arbitrary ambient monoid rather than a free monoid of words. This shift is partly motivated by logic:…
Asynchronous automata are a model of distributed finite state processes synchronising on shared actions. A celebrated result by Zielonka shows how a deterministic asynchronous automaton (AA) can be synthesised, starting from two inputs: a…