Publications in Scientific Journals:
M. Samer, H. Veith:
"On the distributivity of LTL specifications";
ACM Transactions on Computational Logic,
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. . Our main result is a syntactic characterization of distributive LTL queries in terms of LTL templates: we construct a context-free template grammar LTLQx which guarantees that all specifications obtained from LTLQx are distributive, and all templates not obtained from LTLQx have simple nondistributive instantiations.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Created from the Publication Database of the Vienna University of Technology.