Paper: On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees (at LICS 1987)

Authors: Wolfgang Thomas

Abstract

We study "chain logic" over infinite valued trees, a fragment of (Rabin's) monadic tree theory in which set quantification is restricted to chains, i.e. sets which are linearly ordered in the partial tree ordering. Chain logic suffices for many applications of Rabin's tree theory to modal logics or program logics. We characterize chain logic and subsystems of it (for example "path logic") in terms of regular-like expressions and connect them with algebraic language theory by introducing appropriate "tree monoids". As a consequence we obtain decidability results on expressiveness (e.g. for the problem whether a chain logic formula is equivalent to a path logic formula). An application in branching time logic is outlined.

BibTeX

  @InProceedings{Thomas-OnChainLogicPathLog,
    author = 	 {Wolfgang Thomas},
    title = 	 {On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {245--256},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }