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 $$i¾?. To check whether $$\phi $$i¾? is valid on IS or not: first, the system IS is symbolically represented and $$\lnot \phi $$i¾?i¾? is transformed into its normal form. Then, the set $$Sat\lnot \phi $$Sati¾?i¾?, containing all the states from which there exists at least one computation such that $$\lnot \phi $$i¾?i¾? 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\lnot \phi $$Sati¾?i¾?. Supporting tool is also developed to show how the proposed approach works in practice.
['Haiyang Wang', 'Zhenhua Duan', 'Cong Tian']
Symbolic Model Checking for Alternating Projection Temporal Logic