文章基本信息

标题：On the Satisfiability of Indexed Linear Temporal Logics
本地全文：下载
作者：Taolue Chen ; Fu Song ; Zhilin Wu 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：42
页码：254-267
DOI：10.4230/LIPIcs.CONCUR.2015.254
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Indexed Linear Temporal Logics (ILTL) are an extension of standard Linear Temporal Logics (LTL) with quantifications over index variables which range over a set of process identifiers. ILTL has been widely used in specifying and verifying properties of parameterised systems, e.g., in parameterised model checking of concurrent processes. However there is still a lack of theoretical investigations on properties of ILTL, compared to the well-studied LTL. In this paper, we start to narrow this gap, focusing on the satisfiability problem, i.e., to decide whether a model exists for a given formula. This problem is in general undecidable. Various fragments of ILTL have been considered in the literature typically in parameterised model checking, e.g., ILTL formulae in prenex normal form, or containing only non-nested quantifiers, or admitting limited temporal operators. We carry out a thorough study on the decidability and complexity of the satisfiability problem for these fragments. Namely, for each fragment, we either show that it is undecidable, or otherwise provide tight complexity bounds.
关键词：Satisfiability; Indexed linear temporal logic; Parameterised systems