International Journal of Foundations of Computer Science

Live sequence charts (LSCs) have been defined recently as an extension of message sequence charts (MSCs; or their UML variant, sequence charts (MSCs; or their UML variant, sequence diagrams) for rich inter-object specification. One of the main additions is the notion of universal charts and hot, mandatory behavior, which, among other things, enables one to specify forbidden scenarios. LSCs are thus essentially as expressive as statecharts. This paper deals with synthesis, which is the problem of deciding, given an LSC specification, if there exists a satisfying object system and, if so, to synthesize one automatically. The synthesis problem is crucial in the development of complex systems, since sequence diagrams serve as the manifestation of use cases — whether used formally or informally — and if synthesizable they could lead directly to implementation. Synthesis is considerably harder for LSCs than for MSCs, and we tackle it by defining consistency, showing that an entire LSC specification is consistent iff it is satisfiable by a state-based object system, and them synthesizing a satisfying system as a collection of finite state machines or statecharts.

Vector algorithms allow the computation of an output vector r = r₁ r₂ ⋯ r_m given an input vector e = e₁ e₂ ⋯ e_m in a bounded number of operations, independent of m the length of the vectors. The allowable operations are usually restricted to bit-wise operations available in processors, including shifts and binary addition with carry. These restrictions imple that the existence of a vector algorithm for a particular problem opens the way to extremely fast implementations, using the inherent parallelism of bit-wise operations.

This paper presents general results on the existence and construction of vertor algorithms, with a particular focus on problems arising from computational biology. We show that efficient vector algorithms exist for the problem of approximate string matching with arbitrary weighted distances, generalizing a previous result by G. Myers. We also characterize a class of automata for which vector algorithms can be automatically derived from the transition table of the automata.

We establish that regularly extended two-way nondeterministic tree automata with unranked alphabets have the same expressive power as regularly extended nondeterministic tree automata with unranked alphabets alphabets. We obtain this results by establishing regularly extended versions of a congruence on trees and of a congruence on, so called, views. Our motivation for the study of these tree models is the Extensible Markup Language (XML), a metalanguage for defining document grammars. Such grammars have regular sets of right-hand sides for their productions and tree automata provide an alternative and useful modeling tool for them. In particular, we believe that they provide a useful computational model for what we call caterpillar expressions.

The concept of cover automata for finite languages was formally introduced in [3]. Cover automata have been studied as an efficient representation of finite languages. In [3], an algorithm was given to transform a DFA that accepts a finite language to a minimal deterministic finite cover automaton (DFCA) with the time complexity O(n⁴), where n is the number of states of the given DFA. In this paper, we review the basic concept of cover automata and describe a new efficient transformation algorithm with the time complexity O(n²), which is a significant improvement from the previous algorithm.

The aim of this paper is to compare three efficient representations of the position automaton of a regular expression: the Thompson ∊-automaton, the -structure and the ℱ-structure, an optimization of the -structure. These representations are linear w.r.t. the size s of the expression, since their construction is in O(s) space and time, as well as the computation of the set δ(X,a) of the targets of the transitions by a of any subset X of states. The comparison is based on the evaluation of the number of edges of the underlying graphs respectively created by the construction step or visited by the computation of a set δ(X,a).

We look at a model of a queue system which consists of two nondeterministic finite-state machines, each augmented with "reversal-bounded" counters, connected by an unbounded queue. One machine (the "writer") can send messages to the other (the "reader") via the queue. There is no central control, but the machines operate synchronously and share the same global clock. Unlike in the traditional model, the writer can make conditional moves that test the emptiness of the queue. We investigate the decidability of various verification problems, e.g., (binary, forward, backward) reachability, safety, and blocking. We also look at extensions of the model: allowing the writer to also test for queue emptiness, adding a pushdown stack to one or both of the machines, allowing multiple queues or two-way communication, etc. Finally, we consider some reachability questions concerning machines operating in parallel.

We present a new generic ∊-removal algorithm for weighted automata and transducers defined over a semiring. The algorithm can be used with any semiring covered by our framework and works with any queue discipline adopted. It can be used in particular in the case of unweighted automata and transducers and weighted automata and transducers defined over the tropical semiring. It is based on a general shortest-distance algorithm that we briefly describe. We give a full description of the algorithm including its pseudocode and its running time complexity, discuss the more efficient case of acyclic automata, an on-the-fly implementation of the algorithm and an approximation algorithm in the case of the semirings not covered by our framework. We illustrate the use of the algorithm with several semirings. We also describe an input ∊-normalization algorithm for weighted transducers based on the general shortest-distance algorithm. The algorithm, which works with all semirings covered by our framework, admits an on-the-fly implementation.

In this paper we give the cost, in terms of states, of some basic operations (union, intersection, concatenation, and Kleene star) on regular languages in the unary case (where the alphabet contains only one symbol). These costs are given by explicitly determining the number of states in the noncyclic and cyclic parts of the resulting automata. Furthermore, we prove that our bounds are optimal. We also present an interesting connection to Jacobsthal's function from number theory.