Abstract: A Syntactic Characterization of Distributive LTL Queries


Temporal logic query solving, as introduced by Chan in 2000, is a variation of model checking where one subformula of the specification is left open and has to be filled in by the model checker in such a way that the specification becomes true. Motivated by symbolic query solving algorithms for CTL, Chan focussed on a class of CTL queries which have one strongest solution, but no syntactic characterization of this class has been found yet. In this paper, we provide a syntactic characterization for the simpler case of LTL queries. We present a context-free grammar of LTL query templates LTLQ^x which guarantees that (i) all queries in LTLQ^x have at most one strongest solution, and (ii) all query templates not in LTLQ^x have simple instantiations with incomparable strongest solutions. While the LTL case appears to be simpler than the case of CTL, we believe that the proof method exhibited here can be extended to CTL as well.