Higher-order matching is the problem given t = u where t, u are terms of simply typed lambda-calculus and u is closed, is there a substitution thetas such that tthetas and u have the same normal form with respect to betaeta-equality: can t be pattern matched to u? This paper considers the question: can we characterize the set of all solution terms to a matching problem? We provide an automata-theoretic account that is relative to resource: given a matching problem and a finite set of variables and constants, the (possibly infinite) set of terms that are built from those components and that solve the problem is regular. The characterization uses standard bottom-up tree automata.

This paper defines and examines model checking games for the branching time temporal logic CTL*. The games employ a technique called focus which enriches sets by picking out one distinguished element. This is necessary to avoid ambiguities in the regeneration of temporal operators. The correctness of these games is proved, and optimizations are considered to obtain model checking games for important fragments of CTL*. A game based model checking algorithm that matches the known lower and upper complexity bounds is sketched.

Introduce a simple game-theoretic approach to satisfiability checking of temporal logic, for LTL (linear time logic) and CTL (computation tree logic), which has the same complexity as using automata. The mechanisms involved are both explicit and transparent, and underpin a novel approach to developing complete axiom systems for temporal logic. The axiom systems are naturally factored into what happens locally and what happens in the limit. The completeness proofs utilise the game-theoretic construction for satisfiability: if a finite set of formulas is consistent then there is a winning strategy (and therefore construction of an explicit model is avoided).

Baeten, Bergstra, and Klop (and later Caucal) have proved the remarkable result that bisimulation equivalence is decidable for irredundant context-free grammars. In this paper we provide a much simpler and much more direct proof of this result using a tableau decision method involving goal-directed rules. The decision procedure also provides the essential part of the bisimulation relation between two processes which underlies their equivalence. We also show how to obtain a sound and complete sequent-based equational theory for such processes from the tableau system and how one can extract what Caucal calls a fundamental relation from a successful tableau.

We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal /spl mu/-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal /spl mu/-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes.>

J.C.M. Baeten et al. (Lecture Notes in Computer Science, vol. 259, pp. 93-114, 1987) proved that bisimulation equivalence is decidable for irredundant context-free grammars. A much simpler and much more direct proof of this result is provided now. It uses a tableau decision method involving goal-directed rules. The decision procedure yields an upper bound on a tableau depth. Moreover, it provides the essential part of the bisimulation relation between two processes which underlies their equivalence. A second virtue is that it provides a sound and complete equational theory for such processes.>

Abstract Follow set error recovery is a popular technique, implemented as part of a recursive descent parser, for recovering from syntax errors by editing the input string at the point of error detection. A formal description shows that follow set error recovery is, in actual fact, a family of similar techniques differing according to how follow set is defined. A general algorithm for this family of schemes is offered. Standard accounts mention and make use of non‐systematic, almost ad hoc, additions which improve the performance of the technique. It is shown that some of these additions can be systematized using error productions. Criteria for assessment of the technique are offered. Using these criteria and a database of over 100 example programs three different follow set schemes are assessed with respect to each other.