
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.
Logic in computer science, expressiveness, temporal logics over trees, Temporal logic, Expressive power, Kamp's theorem, Theoretical Computer Science, Computer Science(all)
Logic in computer science, expressiveness, temporal logics over trees, Temporal logic, Expressive power, Kamp's theorem, Theoretical Computer Science, Computer Science(all)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
