Ljubljana, Slovenia

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.

Course leader

Luca Geatti and Angelo Montanari

Target group

Students

Fee info

EUR 490: Early student registration
EUR 690: Early non-academic registration

Scholarships

There are several scholarship options which you can read about on our website.