Torfah, Hazem and Zimmermann, Martin ORCID: 0000-0002-8038-2453
(2018)
The complexity of counting models of linear-time temporal logic.
ACTA INFORMATICA, 55 (3).
pp. 191-212.
Text
main.pdf - Author Accepted Manuscript Download (660kB) | Preview |
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.
Item Type: | Article |
---|---|
Additional Information: | A short version appears in Proceedings of FSTTCS 2014 |
Uncontrolled Keywords: | cs.LO, cs.LO, cs.CC, F.4.1 |
Depositing User: | Symplectic Admin |
Date Deposited: | 15 Jul 2019 12:47 |
Last Modified: | 19 Jan 2023 00:37 |
DOI: | 10.1007/s00236-016-0284-z |
Related URLs: | |
URI: | https://livrepository.liverpool.ac.uk/id/eprint/3050008 |