Expressiveness of Hybrid Temporal Logic on Data Words

摘要

Hybrid temporal logic (HTL) on data words can be considered as an extension of the logic LTL↓introduced by Demri and Lazic [Stephane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. In LICS?06: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, pages 17–26, Washington, DC, USA, 2006. IEEE Computer Society]. The paper compares the expressive power of HTL on data words with that of LTL↓. It is shown that there are properties of data words that can be expressed in HTL with two variables but not in LTL↓. On the other hand, every property that can be expressed in HTL with one variable can also be expressed in LTL↓with one variable. The paper further studies the succinctness of HTL in comparison with LTL↓and shows that the number-of-variables hierarchy of HTL is infinite.