On the distributivity of LTL specifications
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.