Narrow Results

We introduce some new models of infinite-state transition systems. The basic model, called a (reversal-bounded) counter machine (CM), is a nondeterministic finite automaton augmented with finitely many reversal-bounded counters (i.e. each counter can be incremented or decremented by 1 and tested for zero, but the number of times it can change mode from nondecreasing to nonincreasing and vice-versa is bounded by a constant, independent of the computation). We extend a CM by augmenting it with some familiar data structures: (i) A pushdown counter machine (PCM) is a CM augmented with an unrestricted pushdown stack. (ii) A tape counter machine (TCM) is a CM augmented with a two-way read/write worktape that is restricted in that the number of times the head crosses the boundary between any two adjacent cells of the worktape is bounded by a constant, independent of the computation (thus, the worktape is finite-crossing). There is no bound on how long the head can remain on a cell. (iii) A queue counter machine (QCM) is a CM augmented with a queue that is restricted in that the number of alternations between non-deletion phase and non-insertion phase on the queue is bounded by a constant. A non-deletion (non-insertion) phase is a period consisting of insertions (deletions) and no-changes, i.e., the queue is idle. We show that emptiness, (binary, forward, and backward) reachability, nonsafety, and invariance for these machines are solvable. We also look at extensions of the models that allow the use of linear-relation tests among the counters and parameterized constants as "primitive" predicates. We investigate the conditions under which these problems are still solvable.

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 give a brief survey of results that use “reversal-bounded counters” in studying reachability problems for various classes of transition systems. We also discuss the connection between the decidability of reachability in counter machines and the solvability of certain Diophantine equations.

Recently, it has been shown that for any higher order pushdown system and for any regular set of configurations, the set , is regular. In this paper, we give an alternative proof of this result for second order automata. Our construction of automaton for recognizing is explicit. The termination of saturation procedure used is obvious. It gives EXPTIME bound on size of the automaton recognizing if there is no alternation present in and in the automaton recognizing .

Semilinearity plays a key role not only in formal languages but also in the study of Petri nets. Although the reachability set of a Petri net may not be semilinear in general, there are a wide variety of subclasses of Petri nets which enjoy having semilinear reachability sets. In this paper, we develop sufficient conditions for Petri nets under which semilinearity is guaranteed. Our approach, based on the idea of path decomposition, can be used for consolidating several existing semilinearity results as well as for deriving new results all under the same framework.

We study subset reachability in nondeterministic finite automata and look for bounds of the length of the shortest reaching words for automata with a fixed number of states. We obtain such bounds for nondeterministic automata over 2-letter, 3-letter and arbitrary alphabets.^a

State explosion is a fundamental problem in the analysis and synthesis of discrete event systems. Continuous Petri nets can be seen as a relaxation of the corresponding discrete model. The expected gains are twofold: improvements in complexity and in decidability. In the case of autonomous nets we prove that liveness or deadlock-freeness remain decidable and can be checked more efficiently than in Petri nets. Then we introduce time in the model which now behaves as a dynamical system driven by differential equations and we study it w.r.t. expressiveness and decidability issues. On the one hand, we prove that this model is equivalent to timed differential Petri nets which are a slight extension of systems driven by linear differential equations (LDE). On the other hand, (contrary to the systems driven by LDEs) we show that continuous timed Petri nets are able to simulate Turing machines and thus that basic properties become undecidable.

This paper describes a weighted finite-state transducer composition algorithm that generalizes the concept of the composition filter and presents various filters that process epsilon transitions, look-ahead along paths, and push forward labels along epsilon paths. These filters, either individually or in combination, make it possible to compose some transducers much more efficiently in time and space than otherwise possible. We present examples of this drawn, in part, from demanding speech-processing applications. The generalized composition algorithm and many of these filters have been included in Open-Fst, an open-source weighted transducer library.

In this work we present an algorithm for solving the reachability problem in finite systems that are modelled with process algebras. Our method is based on Static Analysis, in particular, Data Flow Analysis, of the syntax of a process algebraic system with multi-way synchronisation. The results of the Data Flow Analysis are used in order to build a set of Horn clauses whose least model corresponds to an overapproximation of the reachable states. The computed model can be refined after each transition, and the algorithm runs until either a state whose reachability should be checked is encountered or it is not in the least model for all constructed states and thus is definitely unreachable. The advantages of the algorithm are that in many cases only a part of the Labelled Transition System will be built which leads to lower time and memory consumption. Also, it is not necessary to save all the encountered states which leads to further reduction of the memory requirements of the algorithm.

We define a subclass of Petri nets called m–state n–cycle Petri nets, each of which can be thought of as a ring of n bounded (by m states) Petri nets using n potentially unbounded places as joins. Let Ring(n, l, m) be the class of m–state n–cycle Petri nets in which the largest integer mentioned can be represented in l bits (when the standard binary encoding scheme is used). As it turns out, both the reachability problem and the boundedness problem can be decided in O(n(l+log m)) nondeterministic space. Our results provide a slight improvement over previous results for the so-called cyclic communicating finite state machines. We also compare and contrast our results with that of VASS(n, l, s), which represents the class of n-dimensional s-state vector addition systems with states where the largest integer mentioned can be described in l bits.

We present a geometric approach to the study of singular switched linear systems, defining a Lie group action on the differentiable manifold consisting of the matrices defining their subsystems with orbits coinciding with equivalence classes under an equivalence relation which preserves reachability and derive miniversal (orthogonal) deformations of the system. We relate this with some new results on reachability of such systems.

In order to research the localization problem of information source in a social network, this paper first constructs a complex network node model (Random-Susceptible-Infected-Recovered, R-SIR) based on cellular automata theory, and then utilizes this model to calculate the number of forwarding paths from a node to other forwarding nodes and the probability of occurrence of such forwarding paths, and presents an information source search method based on node reachability measure to locate the information distribution source in the information forwarding network. Theoretical analysis indicates that the algorithm, on the one hand, can avoid the time complexity problem brought by the maximum likelihood estimation, and on the other hand, overcome the inaccuracy problem of step number estimation in accessibility measure. Experimental results show that the algorithm has higher recognition rate and recognition accuracy for the information source in a multi-node network, and can search the information source, and is of great significance for the privacy protection of personal data.

We consider the following matrix reachability problem: given r square matrices with entries in a semiring, is there a product of these matrices which attains a prescribed matrix? Similarly, we define the vector (resp. scalar) reachability problem, by requiring that the matrix product, acting by right multiplication on a prescribed row vector, gives another prescribed row vector (resp. when multiplied on the left and right by prescribed row and column vectors, gives a prescribed scalar). We show that over any semiring, scalar reachability reduces to vector reachability which is equivalent to matrix reachability, and that for any of these problems, the specialization to any r ≥ 2 is equivalent to the specialization to r = 2. As an application of these reductions and of a theorem of Krob, we show that when r = 2, the vector and matrix reachability problems are undecidable over the max-plus semiring (ℤ∪{-∞}, max,+). These reductions also improve known results concerning the classical zero corner problem. Finally, we show that the matrix, vector, and scalar reachability problems are decidable over semirings whose elements are "positive", like the tropical semiring (ℤ∪{+∞}, min,+).

Our aim is twofold: First, we rigorously analyse the generators of quantum-dynamical semigroups of thermodynamic processes. We characterise a wide class of gksl-generators for quantum maps within thermal operations and argue that every infinitesimal generator of (a one-parameter semigroup of) Markovian thermal operations belongs to this class. We completely classify and visualise them and their non-Markovian counterparts for the case of a single qubit. Second, we use this description in the framework of bilinear control systems to characterise reachable sets of coherently controllable quantum systems with switchable coupling to a thermal bath. The core problem reduces to studying a hybrid control system (“toy model”) on the standard simplex allowing for two types of evolution: (i) instantaneous permutations and (ii) a one-parameter semigroup of $d$-stochastic maps. We generalise upper bounds of the reachable set of this toy model invoking new results on thermomajorisation. Using tools of control theory we fully characterise these reachable sets as well as the set of stabilisable states as exemplified by exact results in qutrit systems.

The purpose of this work is to introduce the concept of fuzzy regular languages (FRL) accepted by fuzzy finite automata, and try to introduce the categorical look of fuzzy languages where the codomain of membership functions are taken as a complete residuated lattice, instead of $[0,1]$. Also, we have introduced pumping lemma for FRL, which is used to establish a necessary and sufficient condition for a given fuzzy languages to be non-constant.

Given a tree T, a configuration of T is denoted by which represents that there is a robot at the vertex u, a hole at the vertex v and obstacles in the remaining vertices of T. By an mRJ move we mean that the robot is moved from the vertex u to a vertex v having a hole by jumping over m obstacles along a path. The case m = 0 is a simple move of taking the robot from u to the adjacent vertex v with a hole. We investigate the problem of moving a robot from its initial position to all the other vertices using mRJ moves (for some fixed m) in addition to simple moves. A tree is said to be mRJ reachable if there exists a configuration from which it is possible to take the robot to any vertex of the tree using simple or mRJ moves. A connected graph is 1RJ reachable. However, for m ≥ 2 there exists graphs that are not mRJ reachable. We characterize 2RJ and 3RJ reachable trees and give bound for the diameter of mRJ reachable trees.

This article deals with the intrinsic complexity of tracing and reachability questions in the context of elementary geometric constructions. We consider constructions from elementary geometry as dynamic entities: while the free points of a construction perform a continuous motion the dependent points should move consistently and continuously. We focus on constructions that are entirely built up from join, meet and angular bisector operations. In particular the last operation introduces an intrinsic ambiguity: Two intersecting lines have two different angular bisectors. Under the requirement of continuity it is a fundamental algorithmic problem to resolve this ambiguity properly during motions of the free elements.

After formalizing this intuitive setup we prove the following main results of this article:

• It is NP-hard to trace the dependent elements in such a construction.

• It is NP-hard to decide whether two instances of the same construction lie in the same component of the configuration space.

• The last problem becomes PSPACE-hard if we allow one additional sidedness test which has to be satisfied during the entire motion.

On the one hand the results have practical relevance for the implementations of Dynamic Geometry Systems. On the other hand the results can be interpreted as statements concerning the intrinsic complexity of analytic continuation.