The Complexity of Counting Models of Linear-time Temporal Logic

TL;DR

This paper analyzes the computational complexity of counting models of bounded size for Linear-time Temporal Logic, revealing varying degrees of difficulty depending on model type and encoding of bounds.

Contribution

It precisely characterizes the complexity classes for counting word and tree models of LTL with different bound encodings, extending understanding of model counting complexity.

Findings

Counting word models is #P-complete with unary bounds.

Counting word models is as hard as counting accepting runs of nondeterministic polynomial space Turing machines with binary bounds.

Counting tree models is as hard as counting accepting runs of nondeterministic exponential time Turing machines.

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.