In this article, we investigate LTL specifications where γ[φ ∧ ψ] is equivalent to γ[φ] ∧ γ[ψ] independent of φ and ψ. Formulas γ with this property are called distributive queries because they naturally arise in Chan's seminal approach to temporal logic query solving [Chan 2000]. As recognizing distributive LTL queries is PSpace-complete, we consider distributive fragments of LTL defined by templates as in Buccafurri et al. [2001]. Our main result is a syntactic characterization of distributive LTL queries in terms of LTL templates: we construct a context-free template grammar LTLQ x which guarantees that all specifications obtained from LTLQ x are distributive, and all templates not obtained from LTLQ x have simple nondistributive instantiations.

Temporal logic queries provide a natural framework to extend the realm of model checking from mere verification of engineers' specifications to computing previously unknown temporal properties of a system. Formally, temporal logic queries are patterns of temporal logic specifications which contain placeholders for subformulas; a solution to a temporal logic query is an instantiation which renders the specification true. In this paper, we investigate temporal logic queries that can be solved deterministically, i.e., solving such queries can be reduced in a deterministic manner to solving their subqueries at appropriate system states. We show that this kind of determinism is intimately related to the notion of intermediate collecting queries studied by the authors in previous work. We describe a large class of deterministically solvable CTL queries and devise a BDD-based symbolic algorithm for this class.