Characterizing LTL Formulas by Examples

TL;DR

This paper explores how different types of labeled examples can uniquely characterize LTL formulas, advancing understanding of their descriptive power for specification and learning.

Contribution

It provides a classification of LTL fragments based on example types and introduces schematic examples for enhanced characterization.

Findings

Finite examples classify certain LTL fragments.

Transfinite examples enable characterization of larger fragments.

Schematic examples allow compact representation and unique characterization.

Abstract

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.