Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

First-Order Logic on Higher-Order Nested Pushdown Trees

We introduce a new hierarchy of higher-order nested pushdown trees generalising Alur et al.'s concept of nested pushdown trees. Nested pushdown trees are useful representations of control flows in the verification of programs with recursive calls of first-order functions. Higher-order nested pushdown trees are expansions of unfoldings of graphs generated by higher-order pushdown systems. Moreover, the class of nested pushdown trees of level n is uniformly first-order interpretable in the class of collapsible pushdown graphs of level n+1. The relationship between the class of higher-order pushd…

Nested Words for Order-2 Pushdown Systems

We study linear time model checking of collapsible higher-order pushdown systems (CPDS) of order 2 (manipulating stack of stacks) against MSO and PDL (propositional dynamic logic with converse and loop) enhanced with push/pop matching relations. To capture these linear time behaviours with matchings, we propose order-2 nested words. These graphs consist of a word structure augmented with two binary matching relations, one for each order of stack, which relate a push with matching pops (or collapse) on the respective stack. Due to the matching relations, satisfiability and model checking are un…

Reachability relations of timed pushdown automata

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 v…

The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.

互模拟语义中的并行下推自动机与交换上下文无关文法（扩展摘要）

Parallel Pushdown Automata and Commutative Context-Free Grammars in Bisimulation Semantics (Extended Abstract)

本文研究了在互模拟语义下，将经典下推自动机与上下文无关文法等价定理扩展至并行下推自动机与带并行性进程代数的情况。

一种面向动态线程创建的递归程序的导航逻辑

A Navigation Logic for Recursive Programs with Dynamic Thread Creation

本文提出时序逻辑NTL，用于推理动态下推网络中递归程序的调用、返回及动态线程创建行为，并证明其模型检测与可满足性问题的复杂度不高于下推系统上的LTL，为验证此类程序提供了新途径。

POPACheck：概率下推自动机的模型检查工具

POPACheck: A Model Checker for Probabilistic Pushdown Automata

POPACheck 是一种用于概率下推自动机的模型检查工具，支持时序逻辑规范，能处理概率程序的行为验证。

Type homogeneity is not a restriction for safe recursion schemes

Knapik et al. introduced the safety restriction which constrains both the types and syntax of the production rules defining a higher-order recursion scheme. This restriction gives rise to an equi-expressivity result between order-n pushdown automata and order-n safe recursion schemes, when such devices are used as tree generators. We show that the typing constraint of safety, called homogeneity, is unnecessary in the sense that imposing the syntactic restriction alone is sufficient to prove the equi-expressivity result for trees.

Algebraic Synchronization Trees and Processes

We study algebraic synchronization trees, i.e., initial solutions of algebraic recursion schemes over the continuous categorical algebra of synchronization trees. In particular, we investigate the relative expressive power of algebraic recursion schemes over two signatures, which are based on those for Basic CCS and Basic Process Algebra, as a means for defining synchronization trees up to isomorphism as well as modulo bisimilarity and language equivalence. The expressiveness of algebraic recursion schemes is also compared to that of the low levels in Caucal's pushdown hierarchy.

Visibly Pushdown Modular Games

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 aut…

Finitary semantics of linear logic and higher-order model-checking

In this paper, we explain how the connection between higher-order model-checking and linear logic recently exhibited by the authors leads to a new and conceptually enlightening proof of the selection problem originally established by Carayol and Serre using collapsible pushdown automata. The main idea is to start from an infinitary and colored relational semantics of the lambdaY-calculus already formulated, and to replace it by its finitary counterpart based on finite prime-algebraic lattices. Given a higher-order recursion scheme G, the finiteness of its interpretation in the model enables us…

Verification of recursive parallel systems

In this paper we consider the problem of proving properties of infinite behaviour of formalisms suitable to describe (infinite state) systems with recursion and parallelism. As a formal setting, we consider the framework of Process Rewriting Systems (PRSs). For a meaningfull fragment of PRSs, allowing to accommodate both Pushdown Automata and Petri Nets, we state decidability results for a class of properties about infinite derivations (infinite term rewritings). The given results can be exploited for the automatic verification of some classes of linear time properties of infinite state system…