Characterizing LTL Formulas by Examples
It provides a foundational understanding of the descriptive power of different example types for example-driven specification, debugging, and learning of temporal properties.
This paper investigates how Linear Temporal Logic (LTL) formulas can be uniquely characterized by finite sets of labeled examples, providing a complete classification for basis-restricted LTL fragments and showing that transfinite words and schematic examples enable unique characterizations for larger fragments.
We investigate the extent to which Linear Temporal Logic (LTL) formulas can be uniquely characterized by a finite set of labeled examples. We consider different types of examples, ranging from finite words to transfinite words, as well as schematic examples. In the finite-word setting, we provide a complete classification of basis-restricted LTL fragments that admit such unique characterizations. Next, we show that allowing transfinite words as examples enables finite unique characterizations for large monotone fragments of LTL. Finally, we introduce schematic examples, i.e., patterns that compactly represent a family of finite words, and we show that these enable unique characterization results in the finite setting that were not possible with ordinary finite examples alone. Overall, the work provides a foundational account of the descriptive power of different example types for example-driven specification, debugging, and learning of temporal properties.