11 August 2023
The Safety Fragment of Temporal Logics of Infinite Sequences
In AI and Formal Verification, temporal logics of infinite sequences are extensively used to model, verify, and synthesize hardware and software systems. An important class of them is the safety fragment, that expresses the fact that “something bad never happens”. Languages in this class are such that a prefix of a sequence suffices to establish whether it belongs or not to the language, allowing to reason over finite sequences. The course focuses on such a safety fragment. It defines it, studies its formalizations in terms of first-order logic, temporal logic, and automata, and explores its relationships with the Temporal Hierarchy. Then, it investigates its computational properties, in terms of both worst-case complexity and efficient algorithms for model checking and synthesis. Finally, it discusses succinctness issues.
Luca Geatti and Angelo Montanari
EUR 490: Early student registration
EUR 690: Early non-academic registration
There are several scholarship options which you can read about on our website.