Arity hierarchy for temporal logics
type: Item
instance of: scholarly article
title: Arity hierarchy for temporal logics
zbMATH Open document ID: 1151.03010
author: Alexander Rabinovich
published in: Theoretical Computer Science
publication date: 2008-09-16T00:00:00Z
review text: The paper studies the expressive power of temporal logics over trees. The main result states that in contrast to Kamp's theorem (stating, inter alia, that the temporal logic with ``Until'' and ``Since'' is expressively complete for the monadic first-order logic over the linear order of natural numbers), for every \(n\) there is a modality of arity \(n\) definable by a monadic logic formula, which is not equivalent over trees to any temporal logic formula which uses modalities of arity less than \(n\). The proof uses an instance of Shelah's composition theorem. Interesting corollaries of this result are, e.g., new proofs that CTL* and ECTL+ have no finite bases.
reviewed by: Valentin Goranko
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 5344355
zbMATH Keywords: temporal logics over trees
zbMATH Keywords: expressiveness
zbMATH Keywords: Kamp's theorem
MaRDI profile type: Publication
full work available at URL: j.tcs.2008.06.006
OpenAlex ID: W2113574473
cites work: Monadic Logic of Order over Naturals has no Finite Base
cites work: Q3336675
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Q3906386
cites work: Q4385542
cites work: “Sometimes” and “not never” revisited
cites work: The first order properties of products of algebraic systems
cites work: Q3835817
cites work: Q3757893
cites work: The decision problem for branching time logic
cites work: Q5572332
cites work: Uniformization, choice functions and well orders in the class of trees
cites work: Fairness and related properties in transition systems - a temporal logic to deal with fairness
cites work: Q4484477
cites work: An infinite hierarchy of temporal logics over branching time
cites work: \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\)
cites work: Q2757841
cites work: Expressive completeness of temporal logic of trees
cites work: The monadic theory of order
cites work: Q4362730
cites work: Q3341881
DOI: 10.1016/J.TCS.2008.06.006
description: scientific article; zbMATH DE number 5344355