Model Checking Finite-Horizon Properties
Abstract:
Recent years have witnessed a growing interest in reasoning about the finite-horizon counterpart of LTL, called LTLf, for systems of unbounded but finite horizons. While the problems of satisfiability and synthesis from LTLf specifications have been studied extensively, the verification problem has surprisingly been overlooked.
To this end, this work presents the first study of the model-checking problem for LTLf specifications. We observe that there are striking differences between LTLf and LTL model checking. Most significantly, under the same non-terminating semantics of models, LTLf model checking is EXPSPACE-complete, making it exponentially harder than LTL model checking. This is unexpected since one of the attributes behind the success of LTLf is that problems over LTLf have so far been perceived to be at most as hard as those over LTL, if not easier. For instance, (a) reasoning about LTLf deals with automata over finite words whereas LTLf requires automata over infinite words, (b) the complexity of reactive synthesis and satisfiability from LTLf and LTL are identical, and so on. We will discuss its implications on LTLf synthesis and the upcoming Reactive Synthesis Competition (SYNTCOMP) 2023.
Bio:
Suguman Bansal is an Assistant Professor in the School of Computer Science at Georgia Institute of Technology. Her research is focused on formal methods and their applications to artificial intelligence, programming languages, and machine learning. Previously, she was an NSF/CRA Computing Innovation Postdoctoral Fellow at the University of Pennsylvania, mentored by Prof. Rajeev Alur. She completed her Ph.D. at Rice University, advised by Prof. Moshe Y. Vardi. She is the recipient of the 2020 NSF CI Fellowship, has been named a 2021 MIT EECS Rising Star, and was a keynote speaker at the 29th Static Analysis Symposium (SAS) 2022.