微信服务号

微信订阅号

2025-4-5- 11
Home > Archive>Volume 29, Issue 6, 2018 >1635-1646. DOI:10.13328/j.cnki.jos.005459
PDF HTML XML Export Cite reminder
Tool for Checking Satisfiability of APTL Formulas
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61732013, 61420106004)

  • Article
    • | |
  • Metrics
    • |
  • Reference [11]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Alternating projection temporal logic (APTL) has a concise syntax with strong expressive power. It is able to express not only properties specified in classical temporal logic LTL, but also interval related sequential and periodical properties, as well as game related properties of open systems and multi-agent systems. To verify whether a system satisfies an APTL formula, the satisfiability of the APTL formula should be checked. In this paper, based on the method for checking satisfiability of an arbitrary APTL formula provided, a supporting tool APTL2BCG has been developed. The details of implementation are given as follows. Firstly, LNFG of P is constructed according to the normal form of the formula P. Then, the LNFG is transformed to a generalized alternating Büchi automaton over concurrent game structure (GBCG). Finally, the alternating Büchi automaton is developed over concurrent game structure (BCG) from the obtained GBCG, and the BCG is simplified for checking the satisfiability of the formula P.

    Reference
    [1] Tian C, Duan ZH. Alternating interval based temporal logics. In:Proc. of the ICFEM. 2010. 694-709.[doi:10.1007/978-3-642-16901-4_45]
    [2] Duan ZH. Temporal Logic and Temporal Logic Programming. Beijing:Science Press, 2005.
    [3] Wang HY, Duan ZH, Tian C. Symbolic model checking for alternating projection temporal logic. In:Proc. of the COCOA. 2015. 481-495.[doi:10.1007/978-3-319-26626-8_35]
    [4] Duan ZH, Tian C, Zhang L. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica, 2008,45(1):43-78.[doi:10.1007/s00236-007-0062-z]
    [5] Baier C, Katoen JP. Principles of Model Checking. Cambridge:MIT Press, 2008.
    [6] Duan ZH, Tian C. A practical decision procedure for propositional projection temporal logic with infinite models. Theoretical Computer Science, 2014,554:169-190.[doi:10.1016/j.tcs.2014.02.011]
    [7] Alur R, Henzinger TA, Kupferman O. Alternating-Time temporal logic. JACM, 2002,49:672-713.[doi:10.1145/585265.585270]
    [8] Schewe S, Finkbeiner B. Satisfiability and finite model property for the alternating-time Mu-calculus. In:Proc. of the CSL. 2006. 591-605.[doi:10.1007/11874683_39]
    [9] http://www.cmi.ac.in/~kumar/words/lecture06.pdf
    [10] Manna Z, Sipma H. Alternating the Temporal Picture for Safety. In:Proc. of the ICALP. 2000. 429-450.[doi:10.1007/3-540-45022-X_37]
    [11] Gastin P, Oddoux D. Fast LTL to Buchi Automata Translation. In:Proc. of the CAV. 2001. 53-65.[doi:10.1007/3-540-44585-4_6]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

王海洋,段振华,田聪. APTL公式的可满足性检查工具.软件学报,2018,29(6):1635-1646

Copy
Share
Article Metrics
  • Abstract:3651
  • PDF: 5679
  • HTML: 2855
  • Cited by: 0
History
  • Received:June 26,2017
  • Revised:September 01,2017
  • Adopted:November 06,2017
  • Online: December 28,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033159Visitors
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