Model Checking Research of Multi-valued Alternating-time Temporal Logic
In order to formally verify open systems containing multi-valued information,a multi-valued al-ternating-time temporal logic was proposed based on multi-valued logic,and the model checking problem of this logic was explored. Firstly,a multi-valued concurrent game structure was introduced as a model for such open systems. The key feature of the model was that it could model open systems with multi-val-ued information. Secondly,the syntax and semantics of multi-valued alternating-time temporal logic based on this model were provided,which could describe properties with multi-valued information to be verified. Finally,a model checking algorithm for multi-valued alternating-time temporal logic was pro-posed based on fixed-point theory,and the time complexity of the algorithm was analyzed. The analysis results indicated that model checking for multi-valued alternating-time temporal logic could be completed in polynomial time.
model checkingmulti-valued logicalternating-time temporal logicconcurrent game structure
万方数据
维普
