Model checking is verifying automatically that every behavior of a model satisfies a given property, expressed for instance using an LtlFormula.
The automata-theoretic approach to model checking splits the verification process into four operations depicted as rounded boxes on the following pictures.
- (left) From the model you can compute a state graph. A state in the graph corresponds to a configuration of the system modeled, and the arcs depicts the possible evolutions. This graph can be seen as an automaton whose language is the set of all possible execution of the system modeled.
(right) The LtlFormula to verify is also translated into an automaton whose language is the set of all execution that would invalidate the formula. So this is actually the automaton for the negated formula. Several LtlTranslationAlgorithms exist.
(center) The above two automata are combined using a simple operation called synchronized product. This create a third automaton whose language is the intersection of the languages of the two synchronized automata.
(bottom) A last operation, called EmptinessCheck tells whether the language of the synchronized product is empty. If it is not, it contains a sequence of execution that is allowed by the model, but that does invalidate the formula: this is a counter-example. If it does, then the formula holds for all possible execution of the modeled system.
The automata used are Büchi automata (of variants, we use TGBA in Spot) because the sequence considered are infinite.
The first step, translating the model, depends on the formalism used to represent the model and is not offered by Spot. Algorithms for the other steps are covered by Spot (this is what the pink background means).
Moshe Y. Vardi.
An automata-theoretic approach to linear temporal logic.
In Faron Moller and Graham M. Birtwistle, editors, Proceedings
of the 8th Banff Higher Order Workshop (Banff'94), volume 1043 of
Lecture Notes in Computer Science, pages 238-266, Banff, Alberta, Canada,
[ .ps.gz ]