How does a Linear Temporal Logic (LTL) can be useful to validate linear temporal specifications?

In this post I am going to share my B.Sc. final project about Fast LTL Satisfiability Checking by SAT Solvers, based on a new method from the following research: https://arxiv.org/pdf/1401.5677.pdf

To get into it, let us think about an example. Assume we have a multithreaded application that handles a critical section, as well, during the run we must prevent two threads to enter the same critical section, which can result in an undefined behavior.

This requirement can be formulated by the following LTL formula: G(~at_crit1 V ~at_crit2) where G is a Globally operator and at_crit1, at_crit2 are Atomic Propositions that describe critical section properties in our system’s design.

If such formula is satisfiable, it means that this requirement can be designed and implemented.

The complexity of LTL satisfiability checking is PSPACE-complete, which considered as a very difficult problem in the computer science field.

The method that presented in the paper describes how to reduce the original problem into a much simpler one which results in a linear complexity (in average) for satisfiable formulas, which makes the checking fast (for most of the cases).

Experiments

The application that I developed is a tool that loads such formulas from a text file, executes the algorithm which I implemented by following the paper, then execution time and satisfiability result per formula will be logged. In addition, my project calculates and presents statistics about the efficiency of this method by analyzing the results.

Some of the fundamentals I used in the implementation are: Data Structures, Dynamic Programming, Reverse Polish Notation, Caching and Web Sockets communication.

Here is my project document for more details.