Symbolic Model Checking for Alternating Projection Temporal Logic

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 phi. To check whether f is valid on IS or not: first, the system IS is symbolically represented and (sic)phi is transformed into its normal form. Then, the set Sat((sic)phi), containing all the states from which there exists at least one computation such that (sic)phi 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((sic)phi). Supporting tool is also developed to show how the proposed approach works in practice.