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.FSTTCS.2014.241
URN: urn:nbn:de:0030-drops-48463
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4846/
Go to the corresponding LIPIcs Volume Portal

Torfah, Hazem ; Zimmermann, Martin

The Complexity of Counting Models of Linear-time Temporal Logic

pdf-format:
22.pdf (0.5 MB)

Abstract

We determine the complexity of counting models of bounded size of specifications expressed in Linear-time Temporal Logic. Counting word-models is #P-complete, if the bound is given in unary, and as hard as counting accepting runs of nondeterministic polynomial space Turing machines, if the bound is given in binary. Counting tree-models is as hard as counting accepting runs of nondeterministic exponential time Turing machines, if the bound is given in unary. For a binary encoding of the bound, the problem is at least as hard as counting accepting runs of nondeterministic exponential space Turing machines. On the other hand, it is not harder than counting accepting runs of nondeterministic doubly-exponential time Turing machines.

BibTeX - Entry

@InProceedings{torfah_et_al:LIPIcs:2014:4846,
  author =	{Hazem Torfah and Martin Zimmermann},
  title =	{{The Complexity of Counting Models of Linear-time Temporal Logic}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{241--252},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Venkatesh Raman and S. P. Suresh},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4846},
  URN =		{urn:nbn:de:0030-drops-48463},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.241},
  annote =	{Keywords: Model Counting, Temporal Logic, Model Checking, Counting Complexity}
}

Keywords: Model Counting, Temporal Logic, Model Checking, Counting Complexity
Collection: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)
Issue Date: 2014
Date of publication: 12.12.2014

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