Model Checking Linear Temporal Logic over Finite Traces

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 \emph{first} study of model-checking from $\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 {\em perceived} to be at most as hard as thoseon $\ltl$, if not easier. For instance, (a). reasoning about $\ltlf$ deals with automata over finite words whereas $\ltl$ requires automata over infinitewords, (b). the complexity of reactive synthesis and satisfiability from $\ltlf$ and $\ltl$ are identical, and so on. We also show that under \emph{terminating} semantics, $\ltlf$ model checking is \pspace-complete. Thus, demonstrating the importance of semantics in model checking for finite-horizon temporal specifications. Contributed talk given by Suguman Bansal

Authors

• Suguman Bansal Georgia Institute of Technology

Keywords

No keywords are indexed for this paper.