Logics with rigidly guarded data tests

DOI10.2168/LMCS-11(3:10)2015MaRDI QIDQ3196341zbMATH OpenFDO

Authors Thomas Colcombet, Clemens Ley, Gabriele Puppis

Publication date 29 October 2015

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

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

zbMATH Keywords

data languagesfinite memory automataFO-definabilityorbit-finite data monoidsrigidly guarded MSO

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Algebraic theory of languages and automata (68Q70)

Abstract: The notion of orbit finite data monoid was recently introduced by Bojanczyk as an algebraic object for defining recognizable languages of data words. Following Buchi's approach, we introduce a variant of monadic second-order logic with data equality tests that captures precisely the data languages recognizable by orbit finite data monoids. We also establish, following this time the approach of Schutzenberger, McNaughton and Papert, that the first-order fragment of this logic defines exactly the data languages recognizable by aperiodic orbit finite data monoids. Finally, we consider another variant of the logic that can be interpreted over generic structures with data. The data languages defined in this variant are also recognized by unambiguous finite memory automata.

Recommendations

• On the use of guards for logics with data
• Data monoids
• Nominal monoids
• Automata vs. Logics on Data Words
• Fragments of fixpoint logic on data words

Cited in

(7)

• Nondeterministic and co-nondeterministic implies deterministic, for data languages
• Reasoning About Data Trees Using CHCs
• scientific article; zbMATH DE number 7561623 (Why is no real title available?)
• Nominal monoids
• scientific article; zbMATH DE number 7649885 (Why is no real title available?)
• On the use of guards for logics with data
• Data monoids

Describes a project that uses

Uses Software

• XPath

This page was built for publication: Logics with rigidly guarded data tests

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