Minimal Size of Counters for (Real-Time) Multicounter Automata

We show that, for automata using a finite number of counters, the minimal space that is required for accepting a nonregular language is (log n)ɛ. This is required for weak space bounds on the size of their counters, for real-time and one-way, and for nondeterministic and alternating versions of these automata. The same holds for two-way automata, independent of whether they work with strong or weak space bounds, and of whether they are deterministic, nondeterministic, or alternating. (Here ɛ denotes an arbitrarily small—but fixed—constant; the “space” refers to the values stored in the counters, rather than to the lengths of their binary representation.) On the other hand, we show that the minimal space required for accepting a nonregular language is nɛ for multicounter automata with strong space bounds, both for real-time and one-way versions, independent of whether they are deterministic, nondeterministic, or alternating, and also for real-time and one-way deterministic multicounter automata with weak space bounds. All these bounds are optimal both for unary and general nonregular languages. However, for automata equipped with only one counter, it was known that one-way nondeterministic automata cannot recognize any unary nonregular languages at all, even if the size of the counter is not restricted, while, with weak space bound log n, we present a real-time nondeterministic automaton recognizing a binary nonregular language here.

Non-Self-Embedding Grammars and Descriptional Complexity

Non-self-embedding grammars are a subclass of context-free grammars which only generate regular languages. The size costs of the conversion of non-self-embedding grammars into equivalent finite automata are studied, by proving optimal bounds for the number of states of nondeterministic and deterministic automata equivalent to given non-self-embedding grammars. In particular, each non-self-embedding grammar of size s can be converted into an equivalent nondeterministic automaton which has an exponential size in s and into an equivalent deterministic automaton which has a double exponential size in s. These costs are shown to be optimal. Moreover, they do not change if the larger class of quasi-non-self-embedding grammars, which still generate only regular languages, is considered. In the case of letter bounded languages, the cost of the conversion of non-self-embedding grammars and quasi-non-self-embedding grammars into deterministic automata reduces to an exponential of a polynomial in s.

Parallel decomposition of control algorithms for computational processes based on the use of nondeterministic automaton logic

The paper deals with the issues of decomposition of control algorithms for the processes in parallel computing systems and the use of automaton models. When designing parallel processing systems, an important task is the formal presentation of process control algorithms since they allow achieving a packaged solution to the problems of specification, development, implementation, verification, and analysis of complex control systems, including the control of interacting processes and resources in parallel computing systems. It is especially necessary to use formal methods to verify complex information processing systems by model testing. One of the methods for the formal description of control algorithms is based on the use for these purposes of the nondeterministic automaton (NDA) logic, which is a method that allows one to present control algorithms for information processing in the form of systems of canonical equations describing all particular events implemented in the algorithm. The advantage of such a language is that all transitions in the control system are described not in terms of system states, but in terms of particular events, the simultaneous existence of which determines all states and transitions in the system; this allows avoiding a "combinatorial explosion" in the state space to the possibilities of means verification. Purpose of the paper: research of control algorithms for parallel computing systems using the NDA apparatus. The development and research object is parallel decomposition of control algorithms for parallel computing systems using automatic models.

MINIMIZATION OF PLANAR DIRECTED ACYCLIC GRAPH ALGEBRAS

We introduce planar directed acyclic graph algebras and present an explicit minimization method. The minimal simulation of a nondeterministic automaton on planar directed acyclic graphs is constructed.

COUNTING SUBWORDS USING A TRIE AUTOMATON

We use the concept of trie (prefix tree) representation of a prefix-closed finite language L to design a simple nondeterministic automaton. Each computation of this trie automaton corresponds to a subword occurrence of a word from L in the input word. The matrix representation of the trie automaton leads to a fairly general extension of the original concept of the Parikh matrix from [7].

DETERMINISTIC PUSHDOWN AUTOMATA AND UNARY LANGUAGES

The simulation of deterministic pushdown automata defined over a one-letter alphabet by finite state automata is investigated from a descriptional complexity point of view. We show that each unary deterministic pushdown automaton of size s can be simulated by a deterministic finite automaton with a number of states that is exponential in s. We prove that this simulation is tight. Furthermore, its cost cannot be reduced even if it is performed by a two-way nondeterministic automaton. We also prove that there are unary languages for which deterministic pushdown automata cannot be exponentially more succinct than finite automata. In order to state this result, we investigate the conversion of deterministic pushdown automata into context-free grammars. We prove that in the unary case the number of variables in the resulting grammar is strictly smaller than the number of variables needed in the case of nonunary alphabets.

SYMBOLIC IMPLEMENTATION OF ALTERNATING AUTOMATA

This paper addresses the challenges of symbolic model checking and language emptiness checking where the specification is given as an alternating Büchi automaton. We introduce a novel version of Miyano and Hayashi's construction that allows us to directly convert an alternating automaton to a polynomially-sized symbolic structure. We thus avoid building an exponentially-sized explicit representation of the corresponding nondeterministic automaton. For one-weak automata, Gastin and Oddoux' construction produces smaller automata than Miyano and Hayashi's construction. We present a (symbolic) hybrid approach that combines the benefits of both: while retaining full generality, it uses the cheaper construction for those parts of the automaton that are one-weak. We performed a thorough experimental comparison of the explicit and symbolic approaches and several variants of Miyano and Hayashi's construction, using both BDD-based and SAT-based model checking techniques. The symbolic approaches clearly outperform the explicit one.