Search

The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings. In the Reactive Turing Machine, transitions have labels to give a notion of interactivity. In the resulting process graph, we use bisimilarity instead of language equivalence. Subsequently, we considered other classical theorems and notions from automata theory and formal languages theory. In this paper, we consider the classical theorem of the correspondence between pushdown automata and context-free grammars. By changing the process operator of sequential composition to a sequencing operator with intermediate acceptance, we get a better correspondence in our setting. We find that the missing ingredient to recover the full correspondence is the addition of a notion of state awareness., LIPIcs, Vol. 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021), pages 8:1-8:16

This paper studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes., Comment: 51 pages

A decidability proof for bisimulation equivalence of first-order grammars is given. It is an alternative proof for a result by S\'enizergues (1998, 2005) that subsumes his affirmative solution of the famous decidability question for deterministic pushdown automata. The presented proof is conceptually simpler, and a particular novelty is that it is not given as two semidecision procedures but it provides an explicit algorithm that might be amenable to a complexity analysis., Comment: version accepted to JCSS

Researches about semantic computing are usually evaluated by experiments, lacking support from the theory of computation. But traditional finite automata are defined on a fixed finite set of states. They will be invalid when a different application needs to change the states. However, semantic computing always asks for more robust automata that can modify itself according to the changes of states. Therefore, in this paper, we redefine traditional automata in more robust forms by semantic computing. The intuitive idea is when the state which an automaton is supposed to enter has changed, we drive automata into a state that is similar to the original one. We can find another similar state in the original state set to replace the changed state by semantic similarity. Based on the theories of semantic similarity, there always exists a similar state. Therefore, once a state has changed, we can always find a similar state to replace it, which means that we can empower automata to adapt to the changes of states. Our new automata bridge the gap between semantic computing and the theory of computation. Furthermore, we also redefine fuzzy finite automata and pushdown automata in more robust forms. Finally, we provide an application about the weather forecast, which indicates how to overcome the limitations of traditional automata.

It is well known that reversible finite automata do not accept all regular languages, that reversible pushdown automata do not accept all deterministic context-free languages, and that reversible queue automata are less powerful than deterministic real-time queue automata. It is of significant interest from both a practical and theoretical point of view to close these gaps. We here extend these reversible models by a preprocessing unit which is basically a reversible injective and length-preserving finite state transducer. It turns out that preprocessing the input using such weak devices increases the computational power of reversible deterministic finite automata to the acceptance of all regular languages, whereas for reversible pushdown automata the accepted family of languages lies strictly in between the reversible deterministic context-free languages and the real-time deterministic context-free languages. For reversible queue automata the preprocessing of the input leads to machines that are stronger than real-time reversible queue automata, but less powerful than real-time deterministic (irreversible) queue automata. Moreover, it is shown that the computational power of all three types of machines is not changed by allowing the preprocessing finite state transducer to work irreversibly. Finally, we examine the closure properties of the family of languages accepted by such machines.

To learn complex formal grammars, recurrent neural networks (RNNs) require sufficient computational resources to ensure correct grammar recognition. One approach to expand model capacity is to couple an RNN to an external stack memory. Here, we introduce a “neural state” pushdown automaton (NSPDA), which consists of a discrete stack instead of an continuous one and is coupled to a neural network state machine. We empirically show its effectiveness in recognizing various context-free grammars (CFGs). First, we develop the underlying mechanics of the proposed higher order recurrent network and its manipulation of a stack as well as how to stably program its underlying pushdown automaton (PDA). We also introduce a noise regularization scheme for higher-order (tensor) networks and design an algorithm for improved incremental learning. Finally, we design a method for inserting grammar rules into a NSPDA and empirically show that this prior knowledge improves its training convergence time by an order of magnitude and, in some cases, leads to better generalization. The NSPDA is also compared to a classical analog stack neural network pushdown automaton (NNPDA) as well as a wide array of first and second-order RNNs with and without external memory, trained using different learning algorithms. Our results show that for the Dyck languages, prior rule-based knowledge is critical for optimization convergence and for ensuring generalization to longer sequences at test time. We observe that many RNNs with and without memory, but no prior knowledge, struggle to converge and generalize on complex and longer CFGs.

Watson-Crick automata work on two-stranded tape, and, consequently, they have two reading heads. In the case of sensing 5 ′ → 3 ′ Watson-Crick automata, the two heads start from different ends of the input and they move in opposite directions until they meet. In this paper, an extension of these automata is presented by adding a pushdown stack. This model can also be seen as a 2-head extension of the pushdown automata. Acceptance by empty stack and acceptance by final states are proven to have the same recognition power in this new model. The language family recognized by this model contains only semi-linear context-sensitive languages and it includes the class of context-free languages. Some well-known non-context-free languages are shown as examples. Normal form like results, a pumping lemma and various closure properties are also proven.

Living systems process information using chemistry. Computations can be viewed as language recognition problems where both languages and automata recognizing them form an inclusive hierarchy. Chemical realizations, without using biochemistry, of the main classes of computing automata, Finite Automata (FA), 1-stack Push Down Automata (1-PDA) and Turing Machine (TM) have recently been presented. These use chemistry for the representation of input information, its processing and output information. The Turing machine uses the Belousov-Zhabotinsky (BZ) oscillatory reaction to recognize a representative Context-Sensitive Language (CSL), the 1-PDA uses a pH network to recognize a Context Free Language (CFL) and a FA for a Regular Language (RL) uses a precipitation reaction. By chemically reconfiguring them to recognize representative languages in the lower classes of the Chomsky hierarchy we illustrate the inclusiveness of the hierarchy of native chemical automata. These examples open the door for chemical programming without biochemistry. Furthermore, the thermodynamic metric originally introduced to identify the accept/reject state of the chemical output for the CSL, can equally be used for recognizing CFL and RL by the automata. Finally, we point out how the chemical and thermodynamic duality of accept/reject criteria can be used in the optimization of the energetics and efficiency of computations.

The paper focuses on automata and linear temporal logics for real-time pushdown reactive systems bridging tractable formalisms specialized for expressing separately dense-time real-time properties and context-free properties though preserving tractability. As for automata, we introduce Event-Clock Nested Automata ( ECNA ), a formalism that combines Event Clock Automata ( ECA ) and Visibly Pushdown Automata ( VPA ). ECNA enjoy the same closure and decidability properties of ECA and VPA expressively extending any previous attempt of combining ECA and VPA . As for temporal logics, we introduce two formalisms for specifying quantitative timing context-free requirements: Event-Clock Nested Temporal Logic ( EC_NTL ) and Nested Metric Temporal Logic ( NMTL ). EC_NTL is an extension of both the logic CaRet and Event-Clock Temporal Logic having Exptime -complete satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Systems ( VPTS ) against EC_NTL . NMTL is a context-free extension of standard Metric Temporal Logic ( MTL ) which is in general undecidable having, though, a fragment expressively equivalent to EC_NTL with Exptime -complete satisfiability and visibly model-checking of VPTS problems.

In the last years renewed investigation of operator precedence languages (OPL) led to discover important properties thereof: OPL are closed with respect to all major operations, are characterized, besides the original grammar family, in terms of an automata family and an MSO logic; furthermore they significantly generalize the well-known visibly pushdown languages (VPL). In another area of research, quantitative models of systems are also greatly in demand. In this paper, we lay the foundation to marry these two research fields. We introduce weighted operator precedence automata and show how they are both strict extensions of OPA and weighted visibly pushdown automata. We prove a Nivat-like result which shows that quantitative OPL can be described by unweighted OPA and very particular weighted OPA. In a B\"uchi-like theorem, we show that weighted OPA are expressively equivalent to a weighted MSO-logic for OPL., Comment: full version, 31 pages

Pushdown automata may contain transitions that are never used in any accepting run of the automaton. We present an algorithm for detecting such useless transitions. A finite automaton that captures the possible stack content during runs of the pushdown automaton, is first constructed in a forward procedure to determine which transitions are reachable, and then employed in a backward procedure to determine which of these transitions can lead to a final state. An implementation of the algorithm is shown to exhibit a favorable performance.

We introduce the concept of one-time nondeterminism as a new kind of limited nondeterminism for finite state machines and pushdown automata. Roughly speaking, one-time nondeterminism means that at the outset the computation is nondeterministic, but whenever it performs a guess, this guess is fixed for the rest of the computation. We characterize the computational power of one-time nondeterministic finite automata (OTNFAs) and one-time nondeterministic pushdown devices. Moreover, we study the descriptional complexity of these machines. For instance, we show that for an [Formula: see text]-state OTNFA with a sole nondeterministic state, that is nondeterministic for only one input symbol, [Formula: see text] states are sufficient and necessary in the worst case for an equivalent deterministic finite automaton. In case of pushdown automata, the conversion of a nondeterministic to a one-time nondeterministic as well as the conversion of a one-time nondeterministic to a deterministic one turn out to be non-recursive, that is, the trade-offs in size cannot be bounded by any recursive function.

Edit distance l-neighbourhood of a formal language is the set of all strings that can be transformed to one of the strings in this language by at most l insertions and deletions. Both the regular and the context-free languages are known to be closed under this operation, whereas the family recognized by deterministic pushdown automata is not. This paper establishes the closure of the family recognized by input-driven pushdown automata (IDPDA), also known as visibly pushdown automata, under the edit distance neighbourhood operation. For an n-state nondeterministic IDPDA with n stack symbols, an automaton for its edit distance l-neighbourhood using O ( n l + 1 ) states is constructed, and an asymptotically matching lower bound is established. For an n-state deterministic IDPDA, its 1-neighbourhood in the worst case requires a deterministic IDPDA with at least 2 Ω ( n 2 ) states.

We define a new normal form for weighted pushdown automata. The new type of automaton uses a stack but has only limited access to it. Only three stack commands are available: popping a symbol, pushing a symbol or leaving the stack unaltered. Additionally, ϵ-transitions are not used. We prove that this automaton model can recognize all weighted context-free languages (i.e., generates all algebraic power series).

In this paper, we study the model checking problem of pushdown systems for projection temporal logic (PTL), an interval-based temporal logic that is as expressive as the full regular languages. For this, we provide an algorithm to decide whether a pushdown system, determined by a pushdown automaton, satisfies a desired logic property, by using relevant automata notations and operations. The algorithm terminates in exponential time for normal PTL properties, i.e. properties specified as normal PTL formulas. To show the lower bound of complexity of the model checking problem, we also construct a polynomial-time reduction from the acceptance problem of a linearly bounded alternating Turing machine. As a result, the model checking problem of pushdown systems for normal PTL properties is EXPTIME-complete.

Timed-register pushdown automata constitute a very expressive class of automata, whose transitions may involve state, input, and top-of-stack timed registers with unbounded differences. They strictly subsume pushdown timed automata of Bouajjani et al., dense-timed pushdown automata of Abdulla et al., and orbit-finite timed-register pushdown automata of Clemente and Lasota. We give an effective logical characterisation of the reachability relation of timed-register pushdown automata. As a corollary, we obtain a doubly exponential time procedure for the non-emptiness problem. We show that the complexity reduces to singly exponential under the assumption of monotonic time. The proofs involve a novel model of one-dimensional integer branching vector addition systems with states. As a result interesting on its own, we show that reachability sets of the latter model are semilinear and computable in exponential time.

The computational study on finite/infinite-state systems, probabilistic systems, and finite-state fuzzy systems, has received much attention recently. In contrast, there are very few results for algorithmic analysis of infinite-state fuzzy systems. In this paper, we introduce fuzzy pushdown termination games (FPDTGs), which are an extension of fuzzy pushdown automata with a game feature and can serve as a formal model of infinite-state fuzzy systems. We investigate some computational issues of the games under termination objectives for two players: the goal of player-1 is to maximize the truth value of eventually terminating at some given configurations with the empty stack, while player-2 aims at the opposite. Some interesting results are obtained. For example, we show that both players have optimal memoryless strategies and the same value. The problem of computing the value can be solved in exponential time when the triangular norm is chosen as the minimum one. Furthermore, we present efficient algorithms for computing the values of two special subclasses of FPDTGs. The potential for practical use of our model is demonstrated by a case study on a manufacturing system.

We introduce the notion of a deterministic biautomaton, a device that reads inputs from both ends, and admits at most one computation on every input word. We show that deterministic biautomata recognize a class of languages which is properly included in the class of linear languages, and which is incomparable to the class of languages recognized by deterministic one-turn pushdown automata. We propose three restrictions of the basic model of deterministic biautomata to characterize the classes of languages generated by DL, linear LL(1), and NH-DL grammars. This results in a chain of four subclasses of linear languages in which all inclusions are strict. For these subclasses and basic operations, we show whether or not a particular class is closed under a considered operation. We prove that it is undecidable whether a linear language belongs to any of these four classes and answer some other decidability questions.

Timed pushdown automata (TPDA) are an expressive formalism combining recursion with a rich logic of timing constraints. We prove that reachability relations of TPDA are expressible in linear arithmetic, a rich logic generalising Presburger arithmetic and rational arithmetic. The main technical ingredients are a novel quantifier elimination result for clock constraints (used to simplify the syntax of TPDA transitions), the use of clock difference relations to express reachability relations of the fractional clock values, and an application of Parikh's theorem to reconstruct the integral clock values., Author's version of JCSS article

We present an automated what-if analysis tool AalWiNes for MPLS networks which allows us to verify both logical properties (e.g., related to the policy compliance) as well as quantitative properties (e.g., concerning the latency) under multiple link failures. Our tool relies on weighted pushdown automata, a quantitative extension of classic automata theory, and takes into account the actual dataplane configuration, rendering it especially useful for debugging. In particular, our tool collects the different router forwarding tables and then builds a pushdown system, on which quantitative reachability is performed based on an expressive query language. Our experiments show that our tool outperforms state-of-the-art approaches (which until now have been restricted to logical properties) by several orders of magnitude; furthermore, our quantitative extension only entails a moderate overhead in terms of runtime. The tool comes with a platform-independent user interface and is publicly available as open-source, together with all other experimental artefacts.

This paper studies the logical properties of a very general class of infinite ranked trees, namely those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal mu-calculus, three main problems: model-checking, logical reflection (aka global model-checking, that asks for a finite description of the set of elements for which a formula holds) and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems we provide an effective solution. This is obtained thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata., 35 pages

The store language of a machine of some arbitrary type is the set of all store configurations (state plus store contents but not the input) that can appear in an accepting computation. New algorithms and characterizations of store languages are obtained, such as the result that any nondeterministic pushdown automaton augmented with reversal-bounded counters, where the pushdown can "flip" its contents up to a bounded number of times, can be accepted by a machine with only reversal-bounded counters. Then, connections are made between store languages and several model checking and reachability problems, such as accepting the set of all predecessor and successor configurations from a given set of configurations, and determining whether there are at least one, or infinitely many, common configurations between accepting computations of two machines. These are explored for a variety of different machine models often containing multiple parallel data stores. Many of the machine models studied can accept the set of predecessor configurations (of a regular set of configurations), the set of successor configurations, and the set of common configurations between two machines, with a machine model that is simpler than itself, with a decidable emptiness, infiniteness, and disjointness property. Store languages are key to showing these properties.

A fairly general definition of canonical solutions to algebraic systems over semirings is proposed. This is based on the notion of summation semirings, traditionally known as ${\Sigma }$ -semirings, and on assigning unambiguous context-free languages to variables of each system. The presented definition applies to all algebraic systems over continuous or complete semirings and to all proper algebraic systems over power series semirings, for which it coincides with the usual definitions of their canonical solutions. As such, it unifies the approaches to algebraic systems over semirings studied in literature. An equally general approach is adopted to study pushdown automata, for which equivalence with algebraic systems is proved. Finally, the Chomsky-Schutzenberger theorem is generalised to the setting of summation semirings.

Visibly pushdown transducers ( VPT ) extend visibly pushdown automata (VPA) with outputs. They read nested words, i.e. finite words on a structured alphabet partitioned into call, return and internal symbols, and produce output words, which are not necessarily nested. As for VPA , the behavior of the stack is synchronized with the types of input symbols: on reading a call symbol, exactly one stack symbol is pushed onto the stack; on reading a return symbol, exactly one stack symbol is popped from the stack; and the stack is untouched when reading internal symbols. Along their transitions VPT can append words on their output tape, whose concatenation define the resulting output word. Therefore VPT define transformations from nested words to words and can be seen as a subclass of pushdown transducers. In this paper, we study the algorithmic, closure and expressiveness properties of VPT .

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).

We give a characterization of NPDAs with reversal-bounded counters (NPCMs) in terms of context-free grammars with monotonic counters. We show that the grammar characterization can be used to give simple proofs of previously known results such as the semilinearity of the Parikh map of any language accepted by an NPCM. We prove a Chomsky–Schutzenberger-like theorem: A language L is accepted by an NPCM if and only if there is a k ≥ 1 and an alphabet Σ containing at least k distinguished symbols, p 1 , . . . , p k , such that L = h ( D ∩ E k ( R ) ) for some homomorphism h, Dyck language D ⊆ Σ ⁎ , and regular set R ⊆ Σ ⁎ , where E k ( R ) = { w | w ∈ R , | w | p 1 = ⋯ = | w | p k } . We also give characterizations of other machine models, such as visibly pushdown automata with reversal-bounded counters (VPCMs). We then investigate the complexity of some decision problems concerning these grammatical models. Finally, we introduce other grammatical models equivalent to NPCM.

It is well known that the "store language" of every pushdown automaton -- the set of store configurations (state and stack contents) that can appear as an intermediate step in accepting computations -- is a regular language. Here many models of language acceptors with various data structures are examined, along with a study of their store languages. For each model, an attempt is made to find the simplest model that accepts their store languages. Some connections between store languages of one-way and two-way machines generally are demonstrated, as with connections between nondeterministic and deterministic machines. A nice application of these store language results is also presented, showing a general technique for proving families accepted by many deterministic models are closed under right quotient with regular languages, resolving some open questions (and significantly simplifying proofs for others that are known) in the literature. Lower bounds on the space complexity for recognizing store languages for the languages to be non-regular are obtained., Comment: 19 pages, preprint to be submitted to a journal

In the existing works of semantic computing (SC), the word “computing” in the phrase “semantic computing” means computational implementations of semantics reasoning (e.g., ontology reasoning, rule reasoning, semantic query, and semantic search) but is irrelevant to the formal theory of computation (e.g., computational models such as finite automaton, pushdown automaton, and Turing machine). In this paper, we propose a different understanding of “semantic computing” from a computation theory perspective. Concretely, we present a formal model of SC in terms of automata and discuss SC for the two most important and simplest types of automata, namely finite automata and pushdown automata. For each automaton, we first consider a simple case (equivalent concepts) and then we further investigate a general situation (semantically related concepts). That is, some new automata for SC are provided: finite (or pushdown) automaton for SC under equivalent concepts, finite (or pushdown) automaton for SC w.r.t. external words, nondeterministic finite automaton for SC under equivalent concepts (or w.r.t. external words), fuzzy finite (or pushdown) automaton for SC under semantically related concepts, and fuzzy finite (or pushdown) automaton for SC w.r.t. external words. Furthermore, we give some properties of these new automata for SC and prove that these new automata are extensions (or enlargements) of traditional (fuzzy) automata.

Learning TOC – begins is a web application which is useful for Learning TOC (Theory of Computation). It covers hypothesis of the basic points with cases and it likewise has Exercise segment in which client can check different speculations for all intents and purposes. It likewise creates drawing of different cases. So the client can learn it adequately and additionally quick. Client can build FA of the string without anyone else and print or fare it for his task work. It has the office of Test to check his score and readiness work. So it is extremely valuable for client as exam arrangement. This Web Application is valuable for the educators and understudies and additionally different clients which are has a place with the Computer Science field. The fundamental reason for this web application is to pick up everything outwardly and graphically. It covers the listed topics given below- Regular Expression, Finite Automata, Context Free Grammar, Push Down Automata, Turing Machine, Exercise of the topics, Mock test.

Several kinds of quantum pushdown automata models have been proposed, and their computational power has been investigated intensively. However, for some quantum pushdown automaton models, it is unknown whether quantum models are at least as powerful as their classical counterparts or not. This is due to the reversibility restriction. In this paper, we introduce a new quantum pushdown automaton model that has a garbage tape. This model can overcome the reversibility restriction by exploiting the garbage tape to store popped symbols. We show that the proposed model can simulate any quantum pushdown automaton with classical stack as well as any probabilistic pushdown automaton. We also show that our model can solve a certain promise problem exactly while deterministic pushdown automata cannot. These results imply that our model is strictly more powerful than its classical counterparts in the setting of exact, one-sided error and non-deterministic computation. Showing impossibility for a promise problem is a difficult task in general. However, by analyzing the behavior of a deterministic pushdown automaton carefully, we obtained the impossibility result. This is one of the main contributions of the paper.

An experiment is described that confirms the security of a well-studied class of cryptographic protocols (Dolev-Yao intruder model) can be verified by two-way nondeterministic pushdown automata (2NPDA). A nondeterministic pushdown program checks whether the intersection of a regular language (the protocol to verify) and a given Dyck language containing all canceling words is empty. If it is not, an intruder can reveal secret messages sent between trusted users. The verification is guaranteed to terminate in cubic time at most on a 2NPDA-simulator. The interpretive approach used in this experiment simplifies the verification, by separating the nondeterministic pushdown logic and program control, and makes it more predictable. We describe the interpretive approach and the known transformational solutions, and show they share interesting features. Also noteworthy is how abstract results from automata theory can solve practical problems by programming language means., In Proceedings MARS/VPT 2018, arXiv:1803.08668

We propose a generic method for deciding semantic equivalences between pushdown automata and finite-state automata. The abstract part of the method is applicable to every process equivalence which is a right PDA congruence. Practical usability of the method is demonstrated on selected equivalences which are conceptual representatives of the whole spectrum. In particular, special attention is devoted to bisimulation-like equivalences (including weak, early, delay, branching, and probabilistic bisimilarity), and it is also shown how the method applies to simulation-like and trace-like equivalences. The generality does not lead to the loss of efficiency; the algorithms obtained by applying our method are essentially time-optimal and sometimes even polynomial. The list of particular results obtained by our method includes items which are first of their kind.

A multi-head 1-way pushdown automaton with $k$ heads is a pushdown automaton with $k$ 1-way read heads on the input tape and a stack. It was previously shown that the deterministic variant of the model cannot accept all the context free languages. In this paper, we introduce a 2-tape, 2-head model namely Watson-Crick pushdown automata where the content of the second tape is determined using a complementarity relation, similar to Watson-Crick automata. We show computational powers of nondeterministic two-head pushdown automata and nondeterministic Watson-Crick pushdown automata are same. Moreover, deterministic Watson-Crick pushdown automata can accept all the context free languages.

We study the size-cost of Boolean operations on constant height nondeterministic pushdown automata, i.e. on pushdown automata with a constant limit on the size of the pushdown. For intersection, we show an exponential simulation and prove that the exponential blow-up is necessary. For union, instead, we provide a linear trade-off while, for complement, we show a double-exponential simulation and prove a single-exponential lower bound.

In this paper, we propose a reduction of the minimization problem for a bottom-up deterministic tree automaton (DFTA), making the latter a minimization of a string deterministic finite automaton (DFA). To achieve this purpose, we proceed first by the transformation of the tree automaton into a particular string automaton, followed by minimizing this string automaton. In addition, we show that for our transformation, the minimization of the resulting string automaton coincides with the minimization of the original tree automaton. Finally, we discuss the complexity of our proposal for different types of tree automata, namely: standard, acyclic, incremental, and incrementally constructed tree automata.

Two-player games on graphs are central in many problems in formal verification and program analysis, such as synthesis and verification of open systems. In this work, we consider solving recursive game graphs (or pushdown game graphs) that model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives—such as reachability and ω-regular objectives—in this work, we study for the first time such games with the most well-studied quantitative objective, the mean-payoff objective. In pushdown games, two types of strategies are relevant: (1) global strategies, which depend on the entire global history; and (2) modular strategies, which have only local memory and thus do not depend on the context of invocation but rather only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity by showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games and memoryless modular strategies are sufficient in two-player pushdown games. Finally, we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.

This paper introduces the concepts of fuzzy tree pushdown automata and fuzzy context-free tree grammars. At first, we show that any fuzzy context-free tree grammar can be converted into a corresponding definition of fuzzy Chomsky normal form for trees. Then, the relation between a fuzzy context-free tree grammar and a fuzzy tree pushdown automaton is investigated. In fact, we show that the class of languages accepted by fuzzy tree pushdown automata is identical to the one generated by fuzzy context-free tree grammars. Some examples are given to clarify the results.

We introduce and study input-driven deterministic and nondeterministic double-head pushdown automata. A double-head pushdown automaton is a slight generalization of an ordinary pushdown automaton working with two input heads that move in opposite directions on the common input tape. In every step one head is moved and the automaton decides on acceptance if the heads meet. Demanding the automaton to work input-driven it is required that every input symbol uniquely defines the action on the pushdown store (push, pop, state change). Normally this is modeled by a partition of the input alphabet and is called a signature. Since our automaton model works with two heads either both heads respect the same signature or each head owes its own signature. This results in two variants of input-driven double-head pushdown automata. The induced language families on input-driven double-head pushdown automata are studied from the perspectives of their language describing capability, their closure properties, and decision problems., Comment: In Proceedings AFL 2017, arXiv:1708.06226

The following problem is shown undecidable: given regular languages L,K of finite trees, decide if there exists a deterministic tree-walking automaton which accepts all trees in L and rejects all trees in K. The proof uses a technique of Kopczy\'nski from LICS 2016.

A word is called a reset word for a deterministic finite automaton if it maps all the states of the automaton to a unique state. Deciding about the existence of a reset word of a given maximum length for a given automaton is known to be an NP-complete problem. We prove that it remains NP-complete even if restricted to Eulerian automata with binary alphabets, as it has been conjectured by Martyugin (2011)., Extended version of a paper presented at LATA 2014

We shall consider nondeterministic and deterministic automata equipped with a limited pushdown (constant height npda s and dpda s) as well as their two-way versions (constant height 2 npda s and 2 dpda s). We show two double-exponential gaps for these devices, namely, (i) for complementing constant height one-way npda s and (ii) for converting constant height 2 npda s or 2 dpda s into one-way devices.

We propose in this paper a model checking framework for service trust behaviors. We devise a new trust behavior model, which is a deterministic PushDown Automaton (PDA) based trust behavior model. This model is built based on the observations' sequences, which are derived from the interactions with services. Furthermore, we express the regular and non-regular trust behavior properties using Fixed point Logic with Chop (FLC). The model checking of service trust behaviors with respect to trust properties is performed using a symbolic FLC model checking algorithm. Finally, we present some experiments to assess the efficiency of the proposed algorithm.

Games on recursive game graphs can be used to reason about the control flow of sequential programs with recursion. In games over recursive game graphs, the most natural notion of strategy is the modular strategy, i.e., a strategy that is local to a module and is oblivious to previous module invocations, and thus does not depend on the context of invocation. In this work, we study for the first time modular strategies with respect to winning conditions that can be expressed by a pushdown automaton. We show that such games are undecidable in general, and become decidable for visibly pushdown automata specifications. Our solution relies on a reduction to modular games with finite-state automata winning conditions, which are known in the literature. We carefully characterize the computational complexity of the considered decision problem. In particular, we show that modular games with a universal Buchi or co Buchi visibly pushdown winning condition are EXPTIME-complete, and when the winning condition is given by a CARET or NWTL temporal logic formula the problem is 2EXPTIME-complete, and it remains 2EXPTIME-hard even for simple fragments of these logics. As a further contribution, we present a different solution for modular games with finite-state automata winning condition that runs faster than known solutions for large specifications and many exits., In Proceedings GandALF 2014, arXiv:1408.5560

We present a differentiable stack data structure that simultaneously and tractably encodes an exponential number of stack configurations, based on Lang's algorithm for simulating nondeterministic pushdown automata. We call the combination of this data structure with a recurrent neural network (RNN) controller a Nondeterministic Stack RNN. We compare our model against existing stack RNNs on various formal languages, demonstrating that our model converges more reliably to algorithmic behavior on deterministic tasks, and achieves lower cross-entropy on inherently nondeterministic tasks., 13 pages, 5 figures. Published at CoNLL 2020. This revision fixes a typo

Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class which still captures useful behaviors. In this paper, we propose a new class of bounded underapproximations for multi-pushdown systems, which subsumes most existing classes. We develop an efficient algorithm for solving the under-approximate reachability problem, which is based on efficient fix-point computations. We implement it in our tool BHIM and illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway BHIM solves the binary reachability problem in pushdown automata. To show the versatility of our approach, we then extend our algorithm to the timed setting and provide the first implementation that can handle timed multi-pushdown automata with closed guards.

International audience; Limited automata are single-tape Turing machines with severe rewriting restrictions. They have been introduced in 1967 by Thomas Hibbard, who proved that they have the same computational power as pushdown automata. Hence, they provide an alternative characterization of the class of context-free languages in terms of recognizing devices. After that paper, these models have been almost forgotten for many years. Only recently limited automata were reconsidered in a series of papers, where several properties of them and of their variants have been investigated. In this work we present an overview of the most important results obtained in these researches. We also discuss some related models and possible lines for future investigations.

We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {unit}\rightarrow \mathsf {unit}\rightarrow \mathsf {unit}$$\end{document}unit→unit→unit. At the technical level, our results marry game semantics with automata-theoretic techniques developed to handle infinite alphabets. On the automata-theoretic front, we show decidability of the emptiness problem for register pushdown automata extended with fresh-symbol generation.

International audience; The paper investigates the closure of the language family defined by input-driven pushdown automata (IDPDA) under the following operations: insertion $$ins(L, K)=\{xyz \mid xz \in L, \, y \in K\}$$, deletion $$del(L, K)=\{xz \mid xyz \in L, \, y \in K\}$$, square root $$\sqrt{L}=\{w \mid ww \in L\}$$, and the first half $$\frac{1}{2}L=\{u \mid \exists v: |u|=|v|, \, uv \in L\}$$. For K and L recognized by nondeterministic IDPDA, with m and with n states, respectively, insertion requires $$mn+2m$$ states, as long as K is well-nested; deletion is representable with 2n states, for well-nested K; square root requires $$n^3-O(n^2)$$ states, for well-nested L; the well-nested subset of the first half is representable with $$2^{O(n^2)}$$ states. Without the well-nestedness constraints, non-closure is established in each case.