Description

Model checkers are fully automated verification tools. You might have seen some model checkers before (like Uppaal, Spin, or LTSmin), but that is not necessary. A model checker has two inputs: (1) a model of some system; (2) a property that should hold. The output is a yes/no verdict, and in case of a no-verdict also a counter-example to the property.

The high-performance model checker LTSmin is developed in Twente. It has two characteristics that set it apart:
* it can be linked to many specification languages (like Uppaal, Promela, Petri-Nets, etc.)
* it provides high-performance algorithms (e.g., multi-core and distributed algorithms).

This assignment is about the property languages. An example property could be:

ALWAYS (lift.button=PRESSED at 0  =>  EVENTUALLY (lift.cabin=ARRIVE at 0))

which simply states that whenever the lift is requested at floor 0, it will arrive there sooner or later. Here "ALWAYS",  "EVENTUALLY" and "=>" are properties from temporal logic, while "lift.button=PRESSED at 0" and "lift.cabin=ARRIVE at 0" are atomic properties, dependent on the specified model.

There are three challenges / tasks for you:

1. There are several temporal logics. It would be your task to write (or extend) parsers for them, translate one into the other, or maybe even design a "most general" temporal logic.

2. The atomic properties depend on the particular specification and specification language, and LTSmin is language-agnostic. How can we solve this during parsing (and type-checking)?

3. Part of the assignment is definitely to document the property language, so end users can use your work!

The research part could be on the design and translation of property languages, or on the language technology to combine different parsers.

You can easily learn sufficient knowledge on temporal logic and for this assignment it is not necessary to understand the model checking algorithms in LTSmin. This assignment does require some familiarity with compiler construction methods (like parsing and expression transformation), and the willingness to program stuff. 

References

1. LTSmin website (Digital version available here)
2. An example temporal logic (Digital version available here)
3. LTSmin on github (Digital version available here)

Additional Resources

1. Paper