License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.254
URN: urn:nbn:de:0030-drops-53767
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5376/
Go to the corresponding LIPIcs Volume Portal

Chen, Taolue ; Song, Fu ; Wu, Zhilin

On the Satisfiability of Indexed Linear Temporal Logics

pdf-format:
16.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{chen_et_al:LIPIcs:2015:5376,
  author =	{Taolue Chen and Fu Song and Zhilin Wu},
  title =	{{On the Satisfiability of Indexed Linear Temporal Logics}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{254--267},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Luca Aceto and David de Frutos Escrig},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5376},
  URN =		{urn:nbn:de:0030-drops-53767},
  doi =		{10.4230/LIPIcs.CONCUR.2015.254},
  annote =	{Keywords: Satisfiability, Indexed linear temporal logic, Parameterised systems}
}

Keywords: Satisfiability, Indexed linear temporal logic, Parameterised systems
Collection: 26th International Conference on Concurrency Theory (CONCUR 2015)
Issue Date: 2015
Date of publication: 26.08.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI