Advancements in Reachability Analysis using Transition Relations

Abstract

State space traversal of Finite State Machines is a core technique for several formal verification tasks. Within this framework, Transition Relations (TRs) are a very expressive and powerful way to represent and manipulate state transition graphs. State-of-the-art breadth-first traversals adopt partitioned/clustered TRs, combined with the early quantification scheme, to achieve efficient image/preimage computations. This talk discusses further optimizations to TR usage in the synchronous domain: (a) Disjunctive partitioning, (b) Selective traversal/squaring, (c) Timed Transition Relations.

Disjunctive partitioning is based on splitting variable selection, and it may be viewed as a divide-and-conquer approach to large problems.

Selective traversal/squaring combines aspects of partitioning with the ability to concentrate on particular properties or sub-behaviors (functional modes).

Timed Transition Relations are proposed to extend traditional TRs for some verification, synthesis and cycle-based simulation tasks, characterized by reactive behaviors and the necessity to measure time along state transition sequences.

The work presented is partly based on papers presented at ICCAD'96 and DAC'97, and on new research done in cooperation with Paolo Camurati and Luciano Lavagno.