Search

We look at nondeterministic finite automata augmented with multiple reversal-bounded counters where, during an accepting computation, the behavior of the counters is specified by some fixed pattern. These patterns can serve as a useful "bridge" to other important automata and grammar models in the theoretical computer science literature, thereby helping in their study. Various pattern behaviors are considered, together with characterizations and comparisons. For example, one such pattern defines exactly the smallest full trio containing all the bounded semilinear languages. Another pattern defines the smallest full trio containing all the bounded context-free languages. The "bridging" to other families is then applied, e.g. to certain Turing machine restrictions, as well as other families. Certain general decidability properties are also studied using this framework., 28 pages, 1 figure

Techniques are developed for creating new and general language families of only semilinear languages, and for showing families only contain semilinear languages. It is shown that for language families L that are semilinear full trios, the smallest full AFL containing L that is also closed under intersection with languages in NCM (where NCM is the family of languages accepted by NFAs augmented with reversal-bounded counters), is also semilinear. If these closure properties are effective, this also immediately implies decidability of membership, emptiness, and infiniteness for these general families. From the general techniques, new grammar systems are given that are extensions of well-known families of semilinear full trios, whereby it is implied that these extensions must only describe semilinear languages. This also implies positive decidability properties for the new systems. Some characterizations of the new families are also given., Comment: 20 pages

The family, L(INDLIN), of languages generated by linear indexed grammars has been studied in the literature. It is known that the Parikh image of every language in L(INDLIN) is semi-linear. However, there are bounded semi linear languages that are not in L(INDLIN). Here, we look at larger families of (restricted) indexed languages and study their properties, their relationships, and their decidability properties., Comment: 16 pages, latest version

This paper examines several measures of space complexity on variants of stack automata: non-erasing stack automata and checking stack automata. These measures capture the minimum stack size required to accept any word in a language (weak measure), the maximum stack size used in any accepting computation on any accepted word (accept measure), and the maximum stack size used in any computation (strong measure). We give a detailed characterization of the accept and strong space complexity measures for checking stack automata. Exactly one of three cases can occur: the complexity is either bounded by a constant, behaves (up to small technicalities explained in the paper) like a linear function, or it grows arbitrarily larger than the length of the input word. However, this result does not hold for non-erasing stack automata; we provide an example when the space complexity grows with the square root of the input length. Furthermore, an investigation is done regarding the best complexity of any machine accepting a given language, and on decidability of space complexity properties.

We study counting-regular languages — these are languages L for which there is a regular language L ′ such that the number of strings of length n in L and L ′ are the same for all n. We show that the languages accepted by unambiguous nondeterministic Turing machines with a one-way read-only input tape and a reversal-bounded worktape are counting-regular. Many one-way acceptors are a special case of this model, such as reversal-bounded deterministic pushdown automata, reversal-bounded deterministic queue automata, and many others, and therefore all languages accepted by these models are counting-regular. This result is the best possible in the sense that the claim does not hold for either 2-ambiguous NPDA 's, unambiguous NPDA 's with no reversal-bound, and other models. We also study closure properties of counting-regular languages, and we study decidability problems in regards to counting-regularity. For example, it is shown that the counting-regularity of even some restricted subclasses of NPDA 's is undecidable. Lastly, k-slender languages — where there are at most k words of any length — are also studied. Amongst other results, it is shown that it is decidable whether a language in any semilinear full trio is k-slender.

A language [Formula: see text] is said to be dense if every word in the universe is an infix of some word in [Formula: see text]. This notion has been generalized from the infix operation to arbitrary word operations [Formula: see text] in place of the infix operation ([Formula: see text]-dense, with infix-dense being the standard notion of dense). It is shown here that it is decidable, for a language [Formula: see text] accepted by a one-way nondeterministic reversal-bounded pushdown automaton, whether [Formula: see text] is infix-dense. However, it becomes undecidable for both deterministic pushdown automata (with no reversal-bound), and for nondeterministic one-counter automata. When examining suffix-density, it is undecidable for more restricted families such as deterministic one-counter automata that make three reversals on the counter, but it is decidable with less reversals. Other decidability results are also presented on dense languages, and contrasted with a marked version called [Formula: see text]-marked-density. Also, new languages are demonstrated to be outside various deterministic language families after applying different deletion operations from smaller families. Lastly, bounded-dense languages are defined and examined.

We prove new decidability and undecidability results concerning the finite-ambiguity problem in acceptors, and the finite-valuedness and lossiness problems in transducers. The acceptors and transducers we study have infinite memory.

We present general results that are useful in showing closure and decidable properties of large classes of languages with respect to biologically-inspired operations. We use these results to prove new decidability results and closure properties of some classes of languages under bio-operations such hairpin-inversion, the recently studied operation of pseudo-inversion, and other bio-operations. We also provide techniques for proving undecidability results. In particular, we give a new approach for proving the undecidability of problems for which the usual method of reduction to the undecidability of the Post Correspondence Problem seems hard to apply. Our closure and decidability results strengthen or generalize previous results.

Techniques are developed for creating new and general language families of only semilinear languages, and for showing families only contain semilinear languages. It is shown that for language families \(\mathcal{L}\) that are semilinear full trios, the smallest full AFL containing the languages obtained by intersecting languages in \(\mathcal{L}\) with languages in \(\mathsf{NCM}\) (where \(\mathsf{NCM}\) is the family of languages accepted by \(\textsf {NFA}\)s augmented with reversal-bounded counters), is also semilinear. If these closure properties are effective, this also immediately implies decidability of membership, emptiness, and infiniteness for these general families. From the general techniques, new grammar systems are given that are extensions of well-known families of semilinear full trios, whereby it is implied that these extensions must only describe semilinear languages. This also implies positive decidability properties for the new systems. Some characterizations of the new families are also given.

We introduce a model of one-way language acceptors (a variant of a checking stack automaton) and show the following decidability properties: 1. The deterministic version has a decidable membership problem but has an undecidable emptiness problem. 2. The nondeterministic version has an undecidable membership problem and emptiness problem. There are many models of accepting devices for which there is no difference with these problems between deterministic and nondeterministic versions, i.e., the membership problem for both versions are either decidable or undecidable, and the same holds for the emptiness problem. As far as we know, the model we introduce above is the first one-way model to exhibit properties (1) and (2). We define another family of one-way acceptors where the nondeterministic version has an undecidable emptiness problem, but the deterministic version has a decidable emptiness problem. We also know of no other model with this property in the literature. We also investigate decidability properties of other variations of checking stack automata (e.g., allowing multiple stacks, two-way input, etc.). Surprisingly, two-way deterministic machines with multiple checking stacks and multiple reversal-bounded counters are shown to have a decidable membership problem, a very general model with this property.

Given an n-tape automaton M with a one-way read-only head per tape and a right end marker $ on each tape, we say that M is aligned or 0-synchronized (or simply, synchronized) if for every n-tuple x = (x1,…, xn) that is accepted, there is a computation on x such that at any time during the computation, all heads, except those that have reached the end marker, are on the same position. When a head reaches the marker, it can no longer move. As usual, an n-tuple x = (x1,…, xn) is accepted if M eventually reaches the configuration where all n heads are on $ in an accepting state. In two recent papers, we looked at the problem of deciding, given an n-tape automaton of a given type, whether there exists an equivalent synchronized n-tape automaton of the same type. In this paper, we exhibit various classes of multitape automata which can(not) be converted to equivalent synchronized multitape automata.

In his 1966 book, ''The Mathematical Theory of Context-Free Languages'', S. Ginsburg posed the following open problem: Find a decision procedure for determining if an arbitrary semilinear set is a finite union of stratified linear sets. It turns out that this problem (which remains open) is equivalent to the problem of synchronizability of multitape machines. Given an n-tape automaton M of a given type (e.g., nondeterministic pushdown automaton (NPDA), nondeterministic finite automaton (NFA), etc.) with a one-way read-only head per tape and a right end marker on each tape, we say that M is 0-synchronized (or aligned) if for every n-tuple x=(x"1,...,x"n) that is accepted, there is an accepting computation on x such that at any time during the computation, all heads except those that have reached the end marker are on the same position (i.e., aligned). One of our main contributions is to show that Ginsburg@?s problem is equivalent to deciding for an arbitrary n-tape NFA M accepting L(M)@?a"1^@?x...xa"n^@? (where n>=1 and a"1,...,a"n are distinct symbols) whether there exists an equivalent 0-synchronized n-tape NPDA M^'. Ginsburg@?s problem is decidable if M^' is required to be an NFA, and we will generalize this decidability over bounded inputs. It is known that if the inputs are unrestricted, the problem is undecidable. We also show several other related decidability and undecidability results. It may appear, as one of the referees suggested in an earlier version of this paper, that our main result can be written in first order logic. We explain why this is not the case in the Introduction.

We introduce a model of one-way language acceptors (a variant of a checking stack automaton) and show the following decidability properties: 1. The deterministic version has a decidable membership problem but has an undecidable emptiness problem. 2. The nondeterministic version has an undecidable membership problem and emptiness problem.

The family, \({\mathsf{{\mathcal {L}}(IND_{LIN})}}\), of languages generated by linear indexed grammars has been studied in the literature. It is known that the Parikh image of every language in \({\mathsf{{\mathcal {L}}(IND_{LIN})}}\) is semi-linear. However, there are bounded semi-linear languages that are not in \({\mathsf{{\mathcal {L}}(IND_{LIN})}}\). Here, we look at larger families of (restricted) indexed languages and study their properties, their relationships, and their decidability properties.

Verification of string manipulation operations is a crucial problem in computer security. In this paper, we present a new relational string verification technique based on multi-track automata. Our approach is capable of verifying properties that depend on relations among string variables. This enables us to prove that vulnerabilities that result from improper string manipulation do not exist in a given program. Our main contributions in this paper can be summarized as follows: (1) We formally characterize the string verification problem as the reachability analysis of string systems and show decidability/undecidability results for several string analysis problems. (2) We develop a sound symbolic analysis technique for string verification that over-approximates the reachable states of a given string system using multi-track automata and summarization. (3) We evaluate the presented techniques with respect to several string analysis benchmarks extracted from real web applications.

We consider transition P systems as originally defined in the seminal paper of Gh. Păun, where he introduced the field of membrane computing. We show that it is decidable to determine, given a P system Π, whether it is strongly reversible (i.e., every configuration has at most one direct predecessor), resolving in the affirmative a recent open problem in the field. We also show that the set of all direct predecessors of a given configuration in a P system is an effectively computable semilinear set, which can effectively be expressed as a Presburger formula, strengthening an early result in the literature. We also prove other related results.

Targeting at modeling the high-level dynamics of pervasive computing systems, we introduce bond computing systems (BCS) consisting of objects, bonds and rules. Objects are typed but addressless representations of physical or logical (computing and communicating) entities. Bonds are typed multisets of objects. In a BCS, a configuration is specified by a multiset of bonds, called a collection. Rules specify how a collection evolves to a new one. A BCS is a variation of a P system introduced by Gheorghe Paun where, roughly, there is no maximal parallelism but with typed and unbounded number of membranes, and hence, our model is also biologically inspired. In this paper, we focus on regular bond computing systems (RBCS), where bond types are regular, and study their computation power and verification problems. Among other results, we show that the computing power of RBCS lies between linearly bounded automata (LBA) and LBC (a form of bounded multicounter machines) and hence, the regular bond-type reachability problem (given an RBCS, whether there is some initial collection that can reach some collection containing a bond of a given regular type) is undecidable. We also study a restricted model (namely, B-boundedness) of RBCS where the reachability problem becomes decidable.

We introduce the notion of stateless multihead two-way (respectively, one-way) NFAs and stateless multicounter systems and relate them to P systems and vector addition systems. In particular, we investigate the decidability of the emptiness and reachability problems for these stateless automata and show that the results are applicable to similar questions concerning certain variants of P systems, namely, token systems and sequential tissue-like P systems.

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.

We look at the recently introduced neural-like systems, called SN P systems. These systems incorporate the ideas of spiking neurons into membrane computing. We study various classes and characterize their computing power and complexity. In particular, we analyze asynchronous and sequential SN P systems and present some conditions under which they become (non-)universal. The non-universal variants are characterized by monotonic counter machines and partially blind counter machines and, hence, have many decidable properties. We also investigate the language-generating capability of SN P systems.

The complexity and decidability of various decision problems involving the shuffle operation are studied. The following three problems are all shown to be $NP$-complete: given a nondeterministic finite automaton (NFA) $M$, and two words $u$ and $v$, is $L(M)$ not a subset of $u$ shuffled with $v$, is $u$ shuffled with $v$ not a subset of $L(M)$, and is $L(M)$ not equal to $u$ shuffled with $v$? It is also shown that there is a polynomial-time algorithm to determine, for $NFA$s $M_1, M_2$ and a deterministic pushdown automaton $M_3$, whether $L(M_1)$ shuffled with $L(M_2)$ is a subset of $L(M_3)$. The same is true when $M_1, M_2,M_3$ are one-way nondeterministic $l$-reversal-bounded $k$-counter machines, with $M_3$ being deterministic. Other decidability and complexity results are presented for testing whether given languages $L_1, L_2$ and $R$ from various languages families satisfy $L_1$ shuffled with $L_2$ is a subset of $R$, and $R$ is a subset of $L_1$ shuffled with $L_2$. Several closure results on shuffle are also shown., Comment: Preprint submitted to Information and Computation

We look at a 1-membrane catalytic P system with evolution rules of the form Ca → Cv or a → v, where C is a catalyst, a is a noncatalyst symbol, and v is a (possibly null) string representing a multiset of noncatalyst symbols. (Note that we are only interested in the multiplicities of the symbols.) A catalytic system (CS) can be regarded as a language acceptor in the following sense. Given an input alphabet Σ consisting of noncatalyst symbols, the system starts with an initial configuration wz, where w is a fixed string of catalysts and noncatalysts not containing any symbol in z, and z = a1n1...aknk for some nonnegative integers n1,..., nk, with (a1,...,ak) ⊆ Σ. At each step, a maximal multiset of rules is nondeterministically selected and applied in parallel to the current configuration to derive the next configuration (note that the next configuration is not unique, in general). The string z is accepted if the system eventually halts.It is known that a 1-membrane CS is universal in the sense that any unary recursively enumerable language can be accepted by a 1-membrane CS (even by purely CSs, i.e., when all rules are of the form Ca → Cv). A CS is said to be deterministic if at each step there is a unique maximally parallel multiset of rules applicable. It has been an open problem whether deterministic systems of this kind are universal. We answer this question negatively. We show that the membership problem for deterministic CSs is decidable. In fact, we show that the Parikh map of the language (⊆a1*...ak*) accepted by any deterministic CS is a simple semilinear set which can be effectively constructed. Since nondeterministic 1-membrane CS acceptors (with two catalysts) are universal, our result gives the first example of a variant of P systems for which the nondeterministic version is universal, but the deterministic version is not.We also show that for a deterministic 1-membrane CS using only rules of type Ca → Cv, the set of reachable configurations from a given initial configuration is an effective semilinear set. The application of rules of type a → v, however, is sufficient to render the reachability set nonsemilinear. Our results generalize to multimembrane deterministic CSs. We also consider deterministic CSs which allow rules to be prioritized and investigate three classes of such systems, depending on how priority in the application of the rules is interpreted. For these three prioritized systems, we obtain contrasting results: two are universal and one only accepts semilinear sets.

For 1 ≤ i ≤ k, let Ri denote pi(y)Fi + Gi, where pi(y) is a polynomial in y with integer coefficients, and Fi, Gi are linear polynomials in x1,..., xn with integer coefficients. Let P(z1,..., zk) be a Presburger relation over the nonnegative integers. We show that the following problem is decidable:Given: R1,..., Rk and a Presburger relation P.Question: Are there nonnegative integer values for y, x1,..., xn such that for these values, (R1,..., Rk) satisfies P? We also give some applications to decision problems concerning counter machines.

We show an interesting connection between two-way deterministic finite automata with monotonic counters and quadratic Diophantine equations. The automaton M operates on inputs of the form a1i1...anin for some fixed n and distinct symbols a1,...,an, where i1,...,in are nonnegative integers. We consider the following reachability problem: given a machine M, a state q, and a Presburger relation E over counter values, is there (i1,...,in) such that M, when started in its initial state on the left end of the input a1i1...anin with all counters initially zero, reaches some configuration where the state is q and the counter values satisfy E? In particular, we look at the case when the relation E is an equality relation, i.e., a conjunction of relations of the form Ci = Cj. We show that this case and variations of it are equivalent to the solvability of some special classes of systems of quadratic Diophantine equations. We also study the nondeterministic version of two-way finite automata augmented with monotonic counters with respect to the reachability problem. Finally, we introduce a technique which uses decidability and undecidability results to show "separation" between language classes.

We consider generalized discrete timed automata with general linear relations over clocks and parameterized constants as clock constraints and with parameterized durations. We look at three approximation techniques (i.e., the r-reset-bounded approximation, the B-bounded approximation, and the 〈B,r〉-crossing-bounded approximation), and derive automata-theoretic characterizations of the binary reachability under these approximations. The characterizations allow us to show that the safety analysis problem is decidable for generalized discrete timed automata with unit durations and for deterministic generalized discrete timed automata with parameterized durations. An example specification written in ASTRAL is used to run a number of experiments using one of the approximation techniques.

A language L is said to be dense if every word in the universe is an infix of some word in L. This notion has been generalized from the infix operation to arbitrary word operations \(\varrho \) in place of the infix operation (\(\varrho \)-dense, with infix-dense being the standard notion of dense). It is shown here that it is decidable, for a language L accepted by a one-way nondeterministic reversal-bounded pushdown automaton, whether L is infix-dense. However, it becomes undecidable for both deterministic pushdown automata (with no reversal-bound), and for nondeterministic one-counter automata. When examining suffix-density, it is undecidable for more restricted families such as deterministic one-counter automata that make three reversals on the counter, but it is decidable with less reversals. Other decidability results are also presented on dense languages, and contrasted with a marked version called \(\varrho \)-marked-density. Also, new languages are demonstrated to be outside various deterministic language families after applying different deletion operations from smaller families. Lastly, bounded-dense languages are defined and examined.

The complexity and decidability of various decision problems involving the shuffle operation (denoted by Open image in new window ) are studied. The following three problems are all shown to be \(\mathsf{NP}\)-complete: given a nondeterministic finite automaton (\(\mathsf{NFA}\)) \(M\), and two words \(u\) and \(v\), is Open image in new window , is Open image in new window , and is Open image in new window ? It is also shown that there is a polynomial-time algorithm to determine, for \(\mathsf{NFA}\)s \(M_1, M_2\) and a deterministic pushdown automaton \(M_3\), whether Open image in new window . The same is true when \(M_1, M_2,M_3\) are one-way nondeterministic \(l\)-reversal-bounded \(k\)-counter machines, with \(M_3\) being deterministic. Other decidability and complexity results are presented for testing whether given languages \(L_1, L_2\) and \(L\) from various languages families satisfy Open image in new window .

We show that it is decidable whether a transitive mixed linear relation has an ω-chain. Using this result, we study a number of liveness verification problems for generalized timed automata within a unified framework. More precisely, we prove that (1) the mixed linear liveness problem for a timed automaton with dense clocks, reversal-bounded counters, and a free counter is decidable, and (2) the Presburger liveness problem for a timed automaton with discrete clocks, reversal-bounded counters, and a pushdown stack is decidable.

We study various generalizations of reversal-bounded multicounter machines and show that they have decidable emptiness, infiniteness, disjointness, containment, and equivalence problems. The extensions include allowing the machines to perform linear-relation tests among the counters and parameterized constants (e.g., “Is 3x−5y−2D1+9D2

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 develop a new technique based on counter machines to study the containment and equivalence of queries with linear constraints over integers Z, natural numbers N, rational numbers Q, and real numbers R. We show that the problems are dedicable in exponential space with an exponential time lower bound for conjunctive queries with linear constraints. For a subclass, called SQL-like conjunctive queries, the problems are shown to have a polynomial space upper bound. We also use the counter machine technique to show that for a syntactically restricted subclass of first-order queries with linear constraints over Z and N, the containment and equivalence problems are undecidable for finite databases but decidable for a subclass of finite databases.

We provide an automata-theoretic approach to analyzing an abstract channel modeled by a transducer and to characterizing its lossy rates. In particular, we look at related decision problems and show the boundaries between the decidable and undecidable cases.

We prove new decidability and undecidability results concerning the finite-ambiguity problem in acceptors, and the finite-valuedness and lossiness problems in transducers. The acceptors and transducers we study have infinite memory.

We present general results that are useful in showing closure and decidable properties of large classes of languages with respect to biologically-inspired operations. We use these results to prove new decidability results and closure properties of some classes of languages under hairpin-inversion, pseudo-inversion, and other bio-operations. We also provide a new approach for proving the undecidability of problems involving bio-operations for which the usual method of reduction to the undecidability of the Post Correspondence Problem (PCP) may not be easy to apply. Our closure and decidability results strengthen or generalize previous results.

We survey the properties of automata augmented with reversal-bounded counters. In particular, we discuss the closure/non-closure properties of the languages accepted by these machines as well as the decidability/undecidability of decision problems concerning these devices. We also give applications to several problems in automata theory and formal languages.

Almost all the decision questions concerning the resource requirements of a computational device are undecidable. Here we want to understand the exact boundary that separates the undecidable from the decidable cases of such problems by considering the time complexity of very simple devices that include NFAs (1-way and 2-way), NPDAs and NPDAs augmented with counters - and their unambiguous restrictions. We consider several variations - based on whether the bound holds exactly or as an upper-bound and show decidability as well as undecidability results. We also introduce a stronger version of machine equivalence (known as run-time equivalence) and identify classes of machines for which run-time equivalence is decidable (undecidable). In the case of decidable problems, we also attempt to determine more precisely the complexity class to which the problem belongs.

We address several types of decision questions related to context-free languages when an NPDA is given as input. First we consider the question of whether the NPDA makes a bounded number of stack reversals (over all accepting inputs) and show that this problem is undecidable even when the NPDA is only 2-ambiguous. We consider the same problem for counter machines (i.e., whether the counter makes a bounded number of reversals) and show that it is also undecidable. On the other hand, we show that the problem is decidable for unambiguous NPDAs even when augmented with reversal-bounded counters. Next, we look at problems of equivalence, containment and disjointness with fixed languages. With the fixed language L0 being one of the following: P = $\{ x \# x^r \ | $x∈(0+1)* }, Pu = $\{ x x^r \ | $x∈(0+1)* }, Dk = Dyck language with k-type of parentheses, or Sk = two-sided Dyck language with k types of parentheses, we consider problems such as: 'Is L(M)∩L0 = ∅?', 'Is L(M)⊆L0?', or 'Is L(M) = L0?', where M is an input NPDA (or a restricted form of it). For example, we show that the problem, 'Is L(M)∩P?', is undecidable when M is a deterministic one-counter acceptor, while the problem 'Is L(M)⊆P?' is decidable even for NPDAs augmented with reversal-bounded counters. Another result is that the problem 'Is L(M)⊆Pu?' is decidable in polynomial time for M an NPDA. We also show several other related decidability and undecidability results.

The authors study some decision questions concerning two-way counter machines and obtain the strongest decidable results to date concerning these machines. In particular, it is shown that the emptiness, containment, and equivalence (ECE, for short) problems are decidable for two-way counter machines whose counter is reversal-bounded (i.e., the counter alternates between increasing and decreasing modes at most a fixed number of times). This result is used to give a simpler proof of a recent result in which the ECE problems for two-way reversal-bounded pushdown automata accepting bounded languages (i.e., subsets of $w_1^*\ldots w_k^*$ for some nonnull words $w_1,\ldots,w_k$) are decidable. Other applications concern decision questions about simple programs. Finally, it is shown that nondeterministic two-way reversal-bounded multicounter machines are effectively equivalent to finite automata on unary languages, and hence their ECE problems are decidable also.

Given an n-tape automaton M with a one-way read-only head per tape and a right end marker $ on each tape, we say that M is aligned or 0-synchronized (or simply, synchronized) if for every n-tuple x=(x1, …, xn) that is accepted, there is a computation on x such that at any time during the computation, all heads, except those that have reached the end marker, are on the same position. When a head reaches the marker, it can no longer move. As usual, an n-tuple x=(x1, …, xn) is accepted if M eventually reaches the configuration where all n heads are on $ in an accepting state. In two recent papers, we looked at the problem of deciding, given an n-tape automaton of a given type, whether there exists an equivalent synchronized n-tape automaton of the same type. In this paper, we exhibit various classes of multitape automata which can(not) be converted to equivalent synchronized multitape automata.

We explore the boundaries between decidability and undecidability of the containment and equivalence problems for restricted classes of nondeterministic generalized sequential machines (NGSMs), nondeterministic finite transducers (NFTs), nondeterministic pushdown transducers (NPDTs), and linear context-free grammars (LCFGs). We believe that our results are the sharpest known to date concerning these devices.

Motivated by applications to verification problems in string manipulating programs, we look at the problem of whether the heads in a multitape automaton are synchronized. Given an n-tape pushdown automaton M with a one-way read-only head per tape and a right end marker $ on each tape, and an integer k ≥ 0, we say that M is ksynchronized if at any time during any computation of M on any input n-tuple (x1, . . . , xn) (whether or not it is accepted), no pair of input heads that are not on $ are more than k cells apart. This requirement is automatically satisfied if one of the heads has reached $. Note that an n-tuple (x1, . . . , xn) is accepted if M reaches the configuration where all n heads are on $ and M is in an accepting state. The automaton can be deterministic (DPDA) or nondeterministic (NPDA) and, in the special case, may not have a pushdown stack (DFA, NFA). We obtain decidability and undecidability results for these devices for both one-way and two-way versions. We also consider the notion of k-synchronized oneway and two-way multihead automata and investigate similar problems.

We introduce what we believe to be the simplest known classes of language acceptors for which we can prove that decision problems (like universe, disjointness, containment, etc.) are undecidable. We also look at classes with undecidable decision problems and show that the problems become decidable for the "parameterized" versions of the machines.

In search for "realistic" bio-inspired computing models, we consider asynchronous spiking neural P systems, in the hope to get a class of computing devices with decidable properties. However, although the non-synchronization is known in general to decrease the computing power, in the case of using extended rules (several spikes can be produced by a rule) we obtain again the equivalence with Turing machines (interpreted as generators of sets of vectors of numbers). The problem remains open for the case of restricted spiking neural P systems, whose rules can only produce one spike. On the other hand, we prove that asynchronous spiking neural P systems, with a specific way of halting, using extended rules and where each neuron is either bounded or unbounded, are equivalent to partially blind counter machines and, therefore, have many decidable properties.

Targeting at modeling the high-level dynamics of pervasive computing systems, we introduce Bond Computing Systems (BCS) consisting of objects, bonds and rules. Objects are typed but addressless representations of physical or logical (computing and communicating) entities. Bonds are typed multisets of objects. In a BCS, a configuration is specified by a multiset of bonds, called a collection. Rules specifies how a collection evolves to a new one. A BCS is a variation of a P system introduced by Gheorghe Paun where, roughly, there is no maximal parallelism but with typed and unbounded number of membranes, and hence, our model is also biologically inspired. In this paper, we focus on regular bond computing systems (RBCS), where bond types are regular, and study their computation power and verification problems. Among other results, we show that the computing power of RBCS lies between LBA (linearly bounded automata) and LBC (a form of bounded multicounter machines) and hence, the regular bond-type reachability problem (given an RBCS, whether there is some initial collection that can reach some collection containing a bond of a given regular type) is undecidable. We also study some restricted models (namely, B-boundedness and 1-transfer) of RBCS where the reachability problem becomes decidable.

We look at a 1-membrane catalytic P system with evolution rules of the form Ca →Cv or a →v, where C is a catalyst, a is a noncatalyst symbol, and v is a (possibly null) string representing a multiset of noncatalyst symbols. (Note that we are only interested in the multiplicities of the symbols.) A catalytic system can be regarded as a language acceptor in the following sense. Given an input alphabet Σ consisting of noncatalyst symbols, the system starts with an initial configuration wz, where w is a fixed string of catalysts and noncatalysts not containing any symbol in z, and $z = a_1^{n_1} \ldots a_k^{n_k}$ for some nonnegative integers n1, ..., nk, with { a1 ...ak } ⊆∑. At each step, a maximal multiset of rules is nondeterministically selected and applied in parallel to the current configuration to derive the next configuration (note that the next configuration is not unique, in general). The string z is accepted if the system eventually halts. It is known that a 1-membrane catalytic system is universal in the sense that any unary recursively enumerable language can be accepted by a 1-membrane catalytic system (even by purely catalytic systems, i.e., when all rules are of the form Ca →Cv ). A catalytic system is said to be deterministic if at each step, there is a unique maximally parallel multiset of rules applicable. It has been an open problem whether deterministic systems of this kind are universal. We answer this question negatively: We show that the membership problem for deterministic catalytic systems is decidable. In fact, we show that the Parikh map of the language ( $\subseteq a_1^* \ldots a_k^*$ ) accepted by any deterministic catalytic system is a simple semilinear set which can be effectively constructed. Since nondeterministic 1-membrane catalytic system acceptors (with 2 catalysts) are universal, our result gives the first example of a variant of P systems for which the nondeterministic version is universal, but the deterministic version is not. We also show that for a deterministic 1-membrane catalytic system using only rules of type Ca →Cv, the set of reachable configurations from a given initial configuration is an effective semilinear set. The application of rules of type a →v, however, is sufficient to render the reachability set non-semilinear. Our results generalize to multi-membrane deterministic catalytic systems. We also consider deterministic catalytic systems which allow rules to be prioritized and investigate three classes of such systems, depending on how priority in the application of the rules is interpreted. For these three prioritized systems, we obtain contrasting results: two are universal and one only accepts semilinear sets.

Membrane computing is a branch of molecular computing that aims to develop models and paradigms that are biologically motivated. It identifies an unconventional computing model, namely a P system, from natural phenomena of cell evolutions and chemical reactions. Because of the nature of maximal parallelism inherent in the model, P systems have a great potential for implementing massively concurrent systems in an efficient way that would allow us to solve currently intractable problems. In this paper, we look at various models of P systems and investigate their model-checking problems. We identify what is decidable (or undecidable) about model-checking these systems under extended logic formalisms of CTL. We also report on some experiments on whether existing conservative (symbolic) model-checking techniques can be practically applied to handle P systems with a reasonable size.

A k-system consists of k quadratic Diophantine equations over nonnegative integer variables s1, ..., sm, t1, ..., tn of the form: Σ 1≤j≤l B1j(t1, ..., tn)A1j(s1, ..., sm) = C1(s1, ..., sm) Σ 1≤j≤l Bkj(t1, ..., tn)Akj(s1, ..., sm) = Ck(s1, ..., sm) where l, n, m are positive integers, the B's are nonnegative linear polynomials over t1, ..., tn (i.e., they are of the form b0+b1t1+...+bntn, where each bi is a nonnegative integer), and the A's and C's are nonnegative linear polynomials over s1, ..., sm. We show that it is decidable to determine, given any 2-system, whether it has a solution in s1, ..., sm, t1, ..., tn, and give applications of this result to some interesting problems in verification of infinite-state systems. The general problem is undecidable; in fact, there is a fixed k > 2 for which the k-system problem is undecidable. However, certain special cases are decidable and these, too, have applications to verification.

We show that the emptiness problem for two-way nondeterministic finite automata augmented with one reversal-bounded counter (i.e., the counter alternates between nondecreasing and nonincreasing modes a fixed number of times) operating on bounded languages (i.e., subsets of w1* ... wk* for some nonnull words w1, ..., wk) is decidable, settling an open problem in [11,12]. The proof is a rather involved reduction to the solution of a special class of Diophantine systems of degree 2 via a class of programs called two-phase programs. The result has applications to verification of infinite state systems.

We consider generalized discrete timed automata with general linear relations over clocks and parameterized constants as clock constraints and with parameterized durations. We look at three approximation techniques (i.e., the r-reset-bounded approximation, the B-bounded approximation, and the 〈B, r〉-crossing-bounded approximation), and derive automata-theoretic characterizations of the binary reachability under these approximations. The characterizations allow us to show that the safety analysis problem is decidable for generalized discrete timed automata with unit durations and for deterministic generalized discrete timed automata with parameterized durations. An example specification written in ASTRAL is used to run a number of experiments using one of the approximation techniques.