Symbolic model checking for alternating projection temporal logic

Abstract

This paper presents a symbolic model checking approach for Alternating Projection Temporal Logic (APTL). In our approach, the model of a system to be verified is specified by an Interpreted System IS, and a property of the system is expressed by an APTL formula ϕ. To check whether ϕ is valid on IS or not: first, the system IS is symbolically represented and ¬ϕ is transformed into its normal form. Then, the set Sat(¬ϕ), containing all the states from which there exists at least one computation such that ¬ϕ holds, is computed. Finally, whether the property is valid on the system is equivalently evaluated by checking the emptiness of the intersection of the set of initial states in the system and Sat(¬ϕ). Supporting tool is also developed to show how the proposed approach works in practice.