In this paper. we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the PVS theorem prover. Given a parallel composition of sequential processes and a partition of the state space induced by predicates φ₁....,φ_i on the program variables which defines an abstract state space. we construct an abstract state graph, starting in the abstract initial state. The possible successors of a state are computed using the PVS theorem prover by verifying for each index i if φ_i or ¬φ_i is a postcondition of it. This allows an abstract state space exploration for arbitrary programs.

• GrafSaidi97.ps