Characterization theorems for PDL and FO(TC)

TL;DR

This paper provides a detailed characterization of the expressiveness and relationships between PDL, FO(TC), FO(LFP), and WCL, including automata-based characterizations and bisimulation invariance results.

Contribution

It offers a syntactic and semantic link between FO(TC^1) and FO(LFP), introduces new automata for trees capturing FO(TC^1) and WCL, and establishes PDL as the bisimulation-invariant fragment of these logics.

Findings

Characterization of FO(TC^1) and FO(LFP) relationship

Introduction of parity automata for trees capturing FO(TC^1) and WCL

Bisimulation-invariant characterization of PDL

Abstract

Our main contributions can be divided in three parts: (1) Fixpoint extensions of first-order logic: we give a precise syntactic and semantic characterization of the relationship between $\mathrm{FO(TC^1)}$ and $\mathrm{FO(LFP)}$; (2) Automata and expressiveness on trees: we introduce a new class of parity automata which, on trees, captures the expressive power of $\mathrm{FO(TC^1)}$ and WCL (weak chain logic). The latter logic is a variant of MSO which quantifies over finite chains; and (3) Expressiveness modulo bisimilarity: we show that PDL is expressively equivalent to the bisimulation-invariant fragment of both $\mathrm{FO(TC^1)}$ and WCL. In particular, point (3) closes the open problems of the bisimulation-invariant characterizations of PDL, $\mathrm{FO(TC^1)}$ and WCL all at once.