Olivier Coudert, Jean Christophe Madre, Christian Berthet: Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams. CAV 1990: 23-32