A mechanisation of some context-free language theory in HOL4

We describe the mechanisation of some foundational results in the theory of context-free languages (CFLs), using the HOL4 system. We focus on pushdown automata (PDAs). We show that two standard acceptance criteria for PDAs (“accept-by-empty-stack” and “accept-by-final-state”) are equivalent in power. We are then able to show that the pushdown automata (PDAs) and context-free grammars (CFGs) accept the same languages by showing that each can emulate the other. With both of these models to hand, we can then show a number of basic, but important results. For example, we prove the basic closure properties of the context-free languages such as union and concatenation. Along the way, we also discuss the varying extent to which textbook proofs (we follow Hopcroft and Ullman) and our mechanisations diverge: sometimes elegant textbook proofs remain elegant in HOL; sometimes the required mechanisation effort blows up unconscionably.     

Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time

We prove that weak bisimilarity is decidable in polynomial time between finite-state systems and several classes of infinite-state systems: context-free processes and normed basic parallel processes (normed BPP). To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity problems involving infinite-state systems.     

A hierarchy of deterministic context-free ω-languages

Twenty years ago, Klaus. W. Wagner came up with a hierarchy of ω-regular sets that actually bears his name. It turned out to be exactly the Wadge hierarchy of the sets of ω-words recognized by deterministic finite automata. We describe the Wadge hierarchy of context-free ω-languages, which stands as an extension of Wagner's work from automata to pushdown automata.     

Analyzing ambiguity of context-free grammars

It has been known since 1962 that the ambiguity problem for context-free grammars is undecidable. Ambiguity in context-free grammars is a recurring problem in language design and parser generation, as well as in applications where grammars are used as models of real-world physical structures.We observe that there is a simple linguistic characterization of the grammar ambiguity problem, and we show how to exploit this by presenting an ambiguity analysis framework based on conservative language approximations. As a concrete example, we propose a technique based on local regular approximations and grammar unfoldings. We evaluate the analysis using grammars that occur in RNA analysis in bioinformatics, and we demonstrate that it is sufficiently precise and efficient to be practically useful.     

Linearity and nondeletion on monadic context-free tree grammars

In this paper, subclasses of monadic context-free tree grammars (CFTGs) are compared. Since linear, nondeleting, monadic CFTGs generate the same class of string languages as tree adjoining grammars (TAGs), it is examined whether the restrictions of linearity and nondeletion on monadic CFTGs are necessary to generate the same class of languages.     

An undecidable property of context-free linear orders

We prove that there exists no algorithm to decide whether the language generated by a context-free grammar is dense with respect to the lexicographic ordering. As a corollary to this result, we show that it is undecidable whether the lexicographic orderings of the languages generated by two context-free grammars have the same order type.     

Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes

In a recent paper Baier et al. [Lecture Notes in Computer Science, Springer-Verlag, 2000, p. 358] analyzed a new way of model-checking formulas of a logic for continuous-time processes—called continuous stochastic logic (henceforth CSL)—against continuous-time Markov chains—henceforth CTMCs. One of the important results of that paper was the proof that if two CTMCs were bisimilar then they would satisfy exactly the same formulas of CSL. This raises the converse question—does satisfaction of the same collection of CSL formulas imply bisimilarity? In other words, given two CTMCs which are known to satisfy exactly the same formulas of CSL does it have to be the case that they are bisimilar? We prove that the answer to the question just raised is “yes”. In fact we prove a significant extension, namely that a subset of CSL suffices even for systems where the state space may be a continuum. Along the way we prove a result to the effect that the set of Zeno paths has measure zero provided that the transition rates are bounded.     

On the synchronized derivation depth of context-free grammars

We consider depth of derivations as a complexity measure for synchronized and ordinary context-free grammars. This measure differs from the earlier considered synchronization depth in that it counts the depth of the entire derivation tree. We consider (non-)existence of trade-offs when using synchronized grammars as opposed to non-synchronized grammars and establish lower bounds for certain classes of linear context-free languages.     

Permutations are not context-free: An application of the interchange lemma

Let x be a nonempty string and x? another string with the same characters as x, but possibly in a different order. A string of the form xx? is called a permutation. A permutation-containing string is of the form wxx?y. The Interchange Lemma for context-free languages [11] is used to show that the set of permutation-containing strings over a 16 character alphabet is not context-free. The application of the lemma is important since other techniques, such as the pumping lemma and Ogden's lemma cannot show that the set is not context-free. Finally, a collection of open problems is given.     

Detecting patterns in finite regular and context-free languages

We consider some natural variations on the following classic pattern-matching problem: given an NFA M over the alphabet Σ and a pattern p over some alphabet Δ, does there exist a word x∈L(M) such that x matches p? We consider the restricted problem where M only accepts a finite language. We also consider the variation where only some factor of x is required to match the pattern p. We show that both of these problems are NP-complete. We also consider the same problems for context-free grammars; in this case the problems become PSPACE-complete.     

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.     

Closure properties of linear context-free tree languages with an application to optimality theory

Context-free tree grammars, originally introduced by Rounds [Math. Systems Theory 4(3) (1970) 257–287], are powerful grammar devices for the definition of tree languages. The properties of the class of context-free tree languages have been studied for more than three decades now. Particularly important here is the work by Engelfriet and Schmidt [J. Comput. System Sci. 15(3) (1977) 328–353, 16(1) (1978) 67–99]. In the present paper, we consider a subclass of the class of context-free tree languages, namely the class of linear context-free tree languages. A context-free tree grammar is linear, if no rule permits the copying of subtrees. For this class of linear context-free tree languages we show that the grammar derivation mode, which is very important for the general class of context-free tree languages, is immaterial. The main result we present is the closure of the class of linear context-free tree languages under linear frontier-to-root tree transduction mappings. Two further results are the closure of this class under linear root-to-frontier tree transduction mappings and under intersection with regular tree languages.     

Decidability of performance equivalence for basic parallel processes

We study an extension of the class of Basic Parallel Processes (BPP), in which actions are durational and urgent and parallel components have independent local clocks. The main result is decidability of strong bisimilarity, known also as performance equivalence, in this class. This extends the earlier decidability result for plain BPP by Christensen et al. Our decision procedure is based on decidability of the validity problem for Presburger arithmetic. We prove also polynomial complexity in positive-duration fragment, thus properly extending a previous result by Bérard et al. Both ill-timed and well-timed semantics are treated.