Protocol Analysis through Alternating-Time Temporal Logic and Timed Petri Net Models

Alternating-time Temporal Logic (ATL) is the natural specification language for the open system, which has a strategy to reach a certain state. But the semantics for ATL is not studied sufficiently. In this paper, we define Timed Petri Nets (TPN) , where time is associated with tokens, transitions, arcs and places. TPN is taken as the semantic description for ATL, the representation of time constraints is interpreted for ATL. We obtain a natural relationship between ATL and TPN. commonality, variability, binding time, structural relations are taken into account in this method. An illustrative example for verifying safety protocol is addressed based on timed Petri nets and ATL.