ABSTRACT. The bandwidth of timed automata characterizes the quantity of information produced/transmitted per time unit. We previously delimited 3 classes of TA according to the nature of their asymptotic bandwidth: meager, normal, and obese. In this paper, we propose a method, based on a finite-state simply-timed abstraction, to compute the actual value of the bandwidth of meager automata. The states of this abstraction correspond with barycenters of the faces of the simplices in the region automaton. Then the bandwidth is $\log 1/|z_0|$ where $z_0$ is the smallest root (in modulus) of the characteristic polynomial of this finite-state abstraction.

ABSTRACT. Reachability analysis in rewriting has served as a verification technique in recent decades, despite the underlying issue being undecidable. Regular tree model-checking has found application in verifying security protocols, Java programs, and concurrent systems. The premise in these approaches is to represent the targeted system as a state system and en- code its transitions using a term rewriting system or a tree transducer. The crucial aspect lies in calculating a fixed point that represents the set of configurations or states that can be reached. While this is generally uncomputable, it is sufficient to compute an overapproximation for the purpose of verifying safety properties. Let A, B, and R represent, respectively, an initial set of terms, a set of forbidden (“bad”) terms, and a term rewriting system. The question is whether there exists a regular approximation A⋆ of the set of reachable terms such that A⋆ ⊇ R∗ (A) and A⋆ ∩ B = ∅. Finding suitable approximations requires, in practice, the use of heuristics, steered towards an anticipated conclusive fixed point by the intervention of human domain experts. The parameters upon which they act may take the form of term equations, normalizing rules, predicate abstractions, etc, but in all cases boil down to carefully choosing states to merge during the fixpoint computation, forcing convergence while avoiding overshooting the approximation into B. We propose a practical, scalable automated method offloading that expert work to a SAT solver.

ABSTRACT. Automata have been defined to recognize languages of words indexed by linear orderings, which generalize the usual notions of finite, infinite, and ordinal words. The reachability problem for these automata has already been solved for scattered linear orderings. In this paper, we design an analogous procedure that solves reachability over the specific domains R and Q. Given an automaton on linear orderings, this procedure decides in polynomial time whether this automaton accepts at least one word indexed by R or by Q. We claim that this algorithm constitutes an essential step to designing effective decision procedures for the first-order monadic theory of order interpreted over R or Q.

ABSTRACT. The interaction between a system and its environment corresponds to a game in which the system and the environment generate a word over the alphabet of assignments to the input and output signals. The system player wins if the generated word satisfies a desired specification. A correct reactive system has to satisfy its specification in all environments, and thus corresponds to a strategy for the system player in the above game. This view is the key to the game-based approach for reactive synthesis. It reduces synthesis to the problem of generating winning strategies in two-player games whose winning conditions are on-going behaviours, which can be specified by automata on infinite words. The talk presents the game-based approach, focusing on ways to cope with the fact that the game cannot be played over nondeterministic automata.

ABSTRACT. The notion of push complexity has been recently introduced by Bordhin and Mitrana as a measure of nonregularity for context-free languages. This measure takes into account the number of push operations used to accept inputs of length n. We show that the push complexity of each nonregular context-free language grows at least as a double logarithmic function, with respect to the length of the strings. This lower bound is optimal. Indeed, we prove that there exists a language with push complexity O(log log n). It is known that it cannot be decided whether the number of push operations used by a pushdown automaton is bounded by any constant. We prove that, in the restricted case of pushdown automata with a one-letter input alphabet, this question is decidable. Furthermore, under the same restriction, if the number of push operations used by a pushdown automaton is not bounded by any constant, then it should grow at least as a linear function in the length of the input.

ABSTRACT. When designing and maintaining the information systems, there is a need to use parameterized automata, in which some components of the model that determine its behavior are replaced with variables. It has previously been shown that the complexity of many analysis and synthesis problems increases significantly when machines or programs have parameters. Nevertheless, it can be expected that for some classes of automata the complexity of certain important problems will remain low and and the development of efficient algorithms will be possible. We present here the results of our study of some basic decision problems for finite state transducers parameterized on output data. When choosing this class of automata, we were guided by the intention of preserving the determinism of runs with uncertain values of some elements due to the presence of parameters in the model. We managed to show that for some decision problems their complexity remains low (NL-complete) even after parameters are added to the model, whereas the complexity of other problems that have efficient solutions for ordinary transducers increases significantly (from NL or P-completeness to NP-completeness and beyond) for their parameterized modifications.

ABSTRACT. This paper complements a recent inapproximability result for the minimal pumping constant w.r.t. a fixed regular pumping lemma for nondeterministic finite automata [H. Gruber and M. Holzer and C. Rauch. The Pumping Lemma for Regular Languages is Hard. CIAA 2023, pp. 128-140.], by showing the inapproximability of this problem even for deterministic finite automata, and at the same time proving stronger lower bounds on the attainable approximation ratio, assuming the Exponential Time Hypothesis (ETH). To that end, we describe those homomorphisms that, in a precise sense, preserve the respective pumping arguments used in two different pumping lemmata. We show that, perhaps surprisingly, this concept coincides with the classic notion of star height preserving homomorphisms as studied by McNaughton, and by Hashiguchi and Honda in the 1970s. Also, we gain a complete understanding of the minimal pumping constant for bideterministic finite automata, which may be of independent interest.

ABSTRACT. In this paper we consider block languages, namely sets of words having the same length, and we propose a new representation for these languages. In particular, given an alphabet of size k and a length l, a block language can be represented by a bitmap of length l, where each bit indicates whether the corresponding word, according to the lexicographical order, belongs, or not, to the language (bit equal to 1 or 0, respectively). This representation turns out to be a good tool for the investigation of several properties of block languages, making proofs simpler and reasoning clearer. First, we show how to convert bitmaps into deterministic and nondeterministic finite automata. We then focus on the size of the machines obtained from the conversion and we prove that their size is minimal. Finally, we give an analysis of the maximum number of states sufficient to accept every block language in the deterministic and nondeterministic case.

ABSTRACT. Let $L$ be a regular language not containing $\eps$. We determine the state complexity of the two operations $L \rightarrow L L^+$ and $L \rightarrow L \setminus L L^+$. The latter is of interest because $L \setminus L L^+$ is the ``minimal star basis'', the set of all strings of $L$ that cannot be written as the concatenation of shorter strings of $L$, a concept first studied by John Brzozowski in 1966.

ABSTRACT. The number of states and stack symbols needed to determinize nondeterministic input-driven pushdown automata (NIDPDA) working over a fixed alphabet is determined precisely. It is proved that in the worst case exactly 2^{n^2} states are needed to determinize an n-state NIDPDA, and the proof uses witness automata with a stack alphabet \Gamma = {0,1} working on strings over a 4-symbol input alphabet (Only an asymptotic lower bound was known before in the case of a fixed alphabet). Also, the impact of NIDPDA determinization on the size of stack alphabet is determined precisely for the first time: it is proved that s(2^{n^2}-1) stack symbols are necessary in the worst case to determinize an n-state NIDPDA working over an input alphabet of size s+5 with s left brackets (The previous lower bound was only asymptotic in the number of states and did not depend on the number of left brackets).