Formal Languages and Automata Theory
We develop a general framework for weighted parsing which is built on top of grammar-based language models and employs multioperator monoids as weight algebras. It generalizes previous work in that area (semiring parsing, weighted deductive…
We study the problem of language inclusion between finite, labeled prime event structures. Prime event structures are a formalism to compactly represent concurrent behavior of discrete systems. A labeled prime event structure induces a…
Compiler optimizations are designed to improve run-time performance while preserving input-output behavior. Correctness in this sense does not necessarily preserve security: it is known that standard optimizations may break or weaken…
Grammatical inference is a machine learning area, whose fundamentals are built around learning sets. At present, real-life data and examples from manually crafted grammars are used to test their learning performance. This paper aims to…
In a recent paper of Rampersad et al., the authors conjectured that the smallest possible critical exponent of an infinite balanced word over a 5-letter alphabet is $3/2$. We prove this result, using a formulation of first-order logic, the…
The article continues the study of the genus of regular languages that the authors introduced in a 2012 paper. Generalizing a previous result, we produce a new family of regular languages on a two-letter alphabet having arbitrary high…
The present paper uses spectral theory of linear operators to construct approximately minimal realizations of weighted languages. Our new contributions are: (i) a new algorithm for the SVD decomposition of infinite Hankel matrices based on…
In this dissertation, we study two of the global properties of 1-dimensional cellular automata (CAs) under periodic boundary condition, namely, reversibility and randomness. To address reversibility of finite CAs, we develop a mathematical…
It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Boja\'nczyk, et. al.,(2012) in terms of forest algebras, Straubing (2013) described an…
A word $w$ of letters on edges of underlying graph $\Gamma$ of deterministic finite automaton (DFA) is called synchronizing if $w$ sends all states of the automaton to a unique state. J. \v{C}erny discovered in 1964 a sequence of $n$-state…
We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map solutions and to other solutions. We show that this property can be used to…
Motivated by real-time monitoring and data processing applications, we develop a formal theory of quantitative queries for streaming data that can be evaluated efficiently. We consider the model of unambiguous Cost Register Automata (CRAs),…
Recent studies investigated the problems of analysing Petri nets and synthesising them from labelled transition systems (LTS) with two labels (transitions) only. In this paper, we extend these works by providing new conditions for the…
Automata learning has been successfully applied in the verification of hardware and software. The size of the automaton model learned is a bottleneck for scalability, and hence optimizations that enable learning of compact representations…
In this paper we present a detailed proof of an important result of algebraic logic: namely that the free commutative Kleene algebra is the space of semilinear sets. The first proof of this result was proposed by Redko in 1964, and…
We present the first study of non-deterministic weighted automata under probabilistic semantics. In this semantics words are random events, generated by a Markov chain, and functions computed by weighted automata are random variables. We…
We characterize the class of nondeterministic ${\omega}$-automata that can be used for the analysis of finite Markov decision processes (MDPs). We call these automata `good-for-MDPs' (GFM). We show that GFM automata are closed under classic…
In this note we provide a (decidable) graph-structural characterisation of the infiniteness of $L(w_1, ..., w_k)$, where $L(w_1, ..., w_k) = \{w \in A^* | |w|_{w_1} = \cdots = |w|_{w_k}\}$ is the set of all words that contain the same…
In the past decades, classical results from algebra, including Hilbert's Basis Theorem, had various applications in formal languages, including a proof of the Ehrenfeucht Conjecture, decidability of HDT0L sequence equivalence, and…
Fault Tree Analysis (FTA) is a prominent technique in industrial and scientific risk assessment. Repairable Fault Trees (RFT) enhance the classical Fault Tree (FT) model by introducing the possibility to describe complex dependent repairs…