形式语言与自动机理论

This paper studies temporal planning in probabilistic environments, modeled as labeled Markov decision processes (MDPs), with user preferences over multiple temporal goals. Existing works reflect such preferences as a prioritized list of…

Probabilistic pushdown automata (pPDA) are a natural operational model for a variety of recursive discrete stochastic processes. In this paper, we study certificates - succinct and easily verifiable proofs - for upper and lower bounds on…

Opacity is a property of privacy and security applications asking whether, given a system model, a passive intruder that makes online observations of system's behaviour can ascertain some "secret" information of the system. Deciding opacity…

A theorem of Cobham says that if $k$ and $\ell$ are two multiplicatively independent natural numbers then a subset of the natural numbers that is both $k$- and $\ell$-automatic is eventually periodic. A multidimensional extension was later…

This paper introduces a robust class of functions from finite words to integers that we call Z-polyregular functions. We show that it admits natural characterizations in terms of logics, Z-rational expressions, Z-rational series and…

The largest known reset thresholds for DFAs are equal to $(n-1)^2$, where $n$ is the number of states. This is conjectured to be the maximum possible. PFAs (with partial transition function) can have exponentially large reset thresholds.…

Temporal logics (TLs) have been widely used to formalize interpretable tasks for cyber-physical systems. Time Window Temporal Logic (TWTL) has been recently proposed as a specification language for dynamical systems. In particular, it can…

Compact representations of automata are important for efficiency. In this paper, we study methods to compute reduced automata, in which no two states accept the same language. We do this for finitary automata (FA), an abstract definition…

The execution of different cases of a process is often restricted by inter-case dependencies through e.g., queueing or shared resources. Various high-level Petri net formalisms have been proposed that are able to model and analyze…

Several new algorithms for deciding emptiness of Boolean combinations of regular languages and of languages of alternating automata (AFA) have been proposed recently, especially in the context of analysing regular expressions and in string…

We consider the implementation of the transduction of automatic sequences, and their generalizations, in the Walnut software for solving decision problems in combinatorics on words. We provide a number of applications, including (a)…

Given an $\omega$-automaton and a set of substitutions, we look at which accepted words can also be defined through these substitutions, and in particular if there is at least one. We introduce a method using desubstitution of…

Jumping automata are finite automata that read their input in a non-consecutive manner, disregarding the order of the letters in the word. We introduce and study jumping automata over infinite words. Unlike the setting of finite words,…

For recursive functions general principles of induction needs to be applied. Instead of verifying them directly using the Vienna Development Method Specification Language (VDM-SL), we suggest a translation to Isabelle/HOL. In this paper,…

In this paper we prove that there is a weakly universal weighted cellular automaton in the heptagrid, the tessellation {7,3} of the hyperbolic plane, with 6 states. The present paper improves the same result deposited on arXiv:2301.10691v1…

This paper introduces a new automata-theoretic class of string-to-string functions with polynomial growth. Several equivalent definitions are provided: a machine model which is a restricted variant of pebble transducers, and a few inductive…

We present efficient computational solutions to the problems of checking equality, performing multiplication, and computing minimal representatives of elements of free bands. A band is any semigroup satisfying the identity $x ^ 2 \approx x$…

We present a formalization of basics related to infinite words in the generic proof assistant Isabelle/HOL. Furthermore, we present a formalization of purely morphic and morphic languages. Finally, we present a formalized definition of…

In this paper, we study arbitrary subword-closed languages over the alphabet $\{0,1\}$ (binary subword-closed languages). For the set of words $L(n)$ of the length $n$ belonging to a binary subword-closed language $L$, we investigate the…

A process discovery algorithm aims to construct a model from data generated by historical system executions such that the model describes the system well. Consequently, one desired property of a process discovery algorithm is…