Rational index of Vector Addition Systems languages

Summary The rational index _L of a non-empty language L is a function of into , whose asymptotic behavior can be used to classify languages. We prove that the languages associated to Vector Addition System or Petri nets have rational indexes bounded by polynomials. This situation should be contrasted with the case of context-free languages. Indeed some context-free languages like the Greibach's languages have rational indexes bounded by polynomials. But some other context-free languages have rational indexes in exp n and the generators of the rational cone of context-free languages have rational indexes in exp n ²/ln n. We give an upper bound and a lower bound on the rational index of each term of an infinite sequence of V.A.S. languages, such that any V.A.S. language can be obtained as the image by a rational transduction of one of these languages.     

On efficient deterministic simulation of turing machine computations below logaspace

It is shown that a bounded language accepted by a nondeterministic Turing machine in spaceS(n o(logn) can be accepted by a deterministic Turing machine in space MAX {(s(nn))², logn}. This can be interpreted as extending Savitch's algorithm below logspace. Results of Alt can be used to show that in the general case the indicated space bound cannot be improved. The result can also be interpreted as a sharpening in the special case of bounded languages of the results of Monien and Sudborough.     

Iterated linear control and iterated one-turn pushdowns

For a class of languages, an-controlled linear grammarK consists of a linear context-free grammarG and a control languageH in, where the terminals ofH are interpreted as the labels of rules ofG. The language generated byK is obtained by derivations ofG such that the corresponding strings of labels of the rules applied are control strings inH. The control of linear grammars can be iterated by starting with and by taking the result of thekth step as class of control languages for the (k + 1)st step. The language class obtained by thekth step is denoted by CTRL_k(). Denote by(S) the language class accepted by nondeterministic one-wayS automata, whereS is a storage type. We prove that for anyS, CTRL_k((S)) = (P _1t ^k (S)), whereP _1t ^k (S) is the storage type the configurations of which consist ofk-iterated one-turn pushdowns ofS-configurations. We establish a strong connection between iterated linear control and iterated one-turn pushdowns. In particular, we characterize CTRL _k ( _CF), where _CF is the class of context-free languages, by iterated one-turn pushdown automata in which the innermost pushdown is unrestricted.The work of the author has been supported by the Netherlands Organization for the advancement of pure research (Z.W.O.).     

Bicentres de langages algébriques

Resume Les notions de bicentre et bicentre strict d'un langage, définies par A. De Luca, A. Restivo et S. Salemi généralisent la notion de centre d'un langage définie par M. Nivat. L'objet du présent papier est de répondre á la question suivante lorsque désigne la famille des langages algébriques ou l'une de ses sous-familles classiques:Si L appartient à , le bicentre de L (respectivement le bicentre strict de L) appartient-il à ?Le principal résultat est une réponse positive à cette question lorsqu'il s'agit de la notion de bicentre et que est un full-AFL uniforme de langages algébriques.

---

Bicenters of context-free languages

Summary The notions of bicenter and strict bicenter of a language have been defined by A. De Luca, A. Restivo and S. Salemi and are a generalisation of the notion of center of a language, defined by M, Nivat. This paper deals with the following question, when is the family of context-free languages or one of its classical subfamilies:when L is in , is the bicenter (resp. the strict bicenter) of L also in ?Concerning the notion of bicenter, the main result of the paper is a positive answer when is a uniform full-AFL of context-free languages.

     

Timing Diagrams: Formalization and Algorithmic Verification

Timing diagrams are popular in hardware design. They have been formalized for use in reasoning tasks, such as computer-aided verification. These efforts have largely treated timing diagrams as interfaces to established notations for which verification is decidable; this has restricted timing diagrams to expressing only regular language properties. This paper presents a timing diagram logic capable of expressing certain context-free and context-sensitive properties. It shows that verification is decidable for properties expressible in this logic. More specifically, it shows that containment of -regular languages generated by Büchi automata in timing diagram languages is decidable. The result relies on a correlation between timing diagram and reversal bounded counter machine languages.     

Investigations on Hotz groups for arbitrary grammars

Summary The Hotz group H(G) and the Hotz monoid M(G) of an arbitrary grammar G=(V, X, P, S) are defined by H(G)=F(VX)/P and M(G) =(VX)^*/P respectively. A language LX^* is called a language with Hotz isomorphism if there exists a grammar G with L=L(G) such that the natural homomorphism F(X)/LH(G) is an isomorphism. The main result of this paper states that homomorphic images of sentential form languages are languages with Hotz isomorphism. This is a generalization of a result of Frougny, Sakarovitch, and Valkema on context-free languages.Hotz groups are used to obtain lower bounds for the number of productions which are needed to generate a language. Further it is shown that there are languages with Hotz isomorphism without being a homomorphic image of a sentential form language, and there are context-sensitive languages without Hotz isomorphism. The theory of Hotz monoids is used to get some results on languages generated by grammars with a symmetric set of rules.     

Cut point languages of markov DTOL systems

Letp satisfy 0 p < 1, then by (p) we denote the family of Markov DTOL languages with cut pointp. In this paper we present a complete classification of the collection of such families (p), 0 p < 1, showing that forms an infinite nondense hierarchy with (0) being its only accumulation point from below. Furthermore it is proved that each language in (p) can be expressed as a finite union of DDTOL languages.Work supported partially by the Natural Sciences and Engineering Research Council of Canada grants Nos. A-3590 and A-7700, and partially by Deutsche Forschungsgemeinschaft.     

Axiomatic semantics of R-schemas and verification of graphic programs

We propose an approach to verification of programs in a graphic language in the programming R-technology and introduce an axiomatic semantics of R-schemas and of graphic Pascal. We justify the advantages of graphic representation of programs for correctness proving and describe a support system for this approach under RAFOS and MS-DOS.Translated from Kibernetika, No. 1, pp. 21–27, January–February, 1990.     

A note on classes of complements and the LBA problem

Summary The complements of an AFL form an AFL if and only if is closed under length-preserving universal quantification. The complements of the context-sensitive languages form a principal AFL with a hardest set L ₁. The context-sensitive languages are closed under complementation if and only if L ₁ is context-sensitive.This research was supported in part by the National Science Foundation under Grants MCS76-10076 and DCR74-15091     

On generators and generative capacity of EOL forms

Summary In this paper we study the generative capacity of EOL forms from two different points of view. On the one hand, we consider the generative capacity of special EOL forms which one could call linear like and context free like, establishing the existence of a rich variety of non-regular sub-EOL language families. On the other hand, we propose the notion of a generator L of a language family We mean by this that any synchronized EOL system generating L generates — if understood as an EOL form — all languages of . We characterize the generators of the family of regular languages, and prove that other well known language families do not have generators.Partially supported under NSE Research Council of Canada, grant No. A-7700     

Minimization of norms and logarithmic norms by diagonal similarities

It is a commonly occurring problem to find good norms · or logarithmic norms (·) for a given matrix in the sense that they should be close to respectively the spectral radius (A) and the spectral abscissa (A). Examples may be the certification thatA is convergent, i.e. (A)A<1 or stable, i.e. (A)(A)<0. Often the ordinary norms do not suffice and one would like to try simple modifications of them such as using an ordinary norm for a diagonally transformed matrix. This paper treats this problem for some of the ordinary norms.

---

Minimisierung von Normen und Logarithmischen Normen durch Diagonale Transformationen

Zusammenfassung Ein oft vorkommendes praktisches Problem ist die Konstruktion von guten Normen · und logarithmischen Normen (·) für eine gegebene MatrixA. Mit gut wird dann verstanden, daß A den Spektralradius (A)=max |₁| und (A) die Spektralabszisse (A)=max Re _i gut approximieren. Beispiele findet man für konvergente Matrizen wo (A)A<1 gewünscht ist, und für stabile Matrizen wo (A)(A)<0 zu zeigen ist. Wir untersuchen hier, wie weit man mit Diagonaltransformationen und dengewöhnlichsten Normen kommen kann.

     

Specification and automatic verification of self-timed queues

Speed-independent circuit design is of increasing interest because of global timing problems in VLSI. Unfortunately, speed-independent design is very subtle. We propose the use of statemachine verification tools to ameliorate this problem. This article illustrates issues in the modeling, specification, and verification of speed-independent circuits through consideration of self-timed queues. User-level specifications are given as Petri nets, which are translated into trace structures for automatic processing. Three different implementations of queues are considered: a chain of queue cells, two parallel chains, and a circular buffer example using a separate RAM.     

Interpretations of open default theories in non-monotonic logics

It is shown that the translation of an open default into a modal formula x(L(x)LM ₁ (x)...LM _m (x)w(x)) gives rise to an embedding of open default systems into non-monotonic logics.     

On Solvability of Operator Inclusions: Application to Elliptic Problems with the Neumann Boundary Condition

In studying the surjectivity of set-valued mappings, a modification of the acute-angle lemma (or the equilibrium theorem) is used. This allows one to weaken the coerciveness condition. Some applications to differential equations (inclusions) with Neumann boundary conditions are considered on Sobolev spaces W _p ¹() in which operators are used that are not coercive in the classical sense.     

Exploiting transition locality in automatic verification of finite-state concurrent systems

In this paper we show that statistical properties of the transition graph of a system to be verified can be exploited to improve memory or time performances of verification algorithms.We show experimentally that protocols exhibit transition locality. That is, with respect to levels of a breadth-first state space exploration, state transitions tend to be between states belonging to close levels of the transition graph. We support our claim by measuring transition locality for the set of protocols included in the Mur verifier distribution .We present a cache-based verification algorithm that exploits transition locality to decrease memory usage and a disk-based verification algorithm that exploits transition locality to decrease disk read accesses, thus reducing the time overhead due to disk usage. Both algorithms have been implemented within the Mur verifier.Our experimental results show that our cache-based algorithm can typically save more than 40% of memory with an average time penalty of about 50% when using (Mur) bit compression and 100% when using bit compression and hash compaction, whereas our disk-based verification algorithm is typically more than ten times faster than a previously proposed disk-based verification algorithm and, even when using 10% of the memory needed to complete verification, it is only between 40 and 530% (300% on average) slower than (RAM) Mur with enough memory to complete the verification task at hand. Using just 300 MB of memory our disk-based Mur was able to complete verification of a protocol with about 10⁹ reachable states. This would require more than 5 GB of memory using standard Mur .     

Parallelizing the Murϕ Verifier

With the use of state and memory reduction techniques in verification by explicit state enumeration, runtime becomes a major limiting factor. We describe a parallel version of the explicit state enumeration verifier Mur for distributed memory multiprocessors and networks of workstations using the message passing paradigm. In experiments with three complex cache coherence protocols on an Sp2 multiprocessor and on a network of workstations at UC Berkeley, parallel Mur shows close to linear speedups, which are largely insensitive to communication latency and bandwidth. There is some slowdown with increasing communication overhead, for which a simple yet relatively accurate approximation formula is given. Techniques to reduce overhead and required bandwidth and to allow heterogeneity and dynamically changing load in the parallel machine are discussed, which we expect will allow good speedups when using conventional networks of workstations.     

Hierarchy theorems for two-way finite state transducers

Summary For a family of languages , CAL() is defined as the family of images of under nondeterministic two-way finite state transducers, while FINITE · VISIT() is the closure of under deterministic two-way finite state transducers; CAL⁰()= and for n0, CAL ⁿ⁺¹()=CAL ⁿ (CAL()). For any semiAFL , if FINITE · VISIT() CAL(), then CAL ⁿ () forms a proper hierarchy and for every n0, FINITE · VISIT(CALⁿ()) CAL ⁿ⁺¹() FINITE · VISIT(CAL ⁿ⁺¹()). If is a SLIP semiAFL or a weakly k-iterative full semiAFL or a semiAFL contained in any full bounded AFL, then FINITE · VISIT() CAL() and in the last two cases, FINITE · VISIT(). If is a substitution closed full principal semiAFL and FINITE · VISIT(), then FINITE · VISIT() CAL(). If is a substitution closed full principal semiAFL generated by a language without an infinite regular set and ₁ is a full semiAFL, then is contained in CAL^m(₁) if and only if it is contained in ₁. Among the applications of these results are the following. For the following families , CAL ⁿ () forms a proper hierarchy: =INDEXED, =ETOL, and any semiAFL contained in CF. The family CF is incomparable with CAL ^m (NESA) where NESA is the family of one-way nonerasing stack languages and INDEXED is incomparable with CAL ^m (STACK) where STACK is the family of one-way stack languages.This work was supported in part by the National Science Foundation under Grants No. DCR74-15091 and MCS-78-04725     

Real-time recognition of substring repetition and reversal

Real-time multitape Turing machine algorithms are presented for recognizing the languages {wxyxz^*:|w|=r|x,|z| =t|x|} and {wxyx ^R _z ^*:|w|=r|x,|z| =t|x|} for fixedr, s, andt and for string-matching with forced mismatches.This research was supported in part by the National Science Foundation under Grant MCS77-06613 (first author) and the Bat-Sheva Fund (second author). Part of the work was conducted while the second author was at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York. A preliminary report was included in a paper the authors presented at the Seventeenth Annual IEEE Symposium on Foundations of Computer Science, Houston, Texas, October 1976.     

Backtracking Problem in the Traversal of an Unknown Directed Graph by a Finite Robot

A covering path in a directed graph is a path passing through all vertices and arcs of the graph, with each arc being traversed only in the direction of its orientation. A covering path exists for any initial vertex only if the graph is strongly connected. The traversal of an unknown graph implies that the topology of the graph is not a priori known, and we learn it only in the course of traversing the graph. This is similar to the problem of traversing a maze by a robot in the case where the plan of the maze is not available. If the robot is a general-purpose computer without any limitations on the number of its states, then traversal algorithms with the estimate O(nm) are known, where n is the number of vertices and m is the number of arcs. If the number of states is finite, then this robot is a finite automaton. Such a robot is an analogue of the Turing machine, where the tape is replaced by a graph and the cells are assigned to the graph vertices and arcs. The selection of the arc that has not been traversed yet among those originating from the current vertex is determined by the order of the outgoing arcs, which is a priori specified for each vertex. The best known traversal algorithms for a finite robot are based on constructing the output directed spanning tree of the graph with the root at the initial vertex and traversing it with the aim to find all untraversed arcs. In doing so, we face the backtracking problem, which consists in searching for all vertices of the tree in the order inverse to their natural partial ordering, i.e., from the leaves to the root. Therefore, the upper estimate of the algorithms is different from the optimal estimate O(nm) by the number of steps required for the backtracking along the outgoing tree. The best known estimate O(nm + n ²loglogn) has been suggested by the author in the previous paper [1]. In this paper, a finite robot is suggested that performs a backtracking with the estimate O(n ²log*(n)). The function log* is defined as an integer solution of the inequality 1 log₂ ^log*(n) < 2, where log ^t = log º log º ... º log (the superposition º is applied t – 1 times) is the tth compositional degree of the logarithm. The estimate O(nm + n ²log*(n)) for the covering path length is valid for any strongly connected graph for a certain (unfortunately, not arbitrary) order of the outgoing arcs. Interestingly, such an order of the arcs can be marked by symbols of the finite robot traversing the graph. Hence, there exists a robot that traverses the graph twice: first traversal with the estimate O(nm + n ²loglogn) and the second traversal with the estimate O(nm + n ²log*(n)).