Alternation Is Strict For Higher-Order Modal Fixpoint Logic

Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words

It is well-known that every first-order property on words is expressible using at most three variables. The subclass of properties expressible with only two variables is also quite interesting and well-studied. We prove precise structure theorems that characterize the exact expressive power of first-order logic with two variables on words. Our results apply to both the case with and without a successor relation. For both languages, our structure theorems show exactly what is expressible using a given quantifier depth, n, and using m blocks of alternating quantifiers, for any m \leq n. Using th…

Fixpoint Node Selection Query Languages for Trees

The study of node selection query languages for (finite) trees has been a major topic in the recent research on query languages for Web documents. On one hand, there has been an extensive study of XPath and its various extensions. On the other hand, query languages based on classical logics, such as first-order logic (FO) or Monadic Second-Order Logic (MSO), have been considered. Results in this area typically relate an XPath-based language to a classical logic. What has yet to emerge is an XPath-related language that is as expressive as MSO, and at the same time enjoys the computational prope…

概率高阶不动点逻辑

A Probabilistic Higher-order Fixpoint Logic

本文提出概率高阶不动点逻辑PHFL，证明其表达力强于$\mu^p$-演算，有限马尔可夫链模型检验不可判定，并给出可判定片段。

作为不动点和博弈的微分方程

Differential Equations as Fixpoints and Games

研究通过证明一阶博弈逻辑GL与一阶模态μ-演算L_mu等表达且等价，统一博弈与不动点。还证明了微分方程扩展dGL和微分模态μ-演算的等表达性与等价性，可对常微分方程完全公理化，通过证明搜索判定其性质，有理博弈得出dGL的强算术完备性定理。

Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy

Given two structures $G$ and $H$ distinguishable in $\fo k$ (first-order logic with $k$ variables), let $A^k(G,H)$ denote the minimum alternation depth of a $\fo k$ formula distinguishing $G$ from $H$. Let $A^k(n)$ be the maximum value of $A^k(G,H)$ over $n$-element structures. We prove the strictness of the quantifier alternation hierarchy of $\fo 2$ in a strong quantitative form, namely $A^2(n)\ge n/8-2$, which is tight up to a constant factor. For each $k\ge2$, it holds that $A^k(n)>\log_{k+1}n-2$ even over colored trees, which is also tight up to a constant factor if $k\ge3$. For $k\ge 3$ …

Distributed Automata and Logic

Distributed automata are finite-state machines that operate on finite directed graphs. Acting as synchronous distributed algorithms, they use their input graph as a network in which identical processors communicate for a possibly infinite number of synchronous rounds. For the local variant of those automata, where the number of rounds is bounded by a constant, Hella et al. (2012, 2015) have established a logical characterization in terms of basic modal logic. In this thesis, we provide similar logical characterizations for two more expressive classes of distributed automata. The first class ex…

Alternating Set Quantifiers in Modal Logic

We establish the strictness of several set quantifier alternation hierarchies that are based on modal logic, evaluated on various classes of finite graphs. This extends to the modal setting a celebrated result of Matz, Schweikardt and Thomas (2002), which states that the analogous hierarchy of monadic second-order logic is strict. Thereby, the present paper settles a question raised by van Benthem (1983), revived by ten Cate (2006), and partially answered by Kuusisto (2008, 2015).

Filtration and canonical completeness for continuous modal mu-calculi

The continuous modal mu-calculus is a fragment of the modal mu-calculus, where the application of fixpoint operators is restricted to formulas whose functional interpretation is Scott-continuous, rather than merely monotone. By game-theoretic means, we show that this relatively expressive fragment still allows two important techniques of basic modal logic, which notoriously fail for the full modal mu-calculus: filtration and canonical models. In particular, we show that the Filtration Theorem holds for formulas in the language of the continuous modal mu-calculus. As a consequence we obtain the…

A Type-Based HFL Model Checking Algorithm

Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL model checking: the problem of whether a given finite state system satisfies a given HFL formula. In this paper, we propose a novel algorithm for HFL model checking: it is the first practical algorithm in that it runs fast for typical inputs, despite the hyper-exponential worst-case complexity of the HFL model checking problem. Our algorithm is …

典范模型与模态团队逻辑的复杂性

Canonical Models and the Complexity of Modal Team Logic

该研究通过引入典范模型将模态团队逻辑MTL的可满足性简化为模型检验，并证明其复杂性为TOWER(poly)完全问题，同时刻画了有界模态深度片段的初等层级复杂性。