FO^2(<,+1,) on data trees, data tree automata and branching vector addition systems

DOI10.2168/LMCS-12(2:3)2016zbMATH Open1448.68227arXiv1601.01579MaRDI QIDQ2804201FDOQ2804201

Luc Segoufin, Jérémie Dimino, Florent Jacquemard

Publication date: 28 April 2016

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: A data tree is an unranked ordered tree where each node carries a label from a finite alphabet and a datum from some infinite domain. We consider the two variable first order logic FO2(<,+1,~) over data trees. Here +1 refers to the child and the next sibling relations while < refers to the descendant and following sibling relations. Moreover, ~ is a binary predicate testing data equality. We exhibit an automata model, denoted DAD# that is more expressive than FO2(<,+1,~) but such that emptiness of DAD# and satisfiability of FO2(<,+1,~) are inter-reducible. This is proved via a model of counter tree automata, denoted EBVASS, that extends Branching Vector Addition Systems with States (BVASS) with extra features for merging counters. We show that, as decision problems, reachability for EBVASS, satisfiability of FO2(<,+1,~) and emptiness of DAD# are equivalent.

Full work available at URL: https://arxiv.org/abs/1601.01579

zbMATH Keywords

data automatatwo-variable logiccounter automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Data structures (68P05) Automata and formal grammars in connection with logical questions (03D05) Logic in computer science (03B70)

Cited In (4)

• On regular paths with counting and data tests
• Forward analysis for WSTS, part I: completions
• ML and Extended Branching VASS
• Logics of Repeating Values on Data Trees and Branching Counter Systems

This page was built for publication: \(\mathsf{FO}^2(<,+1,\sim)\) on data trees, data tree automata and branching vector addition systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804201)