On the Distributivity of LTL Specifications (bibtex)
by Marko Samer, Helmut Veith
Abstract:
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 LTLQx which guarantees that all specifications obtained from LTLQx are distributive, and all templates not obtained from LTLQx have simple non-distributive instantiations.
Reference:
On the Distributivity of LTL SpecificationsMarko Samer, Helmut VeithACM Transactions on Computational Logic (TOCL), volume 11, number 3, May 2010, ACM.
Bibtex Entry:
@article{SamVei09TOCL,
  author = {Marko Samer and Helmut Veith},
  title = {On the Distributivity of LTL Specifications},
  number = {3},
  month = {May},
  year = {2010},
  journal = {ACM Transactions on Computational Logic (TOCL)},
  publisher = {ACM},
  volume = {11},
  abstract = {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<sup>x</sup> which guarantees that all specifications obtained from LTLQ<sup>x</sup> are distributive, and all templates not obtained from LTLQ<sup>x</sup> have simple non-distributive instantiations.},
  issn = {1529-3785}
}
Powered by bibtexbrowser