DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2026.19

Characterizing LTL Formulas by Examples

Authors: Balder ten Cate, Dana Fisman, Roi Ohayon, and Patrik Sestic

Published in: LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)

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.

Cite as

Balder ten Cate, Dana Fisman, Roi Ohayon, and Patrik Sestic. Characterizing LTL Formulas by Examples. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 19:1-19:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{tencate_et_al:LIPIcs.MFCS.2026.19,
  author =	{ten Cate, Balder and Fisman, Dana and Ohayon, Roi and Sestic, Patrik},
  title =	{{Characterizing LTL Formulas by Examples}},
  booktitle =	{51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)},
  pages =	{19:1--19:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-442-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{386},
  editor =	{Kouck\'{y}, Michal and Petrișan, Daniela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.19},
  URN =		{urn:nbn:de:0030-drops-274000},
  doi =		{10.4230/LIPIcs.MFCS.2026.19},
  annote =	{Keywords: Linear Temporal Logic, Examples, Transfinite Words}
}

Search Results

Documents authored by Sestic, Patrik

Characterizing LTL Formulas by Examples

Abstract

Cite as

Thanks for your feedback!

Could not send message