P-hardness of the emptiness problem for visibly pushdown languages

Visibly pushdown languages form a subclass of the context-free languages which is appealing because of its nice algorithmic and closure properties. Here we show that the emptiness problem for this class is not any easier than the emptiness problem for context-free languages, namely hard for deterministic polynomial time. The proof consists of a reduction from the alternating graph reachability problem.     

Efficient determinization of visibly and height-deterministic pushdown automata

New algorithms for the determinization of nondeterministic visibly and nondeterministic real-time height-deterministic pushdown automata are presented. The algorithms improve the results of existing algorithms. They construct only accessible states and necessary pushdown symbols of the resulting deterministic pushdown automata.     

The word problem for visibly pushdown languages described by grammars

Visibly pushdown languages are an interesting subclass of deterministic context-free languages that can model nonregular properties of interest in program analysis. Such class properly contains typical classes of parenthesized languages such as “parenthesis”, “bracketed”, “balanced” and “input-driven” languages. It is closed under boolean operations and has decidable decision problems such as emptiness, inclusion and universality. We study the membership problem for visibly pushdown languages, and show that it can be solved in time linear in both the size of the input grammar and the length of the input word. The algorithm relies on a reduction to the reachability problem for game graphs. We also discuss the time complexity of the membership problem for the class of balanced languages which is the largest among those cited above. Besides the intrinsic theoretical interest, we further motivate our main result showing an application to the validation of XML documents against Schema and Document Type Definitions (DTDs). Work partially supported by funds for the research from MIUR 2006, grant “Metodi Formali per la verifica di sistemi chiusi ed aperti”, Università di Salerno. A preliminary version of this paper was published in the Proceedings of the 4th International Symposium Automated Technology for Verification and Analysis (ATVA 2006), Lecture Notes in Computer Science 4218, pp. 96–109, 2006.     

Rewriting of visibly pushdown languages for XML data integration

In this work, we focus on XML data integration by studying rewritings of XML target schemas in terms of source schemas. Rewriting is very important in data integration systems where the system is asked to find and assemble XML documents from the data sources and produce documents that satisfy a target schema.As schema representation, we consider Visibly Pushdown Automata (VPAs), which accept Visibly Pushdown Languages (VPLs). The latter have been shown to coincide with the family of (word-encoded) regular tree languages, which are the basis of formalisms for specifying XML schemas. Furthermore, practical semi-formal XML schema specifications (defined by simple pattern conditions on XML) compile into VPAs that are exponentially more concise than other representations based on tree automata.Notably, VPLs enjoy a “well-behavedness” that facilitates us in addressing rewriting problems for XML data integration. Based on VPAs, we positively solve these problems, and present detailed complexity analyses.     

Semitopological semirings and pushdown automata

This paper deals with algebraic power series over a commutative semiringA. A characteristization result states that a power series is algebraic if and only if it is the behavior of a proper pushdown automaton.To achieve this result some topological concepts are needed to be able to solve linear equations over semirings.     

Characterizations and extensions of pushdown translations

A device called a pushdown assembler has been recently introduced and has been shown capable of defining exactly the syntax directed translations (SDT's). The output operation of the pushdown assembler can be extended in a natural way to obtain a more powerful device called a type B pushdown assembler (or B-machine). A B-machine can define SDT's more simply and directly than the original pushdown assembler. B-machines can also define many interesting translations which are not SDT's. In this paper the B-machine is defined and compared with the original pushdown assembler. The properties of B-machine translations are investigated and it is shown that, as with SDT's, there exists a natural infinite hierarchy of B-machine translations.     

Conjunctive grammars and alternating pushdown automata

In this paper we introduce a variant of alternating pushdown automata, synchronized alternating pushdown automata, which accept the same class of languages as those generated by conjunctive grammars.     

On the power of deep pushdown stacks

Inspired by recent work of Meduna on deep pushdown automata, we consider the computational power of a class of basic program schemes, NPSDS _s , based around assignments, while-loops and non-deterministic guessing but with access to a deep pushdown stack which, apart from having the usual push and pop instructions, also has deep-push instructions which allow elements to be pushed to stack locations deep within the stack. We syntactically define sub-classes of NPSDS _s by restricting the occurrences of pops, pushes and deep-pushes and capture the complexity classes NP and PSPACE. Furthermore, we show that all problems accepted by program schemes of NPSDS _s are in EXPTIME.     

格值下推自动机与格值上下文无关文法

引入了格值下推自动机、格值上下文无关文法及它们的语言的概念,证明了格值下推自动机以两种不同方式接受的语言类的等价性,研究了格值Chomsky范式文法、格值上下文无关文法及其派生所产生的语言的等价条件,揭示了在一定条件下,格值下推自动机接受的语言类与格值上下文无关文法产生的语言类的等价性,证明了有理格值语言均被格值下推自动机识别。     

On regular tree languages and deterministic pushdown automata

The theory of formal string languages and of formal tree languages are both important parts of the theory of formal languages. Regular tree languages are recognized by finite tree automata. Trees in their postfix notation can be seen as strings. This paper presents a simple transformation from any given (bottom-up) finite tree automaton recognizing a regular tree language to a deterministic pushdown automaton accepting the same tree language in postfix notation. The resulting deterministic pushdown automaton can be implemented easily by an existing parser generator because it is constructed for an LR(0) grammar, and its size directly corresponds to the size of the deterministic finite tree automaton. The class of regular tree languages in postfix notation is a proper subclass of deterministic context-free string languages. Moreover, the class of tree languages which are in their postfix notation deterministic context-free string languages is a proper superclass of the class of regular tree languages.     

On the complexity of finite,pushdown, and stack automata

The complexity of predicates on several classes of formal languages is studied. For finite automata, pushdown automata, and several classes of stack automata, every nontrivial predicate on the languages accepted by the 1-way devices requires as much time and space as the recognition problem for any language accepted by the corresponding 2-way devices. Moreover there are nontrivial predicates on the languages accepted by the 1-way devices such that is the accepted language of some corresponding one or two head 2-way device. Thus our lower bounds are fairly tight.This research was sponsored in part by an NSF graduate fellowship in computer science at Cornell University, NSF grant GJ-35570 at Princeton University, and by United States Army Contract No. DA-31-124-ARO-D-462 at the University of Wisconsin.     

Synchronizable deterministic pushdown automata and the decidability of their equivalence

Summary The notion of synchronized and synchronizable deterministic pushdown automata (DPDA's) is introduced. It is shown that the equivalence of two synchronized and even of synchronizable DPDA's can be tested. It is conjectured that every two equivalent DPDA's are synchronizable. It is also shown that the equivalence of two deterministic pushdown transducers whose underlying DPDA's are synchronized can be tested.This work was supported by the Natural Sciences and Engineering Research Council of Canada under Grant A-7403.This work has been done during the second author's visit at the University of Waterloo     

Decidability of the equivalence problem for deterministic pushdown automata

Decidability of the equivalence problem is proved for deterministic pushdown automata. A comparison algorithm for two automata is described. The main theorem leads to solution of a number of open problems in the theory of program schemes and in formal language theory.Translated from Kibernetika i Sistemnyi Analiz, No. 5, pp. 20–45, September–October, 1992.     

Security policies enforcement using finite and pushdown edit automata

Edit automata have been introduced by J.Ligatti et al. as a model for security enforcement mechanisms which work at run time. In a distributed interacting system, they play a role of a monitor that runs in parallel with a target program and transforms its execution sequence into a sequence that obeys the security property. In this paper, we characterize security properties which are enforceable by finite edit automata (i.e. edit automata with a finite set of states) and deterministic context-free edit automata (i.e. finite edit automata extended with a stack). We prove that the properties enforceable by finite edit automata are a sub-class of regular sets. Moreover, given a regular set $P$ , one can decide in time $O(n^2)$ , whether $P$ is enforceable by a finite edit automaton (where $n$ is the number of states of the finite automaton recognizing $P$ ) and we give an algorithm to synthesize the controller. Moreover, we prove that safety policies are always enforced by a deterministic context-free edit automaton. We also prove that it is possible to check if a policy is a safety policy in $O(n^4)$ . Finally, we give a topological condition on the deterministic automaton expressing a regular policy enforceable by a deterministic context-free edit automaton.