Search

The degree of ambiguity (respectively, the path size) of a nondeterministic automaton, on a given input, measures the number of accepting computations (respectively, the number of all computations). It is known that deciding the finiteness of the degree of ambiguity of a nondeterministic pushdown automaton is undecidable. Also, it is undecidable for a given k ≥ 3 to decide whether the path size of a nondeterministic pushdown automaton is bounded by k. As the main result, we show that deciding the finiteness of the path size of a nondeterministic pushdown automaton can be done in polynomial time. Also, we show that the k -path problem for nondeterministic input-driven pushdown automata (respectively, for nondeterministic finite automata) is complete for exponential time (respectively, complete for polynomial space). • We show that finiteness of path size of nondeterministic pushdown automata can be solved in polynomial time. • We show that deciding k-path property is PSPACE complete for nondeterministic finite automata. • We show that deciding k-path property is exponential time complete for nondeterministic input-driven pushdown automata. [ABSTRACT FROM AUTHOR]

We study languages closed under the non-contiguous (scattered) subword containment order. Any subword-closed language L can be uniquely described by its anti-dictionary, i.e. the set of minimal words that do not belong to L. For a language over a finite alphabet, the anti-dictionary is necessarily finite. A language L is said to be atomic if it cannot be presented as the union of two subword-closed languages different from L. In this work, we provide a decision procedure which, given a language over a finite alphabet defined by its anti-dictionary, decides whether it is atomic or not. We also develop an algorithmic procedure for decomposing a language, which is not atomic, into finitely many atomic sublanguages. [ABSTRACT FROM AUTHOR]

We consider weighted tree automata over strong bimonoids (for short: wta). A wta A has the finite-image property if its recognized weighted tree language 〚 A 〛 has finite image; moreover, A has the preimage property if the preimage under 〚 A 〛 of each element of the underlying strong bimonoid is a recognizable tree language. For each wta A over a past-finite monotonic strong bimonoid we prove the following results. In terms of A 's structural properties, we characterize whether it has the finite-image property. We characterize those past-finite monotonic strong bimonoids such that for each wta A it is decidable whether A has the finite-image property. In particular, the finite-image property is decidable for wta over past-finite monotonic semirings. Moreover, we prove that A has the preimage property. All our results also hold for weighted string automata. [ABSTRACT FROM AUTHOR]

We solve in polynomial time two decision problems that occur in type checking when typings depend on universe level constraints. [ABSTRACT FROM AUTHOR]

In this paper we consider a number of natural decision problems involving k -regular sequences. Specifically, they arise from considering • lower and upper bounds on growth rate; in particular boundedness, • images, • regularity (recognizability by a deterministic finite automaton) of preimages, and • factors, such as squares and palindromes, of such sequences. We show that these decision problems are undecidable. [ABSTRACT FROM AUTHOR]

The model of deterministic input-driven multi-counter automata is introduced and studied. On such devices, the input letters uniquely determine the operations on the underlying data structure that is consisting of multiple counters. We study the computational power of the resulting language families and compare them with known language families inside the Chomsky hierarchy. In addition, it is possible to prove a proper counter hierarchy depending on the alphabet size. This means that any input alphabet induces an upper bound which depends on the alphabet size only, such that k + 1 counters are more powerful than k counters as long as k is less than this bound. The hierarchy interestingly collapses at the level of the bound. Furthermore, we investigate the closure properties of the language families. For input-driven multi-counter automata with 0 or 1 counter, we discuss the computational complexity of their decidable problems. For k ≥ 2 counters, the decidability problems of emptiness, finiteness, universality, inclusion, equivalence, regularity, and context-freeness are shown to be non-semidecidable. Finally, we study descriptional complexity aspects of input-driven multi-counter automata. It is shown that a nondeterministic device can be determinized and that 2 n − 1 is a necessary and sufficient blow-up in the number of states for the determinization. For the operational state complexity of deterministic input-driven multi-counter automata under Boolean operations, tight bounds on the number of states are established. Finally, it turns out that the size trade-offs between deterministic input-driven multi-counter automata with k + 1 and k counters are non-recursive, that is, they are not bounded by any recursive function. [ABSTRACT FROM AUTHOR]

SRL is a total programming language with distinctive features: (i) every program that mentions n registers defines a bijection Z n → Z n , and (ii) the generation of the SRL -program that computes the inverse of that bijection can be automatic. Containing SRL a very essential set of commands, it is suitable for studying strengths and weaknesses of reversible computations. We deal with the fixed points of SRL -programs. Given any SRL -program P , we are interested in the problem of deciding if a tuple of initial register values of P exists which remains unaltered after its execution. We show that the existence of fixed points in SRL is undecidable and complete in Σ 1 0. We show that such problem remains undecidable even when the number of registers mentioned by P is limited to 12. Moreover, if we restrict to the linear programs of SRL , i.e. to those programs where different registers control nested loops, then the problem is already undecidable for the class of SRL -programs that mention no more than 3712 registers. Last, we show that, except for trivial cases, finding if the number of fixed points has a given cardinality is also undecidable. [ABSTRACT FROM AUTHOR]

We consider the one-variable fragment of first-order logic extended with Presburger constraints. The logic is designed in such a way that it subsumes the previously-known fragments extended with counting, modulo counting or cardinality comparison and combines their expressive powers. We prove Image 1 -completeness of the logic by presenting an optimal algorithm for solving its finite satisfiability problem. [ABSTRACT FROM AUTHOR]

Site-directed insertion is an overlapping insertion operation that can be viewed as analogous to the overlap assembly or chop operations that concatenate strings by overlapping a suffix and a prefix of the argument strings. We consider decision problems and language equations involving site-directed insertion. By relying on the tools provided by semantic shuffle on trajectories (M. Domaratzki, Developments in Language Theory 2004) we show that one variable equations involving site-directed insertion and regular constants can be solved algorithmically. We consider also maximal and minimal variants of the site-directed insertion operation and the nondeterministic state complexity of site-directed insertion. [ABSTRACT FROM AUTHOR]

We study a variant ATL FB of the alternating-time temporal logic ATL with a non-standard, 'finitely bounded' semantics (FBS). FBS was originally defined as a game-theoretic semantics where players must commit to time limits when attempting to verify eventuality (respectively, to falsify safety) formulae. It turns out that FBS has a natural corresponding compositional semantics that essentially evaluates formulae only on finite initial segments of paths and imposes uniform bounds on all plays for the fulfilment of eventualities. The resulting version ATL FB differs in some essential features from the standard ATL, as it no longer has the finite model property, though the two logics are equivalent on finite models. We develop two tableau systems for ATL FB. The first one deals with infinite sets of formulae and may run in a transfinite sequence of steps, whereas the second one deals only with finite sets of formulae in an extended language allowing explicit symbolic indication of time limits in formulae. We prove soundness and completeness of the infinitary tableau system and prove that it is equivalent to the finitary one. We also show that the finitary tableau system provides an exponential-time decision procedure for the satisfiability problem of ATL FB and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATL FB and prove its soundness and completeness. [ABSTRACT FROM AUTHOR]

Abstract In this short paper I will exhibit several mistakes in the recent attempt by Bimbó [3] to prove the decidability of the multiplicative exponential fragment of linear logic (MELL). In fact, the main mistake is so serious that there is no obvious fix, and therefore the decidability of MELL remains an open problem. As a side effect, this paper contains a complete (syntactic) proof of the decidability of the relevant version of MELL (called RMELL in this paper), that is the logic obtained from MELL by replacing the linear logic contraction rule by a general unrestricted version of the contraction rule. This proof can also be found (with a small error) in [3] , and a semantic proof can be found in [35]. [ABSTRACT FROM AUTHOR]

Abstract Let G be a group and let φ : Σ ⁎ → G be a monoid homomorphism from the set of all strings Σ ⁎ over some finite alphabet Σ onto the group G. The set Σ is then called a generating set for G and the language { 1 } φ − 1 ⊆ Σ ⁎ is called the word problem of G with respect to the generating set Σ (via the homomorphism φ) and is denoted by W (G , Σ). We consider nine conditions that hold in each such language of the form W (G , Σ) and determine which combinations of these conditions are equivalent to the property of the language in question being the word problem of a group. We show that each of these nine conditions is decidable for the family of regular languages but that each is undecidable for the family of one-counter languages (the languages accepted by one-counter pushdown automata). We also show that the property of a language being the word problem of a group is undecidable for the family of one-counter languages but is decidable for the family of deterministic context-free languages (the languages accepted by deterministic pushdown automata). [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

We show that it is undecidable whether or not an injective rational function (realized by a finite transducer) f : A ⁎ → A ⁎ has a fixed point. The proof applies undecidability of the Post's Correspondence Problem for injective morphisms. As a corollary we obtain that the existence of a fixed point of injective computable functions is undecidable. [ABSTRACT FROM AUTHOR]

There have been several attempts to extend the notion of conjugacy from groups to monoids. The aim of this paper is study the decidability and independence of conjugacy problems for three of these notions (which we will denote by ∼ p , ∼ o , and ∼ c ) in certain classes of finitely presented monoids. We will show that in the class of polycyclic monoids, p -conjugacy is “almost” transitive, ∼ c is strictly included in ∼ p , and the p - and c -conjugacy problems are decidable with linear complexity on a two-tape Turing Machine. For other classes of monoids, the situation is more complicated. We show that there exists a monoid M defined by a finite complete presentation such that the c -conjugacy problem for M is undecidable, and that for finitely presented monoids, the c -conjugacy problem and the word problem are independent, as are the c -conjugacy and p -conjugacy problems. On other hand, we show that for finitely presented monoids, the o -conjugacy problem is reducible to the c -conjugacy problem. [ABSTRACT FROM AUTHOR]

We consider parsers of deterministic context-free languages and study the sizes of their syntax checking components. More precisely, we allow the input processing from left to right or, alternatively, from right to left, whatever is best for the given language. As practical examples, we establish an infinite sequence of deterministic context-free languages L k , for k ≥ 1 , such that there is an exponential size trade-off between a deterministic pushdown automaton that reads its input from right to left and another one that reads its input from left to right. Concerning the constructibility of such a parser out of a given deterministic context-free language, it is shown that it is undecidable whether the reversal of a given deterministic context-free language is again deterministic context free. Related to decidability questions, it turns out that the size trade-offs between deterministic pushdown automata that represent the reversals of their accepted languages and deterministic pushdown automata that represent their accepted languages are non-recursive. That is, one can choose an arbitrarily large recursive function ϱ , but the gain in economy of description eventually exceeds ϱ when changing from the former system to the latter. Furthermore, we study the expressive capacity of the family of languages whose reversals are deterministic context free. Finally, we turn to the family of deterministic context-free languages whose reversals are also deterministic context free and collect several of their closure properties. [ABSTRACT FROM AUTHOR]

We investigate chop operations, which can be seen as generalized concatenation. For several language families of the Chomsky hierarchy we prove (non)closure properties under chop operations and incomparability to the family of languages that are the chop of two regular languages. We also prove non-closure of that language family under Boolean operations and closure under reversal. Further, the representation of a regular language as the chop of two regular expressions can be exponentially more succinct than its regular expression. By considering the chop of two linear context-free languages we already obtain language families that have non-semi-decidable problems such as emptiness or finiteness. [ABSTRACT FROM AUTHOR]

We consider a new operation on the family of binary relations on integers called Hadamard star. View a binary relation R ⊆ N × N as a mapping of N into the power set of N and let R ( n ) denote the subset of integers m such that ( n , m ) ∈ R . Then the Hadamard star of R is the relation which assigns to each integer n the Kleene star of R ( n ) . This is reminiscent of the Hadamard inverse of series with coefficients in a field. We characterize the rational relations whose Hadamard star is also rational and show that this property is decidable. [ABSTRACT FROM AUTHOR]

As part of a general research programme into the expressive power of different generalisations of the sequent framework we investigate hypersequent calculi given by rules of the newly introduced format of hypersequent rules with context restrictions. The introduced rule format is used to prove uniform syntactic cut elimination, decidability and complexity results. We also introduce transformations between hypersequent rules of this format and Hilbert axioms, entailing a result about the limits of such rules. As case studies, we apply our methods to several modal logics and obtain e.g. a complexity-optimal decision procedure for the logic S5 and new calculi for the logic K 4 . 2 as well as combinations of modal logics in the form of simply dependent bimodal logics. [ABSTRACT FROM AUTHOR]

This paper provides efficient algorithms that decide membership for classes of several Boolean hierarchies for which efficiency (or even decidability) were previously not known. We develop new forbidden-chain characterizations for the single levels of these hierarchies and obtain the following results: • The classes of the Boolean hierarchy over level Σ 1 of the dot-depth hierarchy are decidable in NL (previously only the decidability was known). The same remains true if predicates mod d for fixed d are allowed. • If modular predicates for arbitrary d are allowed, then the classes of the Boolean hierarchy over level Σ 1 are decidable. • For the restricted case of a two-letter alphabet, the classes of the Boolean hierarchy over level Σ 2 of the Straubing–Thérien hierarchy are decidable in NL. This is the first decidability result for this hierarchy. • The membership problems for all mentioned Boolean-hierarchy classes are logspace many-one hard for NL. • The membership problems for quasi-aperiodic languages and for d -quasi-aperiodic languages are logspace many-one complete for PSPACE. [ABSTRACT FROM AUTHOR]

Interval temporal logics provide a general framework for temporal representation and reasoning, where classical (point-based) linear temporal logics can be recovered as special cases. In this paper, we study the effects of the addition of one or more equivalence relations to one of the most representative interval temporal logics, namely, the logic AB B ¯ of Allen's relations meets , begun by , and begins . We first prove that the satisfiability problem for the extension of AB B ¯ with one equivalence relation remains decidable over finite linear orders, but it becomes nonprimitive recursive. Then, we show that decidability is lost over N . Finally, we show that the addition of two or more equivalence relations makes finite satisfiability for the resulting logic undecidable. 1 [ABSTRACT FROM AUTHOR]

Unique decomposition has been a subject of interest in process algebra for a long time (for example in BPP [1] or CCS [2,3] ), as it provides a normal form and useful cancellation properties. We provide two parallel decomposition results for subsets of the applied π -calculus: we show that every closed normed (i.e. with a finite shortest complete trace) process P can be decomposed uniquely into prime factors P i with respect to strong labeled bisimilarity, i.e. such that P ∼ l P 1 | … | P n . Moreover, we prove that closed finite processes can be decomposed uniquely with respect to weak labeled bisimilarity. We also investigate whether efficient algorithms that compute the unique decompositions exist. The simpler problem of deciding whether a process is in its unique decomposition form is undecidable in general in both cases, due to potentially undecidable equational theories. Moreover, we show that the unique decomposition remains undecidable even given an equational theory with a decidable word problem. [ABSTRACT FROM AUTHOR]

We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is defined by an undirected graph and the behaviour of each node is defined by a timed automaton communicating with its neighbours via broadcast messages. We consider parameterized verification problems formulated in terms of reachability. In particular we are interested in searching for an initial configuration from which an individual node can reach an error state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata. [ABSTRACT FROM AUTHOR]

We investigate the descriptional and computational complexity of boundary sets of regular and context-free languages. For a letter a , the right (left, respectively) a -boundary set of a language L consists of the words in L whose a -predecessor or a -successor w.r.t. the prefix (suffix, respectively) relation is not in L . For regular languages described by deterministic finite automata (DFAs) we give tight bounds on the number of states for accepting boundary sets. Moreover, the question whether the boundary sets of a regular language is finite is shown to be NL -complete for DFAs, while it turns out to be PSPACE -complete for nondeterministic devices. Boundary sets for context-free languages are not necessarily context free anymore. Here we find a subtle difference of right and left a -boundary sets. While right a -boundary sets of deterministic context-free languages stay deterministic context free, we give an example of a deterministic context-free language whose a -boundary set is already non-context free. In fact, the finiteness problem for a -boundary sets of context-free languages becomes undecidable. [ABSTRACT FROM AUTHOR]

The intensional fragment of classical propositional linear logic combines modalities with contraction-free relevance logic — adding modalized versions of the thinning and contraction rules. This paper provides a proof of the decidability of this logic based on a sequent calculus formulation. Some related logics and some other fragments of linear logic are also shown decidable. [ABSTRACT FROM AUTHOR]

In this paper, we show the decidability of a new subclass of linear hybrid automata. These automata are planar, that is, consist of two state variables, monotonic along some direction in the plane and have identity resets, that is, the values of the continuous variables are not reset to a different value on a discrete transition. Our proof uses a combination of a tree construction capturing the edge-to-edge reachability and a finite bisimulation construction. Our class strictly contains the class of two dimensional piecewise constant derivative systems for which decidability of the reachability problem is known. [ABSTRACT FROM AUTHOR]

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. Their computational behavior mainly depends on two parameters: the set of modalities they feature and the linear orders over which they are interpreted. In this paper, we identify all fragments of Halpern and Shoham's interval temporal logic HS with a decidable satisfiability problem over the class of strongly discrete linear orders as well as over its relevant subclasses (the class of finite linear orders, Z , N , and Z − ). We classify them in terms of both their relative expressive power and their complexity, which ranges from NP-completeness to non-primitive recursiveness. [ABSTRACT FROM AUTHOR]

The paper deals with recent developments about non-uniform cellular automata. After reviewing known results about structural stability we complete them by showing that also sensitivity to initial conditions is not structurally stable. The second part of the paper reports the complexity results about the main dynamical properties. Some proofs are shortened and clarified. The third part is completely new and starts the exploration of the fixed points set of non-uniform cellular automata. [ABSTRACT FROM AUTHOR]

We study the freeness problem over morphism and matrix semigroups. We show that the freeness problem is undecidable for morphisms over a three-letter alphabet. We show that there is a commutative semiring R such that the freeness problem is undecidable for upper-triangular 2 × 2 matrices having entries in R . [ABSTRACT FROM AUTHOR]

Given a finite set X of strings, X is a hypercode if a string in X is not a subsequence of any other string in X . We consider hypercodes for involution codes, which are useful for DNA strand design, and define an involution hypercode. We then tackle the involution hypercode decidability problem; that is, to determine whether or not a given language is an involution hypercode. Based on the hypercode properties, we design a polynomial runtime algorithm for regular languages. We also prove that it is decidable whether or not a context-free language is an involution hypercode. Note that it is undecidable for some other involution codes such as involution prefix codes, suffix codes, and k -intercodes. [ABSTRACT FROM AUTHOR]

This investigation studies nonemptiness problems of plane edge coloring with three colors. In the edge coloring (or Wang tiles) of a plane, unit squares with colored edges that have one of p colors are arranged side by side such that the touching edges of the adjacent tiles have the same colors. Given a basic set B of Wang tiles, the nonemptiness problem is to determine whether or not Σ(B)≠ ∅, where Σ(B) is the set of all global patterns on Z² that can be constructed from the Wang tiles in B. Wang's conjecture is that for any B of Wang tiles, Σ(B)≠∅ if and only if P(B)≠∅, where P(B) is the set of all periodic patterns on Z² that can be generated by the tiles in B. When p ≥ 5, Wang's conjecture is known to be wrong. When p = 2, the conjecture is true. This study proves that when p = 3, the conjecture is also true. If P(B)≠∅, then B has a subset B' of minimal cycle generators such that P(B') ≠∅ and P(B") = ∅ for B" B'. This study demonstrates that the set C(3) of all minimal cycle generators contains 787,605 members that can be classified into 2,906 equivalence classes. N(3) is the set of all maximal non-cycle generators: if B ∈ N(3), then P (B) = ∅ and =P(B") ≠ ∅ for B" B. Wang's conjecture is shown to be true by proving that B ∈ N(3) implies Σ(B)=∅. [ABSTRACT FROM AUTHOR]

Abstract: In this paper we study the dynamics of D-dimensional cellular automata (CA) by considering them as one-dimensional (1D) CA along some direction (slicing constructions). These constructions allow to give the D-dimensional version of important notions as 1D closing property and lift well-known one-dimensional results to the D-dimensional settings. Indeed, like in one-dimensional case, closing D-dimensional CA have jointly dense periodic orbits and biclosing D-dimensional CA are open. By the slicing constructions, we further prove that for the class of closing D-dimensional CA, surjectivity implies surjectivity on spatially periodic configurations (old standing open problem). We also deal with the decidability problem of the D-dimensional closing. By extending the Kariʼs construction from [31] based on tilings, we prove that the two-dimensional, and then D-dimensional, closing property is undecidable. In such a way, we add one further item to the class of dimension sensitive properties, i.e., properties that are decidable in dimension 1 and are undecidable in higher dimensions. It is well-known that there are not positively expansive CA in dimension 2 and higher. As a meaningful replacement, we introduce the notion of quasi-expansivity for D-dimensional CA which shares many global properties (in the D-dimensional settings) with the 1D positive expansivity. We also prove that for quasi-expansive D-dimensional CA the topological entropy (which is an uncomputable property for general CA) has infinite value. In a similar way as quasi-expansivity, the notions of quasi-sensitivity and quasi-almost equicontinuity are introduced and studied. [Copyright &y& Elsevier]