Résumé
In this paper, we focus on the application of LTL (Linear Temporal Logic) model checking on logical diagrams (LD), which are a type of functional specification used for logical controllers in many nuclear power plants. The goal is to check properties on LDs and to generate counter examples serving as validation tests for logical controllers. We propose a sound and complete LTL encoding framework for LDs allowing the use of model checking (MC) and evaluate different MC techniques on real world LD to efficiently generate counterexamples for verifiable properties.