Two-Way Unary Temporal Logic over Trees

DOI10.2168/LMCS-5(3:5)2009MaRDI QIDQ3395100zbMATH OpenFDO

Authors Mikołaj Bojańczyk

Publication date 20 August 2009

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

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

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Abstract: We consider a temporal logic EF+F^-1 for unranked, unordered finite trees. The logic has two operators: EFphi, which says "in some proper descendant phi holds", and F^-1phi, which says "in some proper ancestor phi holds". We present an algorithm for deciding if a regular language of unranked finite trees can be expressed in EF+F^-1. The algorithm uses a characterization expressed in terms of forest algebras.

Recommendations

• EF+EX forest algebras
• A family of temporal logics on finite trees
• Expressive completeness of temporal logic of trees
• EXTENDED TEMPORAL LOGICS ON FINITE TREES
• Algebra for Infinite Forests with an Application to the Temporal Logic EF

Cited in

(3)

• EXTENDED TEMPORAL LOGICS ON FINITE TREES
• Algebra for trees
• Algebra for Infinite Forests with an Application to the Temporal Logic EF

This page was built for publication: Two-Way Unary Temporal Logic over Trees

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