Abstract: On the Distributivity of LTL Specifications


In this paper 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 non-distributive instantiations.