Complexity of Safety and coSafety Fragments of Linear Temporal Logic

Abstract

ones in such a way to satisfy the formula. LTL realizability Linear Temporal Logic (LTL) is the de-facto standard tempo- is 2EXPTIME-complete, on both infinite (Rosner 1992) and ral logic for system specification, whose foundational prop- finite (De Giacomo and Vardi 2015) traces. erties have been studied for over five decades. Safety and Despite the complexity of these problems, several LTL cosafety properties define notable fragments of LTL, where a tools have been developed, including model checkers and prefix of a trace suffices to establish whether a formula is true translators to automata. However, some applications (such or not over that trace. In this paper, we study the complex- as in runtime verification) do not always require the full ity of the problems of satisfiability, validity, and realizabil- expressivity of LTL, and would rather benefit instead from ity over infinite and finite traces for the safety and cosafety computational efficiency. Several fragments considered in fragments of LTL. As for satisfiability and validity over infi- the literature address these aspects. Two notable ones are the nite traces, we prove that the majority of the fragments have the same complexity as full LTL, that is, they are PSPACE- safety and cosafety fragments (Sistla 1994): they are a sub- complete. The picture is radically different for realizability: class of ω-regular languages where a finite prefix suffices to we find fragments with the same expressive power whose establish the membership of an infinite word to a language, complexity varies from 2EXPTIME-complete (as full LTL) thus allowing one to reason over finite traces. This is very to EXPTIME-complete. Notably, for all cosafety fragments, helpful in practice, e.g., it allows one to avoid Safra’s de- the complexity of the three problems does not change pass- terminization algorithm (Safra 1988) in favor of the classi- ing from infinite to finite traces, while for all safety fragments cal su