微信服务号

微信订阅号

2025-4-6- 10
Home > Archive>Volume 28, Issue 4, 2017 >898-906. DOI:10.13328/j.cnki.jos.005057
PDF HTML XML Export Cite reminder
NuTL2PFG: Checking Satisfiability of νTL Formulas
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61322202, 61133001, 61420106004, 91418201)

  • Article
    • | |
  • Metrics
    • |
  • Reference [25]
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    Linear time μ-calculus (νTL) is a formalism which has a strong expressive power with a succinct syntax. It is useful for specifying and verifying various properties of concurrent programs. However, the nesting of fix point operators makes its decision problem difficult to solve. To tackle the issue, a tool called NuTL2PFG for checking the satisfiability of νTL formulas is developed in this paper. Based on present future form (PF form) of νTL formulas, the tool is able to construct the present future form graph (PFG) for a given formula to specify the models that satisfy the formula. Further, the tool checks the satisfiability of a given formula by searching for a ν-path in its PFG free of infinite unfoldings of least fixpoints. Experimental results show that NuTL2PFG is more efficient than the existing tools.

    Reference
    [1] Barringer H, Kuiper R, Pnueli A. A really abstract concurrent model and its temporal logic. In:Proc. of the POPL'86. New York:ACM Press, 1986. 173-183.[doi:10.1145/512644.512660]
    [2] Kozen D. Results on the propositional μ-calculus. Theoretical Computer Science, 1983,27(3):333-354.[doi:10.1016/0304-3975(82) 90125-6]
    [3] Pnueli A. The temporal logic of programs. In:Proc. of the FOCS'77. New York:IEEE Computer Society, 1977. 46-57.[doi:10.1109/SFCS.1977.32]
    [4] Barringer H, Kuiper R, Pnueli A. Now you may compose temporal logic specifications. In:DeMillo RA, ed. Proc. of the STOC'84. New York:ACM Press, 1984. 51-63.[doi:10.1145/800057.808665]
    [5] Emerson EA, Clarke EM. Characterizing correctness properties of parallel programs using fixpoints. In:de Bakker JW, van Leeuwen J, eds. Proc. of the ICALP'80. LNCS 85, Heidelberg:Springer-Verlag, 1980. 169-181.[doi:10.1007/3-540-10003-2_69]
    [6] Vardi MY. A temporal fixpoint calculus. In:Ferrante J, Mager P, eds. Proc. of the POPL'88. New York:ACM Press, 1988. 250-259.[doi:10.1145/73560.73582]
    [7] Sistla AP, Clarke EM. The complexity of propositional linear temporal logics. Journal of the Association for Computing Machinery, 1985,32(3):733-749.[doi:10.1145/3828.3837]
    [8] Streett RS, Emerson EA. An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation, 1989,81(3):249-264.[doi:10.1016/0890-5401(89)90031-X]
    [9] Stirling C, Walker D. CCS, liveness, and local model checking in the linear time mu-calculus. In:Sifakis J, ed. Proc. of the AVMFSS'89. LNCS 407, Heidelberg:Springer-Verlag, 1990. 166-178.[doi:10.1007/3-540-52148-8_14]
    [10] Kaivola R. A simple decision method for the linear time mu-calculus. In:Desel J Dr. rer. nat, ed. Proc. of the STRICT'95. London:Springer-Verlag, 1995. 190-204.[doi:10.1007/978-1-4471-3078-9_13]
    [11] Bradfield J, Esparza J, Mader A. An effective tableau system for the linear time mu-calculus. In:Meyer F, Monien B, eds. Proc. of the ICALP'96. LNCS 1099, Heidelberg:Springer-Verlag, 1996. 98-109.[doi:10.1007/3-540-61440-0_120]
    [12] Banieqbal B, Barringer H. Temporal logic with fixed points. In:Banieqbal B, Barringer H, Pnueli A, eds. Proc. of the Temporal Logic in Specification'87. LNCS 398, Heidelberg:Springer-Verlag, 1989. 62-74.[doi:10.1007/3-540-51803-7_22]
    [13] Dax C, Hofmann M, Lange M. A proof system for the linear time mu-calculus. In:Arun-Kumar S, Garg N, eds. Proc. of the FSTTCS 2006. LNCS 4337, Heidelberg:Springer-Verlag, 2006. 274-285.[doi:10.1007/11944836_26]
    [14] Liu Y, Duan ZH, Tian C, Liu B. Present-Future form of linear time mu-calculus. In:Liu SY, Duan ZH, eds. Proc. of the SOFL+ MSVL 2013. LNCS 8332, Switzerland:Springer Int'l Publishing, 2014. 76-85.[doi:10.1007/978-3-319-04915-1_6]
    [15] Liu Y, Duan ZH, Tian C. An improved decision procedure for linear time mu-calculus. arXiv preprint arXiv:1507.05513, 2015.
    [16] Duan ZH. An extended interval temporal logic and a framing technique for temporal logic programming[Ph.D. Thesis]. Newcastle upon Tyne:University of Newcastle upon Tyne, 1996.
    [17] Duan ZH. Temporal Logic and Temporal Logic Programming. Beijing:Science Press, 2005.
    [18] Duan ZH, Tian C. Decidability of propositional projection temporal logic with infinite models. In:Cai JY, Cooper SB, Zhu H, eds. Proc. of the TAMC 2007. LNCS 4484, Heidelberg:Springer-Verlag, 2007. 521-532.[doi:10.1007/978-3-540-72504-6_47]
    [19] Duan ZH, Tian C. An improved decision procedure for propositional projection temporal logic. In:Dong JS, Zhu HB, eds. Proc. of the ICFEM 2010. LNCS 6447, Heidelberg:Springer-Verlag, 2010. 90-105.[doi:10.1007/978-3-642-16901-4_8]
    [20] 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]
    [21] Stirling C. Modal and temporal logics. Technical Report, ECS-LFCS-91-157, University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science, 1991.
    [22] Walukiewicz I. Completeness of Kozen's axiomatisation of the propositional μ-calculus. Information and Computation, 2000, 157(1):142-182.[doi:10.1006/inco.1999.2836]
    [23] Bruse F, Friedmann O, Lange M. On guarded transformation in the modal μ-calculus. Logic Journal of the IGPL, 2015,23(2):194-216.[doi:10.1093/jigpal/jzu030]
    [24] Fischer MJ, Ladner RE. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 1979,18(2):194-211.[doi:10.1016/0022-0000(79)90046-1]
    [25] Tarjan R. Depth-First search and linear graph algorithms. SIAM Journal on Computing, 1972,1(2):146-160.[doi:10.1137/0201010]
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

刘尧,段振华,田聪. NuTL2PFG:νTL公式的可满足性检查.软件学报,2017,28(4):898-906

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:December 25,2015
  • Revised:February 24,2016
  • Online: May 05,2016
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033332Visitors
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