Feb 25, 2011: Elwin Pater: LTL model checking for LTSmin

February 25, 2011LTL model checking for LTSmin
Room: Zi 5126Elwin Pater

LTSmin is a toolset for manipulating labelled transition systems. It provides the means to generate state spaces from high level specifications through an abstract interface called PINS (Interface for a Partitioned Next State). The PINS interface makes it possible to modularize the design of model checkers, and separate front-end (language) and back-ends (state space generation) completely. Recently the LTSmin toolset has been extended with new enumerative state space generation back-end, based on General State Exploring Algorithms (GSEA). On top of this, an algorithm for verifying liveness properties (Linear Temporal Logic, LTL) is implemented. It works in a modular fashion using the PINS interface to provide the required information. In the talk i will shortly introduce the theory behind LTL model checking using buchi automata, followed by the concrete implementation in LTSmin using the PINS interface.