Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)

Luca Geatti, Alessio Mansutti, Angelo Montanari

This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish…