First

a unified ATN formal framework was presented

into which typical negotiation strategies could be reduced.Second

the formal verification of ATN was defined based on the formal framework.The objectives and procedures of the formal verification of ATN were described.Third

several typical negotiation strategies were discussed

and the computational complexity of the corresponding verification problems was shown

several conclusions had been obtained.Last

the formal verification of ATN was implemented by using logic programming and model checking methods.The experimental results show that the number of rules is a crucial factor in determining the runtime.Both logic programming and model checking are efficient when the number of transition rules is small

and logic programming does not scale as well as model checking.