An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps

We present a symbolic algorithm for strongly connected component decomposition. The algorithm performs Θ(n log n) image and preimage computations in the worst case, where n is the number of nodes in the graph. This is an improvement over the previously known quadratic bound. The algorithm can be used to decide emptiness of Büchi automata with the same complexity bound, improving Emerson and Lei's quadratic bound, and emptiness of Streett automata, with a similar bound in terms of nodes. It also leads to an improved procedure for the generation of nonemptiness witnesses. This work was supported in part by SRC contract 98-DJ-620 and NSF grant CCR-99-71195. This work was done while the author was at the University of Colorado at Boulder.     

Variations on parallel explicit emptiness checks for generalized Büchi automata

We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a strongly connected component (SCC) enumeration and support generalized Büchi acceptance, and require no synchronization points or recomputing procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.     

Representations of commutative asynchronous automata

Ito (1976, 1978) [14], [17] provided representations of strongly connected automata by group-matrix type automata. This shows the close connection between strongly connected automata with their automorphism groups. In this paper we deal with commutative asynchronous automata. In particular, we introduce and study normal commutative asynchronous automata and cyclic commutative asynchronous automata. Some properties on endomorphism monoids of these automata are given. Also, the representations of normal commutative asynchronous automata and cyclic commutative asynchronous automata are provided by S-automata and regular S-automata, respectively. The cartesian composition $\mathbf{A}°\mathbf{B}$ of a strongly connected automaton A and a cyclic commutative asynchronous automaton B is studied. It is shown that the endomorphism monoid $E(\mathbf{A}°\mathbf{B})$ of automaton $\mathbf{A}°\mathbf{B}$ is a Clifford monoid. Finally, a representation of $\mathbf{A}°\mathbf{B}$ is provided by regular Clifford monoid matrix-type automaton. This generalizes and extends the representations of strongly connected automata given by Ito (1976) [14].     

Distance automata having large finite distance or finite ambiguity

A distance automaton is a (nondeterministic finite) automaton which is equipped with a nonnegative cost function on its transitions. The distance of a word recognized by such a machine quantifies the expenses associated with the recognition of this word. The distance of a distance automaton is the maximal distance of a word recognized by this machine or is infinite, depending on whether or not a maximum exists. We present distance automata havingn states and distance 2 ⁿ – 2. As a by-product we obtain regular languages having exponential finite order. Given a finitely ambiguous distance automaton withn states, we show that either its distance is at most 3 ⁿ – 1, or the growth of the distance in this machine is linear in the input length. The infinite distance problem for these distance automata is NP-hard and solvable in polynomial space. The infinite-order problem for regular languages is PSPACE-complete.A preliminary version of this article appeared in theProceedings of the 15th Symposium on Mathematical Foundations of Computer Science, 1990.     

The Saga of Synchronous Bus Arbiter: On Model Checking Quantitative Timing Properties of Synchronous Programs

Quantified Discrete-time Duration Calculus, (QDDC), is a form of interval temporal logic [14]. It is well suited to specify quantitative timing properties of synchronous systems. An automata theoretic decision procedure for QDDC allows converting a QDDC formula into a finite state automaton recognising precisely the models of the formula. The automaton can be used as a synchronous observer for model checking the property of a synchronous program. This theory has been implemented into a tool called DCVALID which permits model checking QDDC properties of synchronous programs written in Esterel, Verilog and SMV notations.In this paper, we consider two well-known synchronous bus arbiter circuits (programs) from the literature. We specify some complex quantitative properties of these arbiters, including their response time and loss time, using QDDC. We show how the tool DCVALID can be used to effectively model check these properties (with some surprising results).     

Deciding Emptiness for Stack Automata on Infinite Trees

We show that the emptiness problem for Büchi stack automata on infinite trees is decidable in elementary time. We first establish the decidability of the emptiness problem for pushdown automata on infinite trees. This is done using a pumping-like argument applied to computation trees. We then show how to reduce the emptiness problem for stack automata to the emptiness problem for pushdown automata. Elsewhere, we have used the result to establish the decidability of several versions of nonregular dynamic logic.     

Inductive inference of logic programs based on algebraic semantics

In this paper we present a new inductive inference algorithm for a class of logic programs, calledlinear monadic logic programs. It has several unique features not found in Shapiro’s Model Inference System. It has been proved that a set of trees isrational if and only if it is computed by a linear monadic logic program, and that the rational set of trees is recognized by a tree automaton. Based on these facts, we can reduce the problem of inductive inference of linear monadic logic programs to the problem of inductive inference of tree automata. Further several efficient inference algorithms for finite automata have been developed. We extend them to an inference algorithm for tree automata and use it to get an efficient inductive inference algorithm for linear monadic logic programs. The correctness, time complexity and several comparisons of our algorithm with Model Inference System are shown.     

The firing squad synchronization problem for a class of polyautomata networks

By the work of Rosenstiehl we know that the firing squad synchronization problem for the class of all polyautomata networks N satisfying the following conditions has a solution: (1) N is connected, (2) the connections of N are bilateral (that is, each connection carries information in both directions). We show that the problem has a solution even if we delete condition (2) if we add the following conditions: (3) the “fan-out” of each output terminal of automata is at most one, (4) for each output terminal of an automaton, the automaton knows whether there is a connection from the output terminal or not. The firing time of our solution is at most (2a2 + 1)ⁿ for sufficiently large n (n is the number of finite automata in the given network and a is the number of output terminals of the component finite automaton).     

Deciding word neighborhood with universal neighborhood automata

Given some form of distance between words, a fundamental operation is to decide whether the distance between two given words w and v is within a given bound. In earlier work, we introduced the concept of a universal Levenshtein automaton for a given distance bound n. This deterministic automaton takes as input a sequence χ of bitvectors computed from w and v. The sequence χ is accepted iff the Levenshtein distance between w and v does not exceed n. The automaton is called universal since the same automaton can be used for arbitrary input words w and v, regardless of the underlying input alphabet. Here, we extend this picture. After introducing a large abstract family of generalized word distances, we exactly characterize those members where word neighborhood can be decided using universal neighborhood automata similar to universal Levenshtein automata. Our theoretical results establish several bridges to the theory of synchronized finite-state transducers and dynamic programming. For small neighborhood bounds, universal neighborhood automata can be held in main memory. This leads to very efficient algorithms for the above decision problem. Evaluation results show that these algorithms are much faster than those based on dynamic programming.     

Program equivalence checking by two-tape automata

This paper shows how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. The semantics of sequential programs is defined in terms of dynamic logic structures. If a dynamic frame is acyclic (i.e., all program statements are irreversible), then it can be specified by means of a two-tape deterministic automaton. Then the equivalence checking problem for sequential programs in which the semantics of operators is determined by acyclic dynamic frames can be reduced to the emptiness problem for two-tape automata (compound machines).