The tensor product $K \mathop{\otimes_{\cal R}} C_2'$ of the ${}^*$-continuous Kleene algebra $K$ with the polycyclic ${}^*$-continuous Kleene algebra $C_2'$ over two bracket pairs contains a copy of the fixed-point closure of $K$: the centralizer of $C_2'$ in $K \mathop{\otimes_{\cal R}} C_2'$. We prove a representation of elements of $K\mathop{\otimes_{\cal R}} C_2'$ by automata \`a la Kleene and refine it by normal form theorems that restrict the occurrences of brackets on paths through the automata. This is a foundation for a calculus of context-free expressions. We also show that $C_2'$ validates a relativized form of the ``completeness property'' that distinguishes the bra-ket ${}^*$-continuous Kleene algebra $C_2$ from the polycyclic one. less

The recent years have seen remarkable progress in establishing the complexity of the reachability problem for vector addition systems with states (VASS), equivalently known as Petri nets. Existing work primarily considers the case in which both the VASS as well as the initial and target configurations are part of the input. In this paper, we investigate the reachability problem in the setting where the VASS is fixed and only the initial configuration is variable. We show that fixed VASS fully express arithmetic on initial segments of the natural numbers. It follows that there is a very weak reduction from any fixed such number-theoretic predicate (e.g. primality or square-freeness) to reachability in fixed VASS where configurations are presented in unary. If configurations are given in binary, we show that there is a fixed VASS with five counters whose reachability problem is PSPACE-hard. less

Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but not tested for zero. Whether the reachability problem is decidable for PVASS is a long-standing open problem. We consider continuous PVASS, which are PVASS with a continuous semantics. This means, the counter values are rational numbers and whenever a vector is added to the current counter values, this vector is first scaled with an arbitrarily chosen rational factor between zero and one. We show that reachability in continuous PVASS is NEXPTIME-complete. Our result is unusually robust: Reachability can be decided in NEXPTIME even if all numbers are specified in binary. On the other hand, NEXPTIME-hardness already holds for coverability, in fixed dimension, for bounded stack, and even if all numbers are specified in unary. less

We consider the problem of enumerating a regular language $L$ in radix order, or more precisely, the equivalent problem of enumerating all words in $L$ of a given length in lexicographic order. Ackerman and Shallit gave in 2009 the principles of an efficient solution to this problem, but they did not use the enumeration complexity framework for their analysis. We adapt their work into an explicit algorithm that fits this framework. less

Opacity is a property that captures security concerns in cyber-physical systems and its verification plays a significant role. This paper investigates the verifications of K-step and infinite-step weak and strong opacity for partially observed nondeterministic finite state automata. K-step weak opacity is checked by constructing, for some states in the observer, appropriate state-trees, to propose a necessary and sufficient condition. Based on the relation between K-step weak and infinite-step weak opacity, a condition that determines when a system is not infinite-step weak opaque is presented. Regarding K-step and infinite-step strong opacity, we develop a secret-involved projected automaton, based on which we construct secret-unvisited state trees to derive a necessary and sufficient condition for K-step strong opacity. Furthermore, an algorithm is reported to compute a verifier that can be used to obtain a necessary and sufficient condition for infinite-step strong opacity. It is argued that, in some particular cases, the proposed methods achieve reduced complexity compared with the state of the art. less

Mata is a well-engineered automata library written in C++ that offers a unique combination of speed and simplicity. It is mean to serve in applications such as string constraint solving and reasoning about regular expressions, and a as reference implementation of automata algorithms. Besides basic algorithms for (non)deterministic automata, it implements a fast simulation reduction and antichain-based language inclusion checking. The simplicity allows a straightforward access to the low level structures, making it relatively easy to extend and modify. Besides the C++ API, the library also implements a Python binding. The library comes with a large benchmark of automata problems collected from relevant applications such as string constraint solving, regular model checking, and reasoning about regular expressions. We show that Mata is on this benchmark significantly faster than all libraries from a wide range of automata libraries we collected. Its usefulness in string constraint solving is demonstrated by the string solver Z3-Noodler, which is based on Mata and outperforms the state of the art in string constraint solving on many standard benchmarks. less

We investigate the dimension-parametric complexity of the reachability problem in vector addition systems with states (VASS) and its extension with pushdown stack (pushdown VASS). Up to now, the problem is known to be $\mathcal{F}_k$-hard for VASS of dimension $3k+2$ (the complexity class $\mathcal{F}_k$ corresponds to the $k$th level of the fast-growing hierarchy), and no essentially better bound is known for pushdown VASS. We provide a new construction that improves the lower bound for VASS: $\mathcal{F}_k$-hardness in dimension $2k+3$. Furthermore, building on our new insights we show a new lower bound for pushdown VASS: $\mathcal{F}_k$-hardness in dimension $\frac k 2 + 4$. This dimension-parametric lower bound is strictly stronger than the upper bound for VASS, which suggests that the (still unknown) complexity of the reachability problem in pushdown VASS is higher than in plain VASS (where it is Ackermann-complete). less

Nondeterministic Discounted-Sum Automata (NDAs) are nondeterministic finite automata equipped with a discounting factor $\lambda>1$, and whose transitions are labelled by weights. The value of a run of an NDA is the discounted sum of the edge weights, where the $i$-th weight is divided by $\lambda^{i}$. NDAs are a useful tool for modelling systems where the values of future events are less influential than immediate ones. While several problems are undecidable or open for NDA, their deterministic fragment (DDA) admits more tractable algorithms. Therefore, determinization of NDAs (i.e., deciding if an NDA has a functionally-equivalent DDA) is desirable. Previous works establish that when $\lambda\in \mathbb{N}$, then every complete NDA, namely an NDA whose states are all accepting and its transition function is complete, is determinizable. This, however, no longer holds when the completeness assumption is dropped. We show that the problem of whether an NDA has an equivalent DDA is decidable when $\lambda\in \mathbb{N}$. less

The transformation of a nondeterministic finite-state automaton into a deterministic finite-state automaton is an integral part of any course on formal languages and automata theory. For some students, understanding this transformation is challenging. Common problems encountered include not comprehending how the states of the deterministic finite-state automaton are determined and not comprehending the role that all the edges of the nondeterministic finite-state automaton have in the deterministic finite-state automaton's construction. To aid students in understanding, transformation visualization tools have been developed. Although useful in helping students, these tools do not properly illustrate the relationship between the states of the deterministic finite-state automaton and the edges of the nondeterministic finite-state automaton. This article presents a novel interactive visualization tool to illustrate the transformation that highlights this relationship and that is integrated into the FSM programming language. In addition, the implementation of the visualization is sketched. less

Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Whenever two MTS are not in modal refinement relationship, it could still be the case that the set of implementations of one MTS is included in the set of implementations of the other. The challenge of devising an alternative notion of modal refinement that is both sound and complete with respect to the set of implementations, without disregarding valuable implementations, remains open. In this paper, we address this challenge. We introduce a subset of MTS called Non-reducible Modal Transition Systems (NMTS), together with a novel refinement relation for NMTS. We show that NMTS refinement is sound and also complete with respect to its set of implementations. We illustrate through examples how the additional constraints imposed by NMTS are necessary for achieving completeness. Furthermore, we discuss a property holding for NMTS whose implementations are non-deterministic. We show that any implementation obtained through modal refinement but disregarded by NMTS refinement is violating this property. less