کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
421797 | 684963 | 2011 | 14 صفحه PDF | دانلود رایگان |
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.
Journal: Electronic Notes in Theoretical Computer Science - Volume 278, 3 November 2011, Pages 115-128