Two-Way Unary Temporal Logic over Trees

DOI10.2168/LMCS-5(3:5)2009zbMATH Open1168.03009arXiv0904.4119MaRDI QIDQ3395100FDOQ3395100

Authors: Mikołaj Bojańczyk 

Publication date: 20 August 2009

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

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.

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

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

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)

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)