References & Citations
Computer Science > Logic in Computer Science
Title: Characterization theorems for PDL and FO(TC)
(Submitted on 12 Jan 2015 (v1), last revised 26 Jun 2015 (this version, v2))
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.
Submission history
From: Facundo Carreiro [view email][v1] Mon, 12 Jan 2015 11:36:21 GMT (952kb)
[v2] Fri, 26 Jun 2015 21:24:10 GMT (951kb)
Link back to: arXiv, form interface, contact.