文章基本信息

标题：Temporal Logics on Words with Multiple Data Values
本地全文：下载
作者：Ahmet Kara ; Thomas Schwentick ; Thomas Zeume 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2010
卷号：8
页码：481-492
DOI：10.4230/LIPIcs.FSTTCS.2010.481
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：The paper proposes and studies temporal logics for attributed words, that is, data words with a (finite) set of (attribute,value)-pairs at each position. It considers a basic logic which is a semantical fragment of the logic $\LTL^\downarrow_1$ of Demri and Lazic with operators for navigation into the future and the past. By reduction to the emptiness problem for data automata it is shown that this basic logic is decidable. Whereas the basic logic only allows navigation to positions where a fixed data value occurs, extensions are studied that also allow navigation to positions with different data values. Besides some undecidable results it is shown that the extension by a certain UNTIL-operator with an inequality target condition remains decidable.
关键词：Expressiveness; Decidability; Temporal Logic; Data words