Zeitschriftenartikel:
M. Samer, H. Veith:
"On the distributivity of LTL specifications";
ACM Transactions on Computational Logic,
11
(2010),
3.
Kurzfassung englisch:
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 LTLQx which guarantees that all specifications obtained from LTLQx are distributive, and all templates not obtained from LTLQx have simple nondistributive instantiations.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1145/1740582.1740588
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.