APTL Model Checker for Verifying Multi-agent Systems
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61732013, 61420106004)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    The model checking tool based on Alternating Projection Temporal Logic (APTL) is designed and implemented to improve the ability of expressing for linear temporal logic in this study. The supporting tool MCMAS_APTL is developed inspired by the method for symbolic model checking of APTL provided by Wang et al. The tool MCMAS_APTL could be used for verifying the properties of Multi-agent Systems (MASs) effectively. The detailed procedures of checking whether a MAS satisfies a property by MCMAS_APTL are given as follows. Firstly, describing the system IS with the Interpreted System Programming Language (ISPL) and specifying the property of the system by an APTL formula P. Then, symbolically representing the system IS and transforming the negation of P into normal form. Finally, calculating the set of states from which there is at least one existing path satisfying the negation of P. If the obtained state set contains an initial state, then the system does not satisfy the formula P; otherwise, the system satisfies the formula P. The details of implementing MCMAS_APTL are provided in this paper, and a robotic soccer game is presented to show how the model checker MCMAS_APTL works in practice.

    Reference
    Related
    Cited by
Get Citation

王海洋,段振华,田聪.用于验证多智能体系统的APTL模型检测器.软件学报,2019,30(2):231-243

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:November 17,2017
  • Revised:March 24,2018
  • Adopted:
  • Online: May 02,2018
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063