文章基本信息

标题：Automata and temporal logic over arbitrary linear time
本地全文：下载
作者：Julien Cristau
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2009
卷号：4
页码：133-144
DOI：10.4230/LIPIcs.FSTTCS.2009.2313
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Linear temporal logic was introduced in order to reason about reactive systems. It is often considered with respect to infinite words, to specify the behaviour of long-running systems. One can consider more general models for linear time, using words indexed by arbitrary linear orderings. We investigate the connections between temporal logic and automata on linear orderings, as introduced by Bruyere and Carton. We provide a doubly exponential procedure to compute from any LTL formula with \until, \since, and the Stavi connectives an automaton that decides whether that formula holds on the input word. In particular, since the emptiness problem for these automata is decidable, this transformation gives a decision procedure for the satisfiability of the logic.
关键词：LTL; linear orderings; automata