微信服务号

微信订阅号

2025-4-9- 12
Home > Archive>Volume 20, Issue 8, 2009 >2026-2036
PDF HTML XML Export Cite reminder
Compositional Reasoning in Intuitionistic Linear-Time ?-Calculus
Author:
Affiliation:

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

    This paper discusses the use of intuitionistic linear-time μ-calculus (IμTL) whose underlying model is based on Heyting algebra of prefixed closed sets as the basis for the specification of assumption and guarantee paradigm, and then propose an assumption-guarantee rule in IμTL. The rule formulated is more general then previously proposed rules that used linear-time temporal logic (LTL) in the specification of assumption and guarantee paradigm and extends the discussion for safety properties of the form “always φ”, and therefore represents more uniform reasoning of assumption and guarantee specifications for also supporting circular compositional reasoning.

    Reference
    [1] Alur R, Henzinger TA. Reactive modules. Formal Methods in System Design, 1999,(15):7?48.
    [2] Clark EM, Filorn T, Jha S. Exploting symmetry in temporal logic model checking. In: Proc. of the CAV’93. Number 697. 1993.
    [3] Godefroid P, Wolper P. A partial approach to model checking. In: Proc. of the 6th Annual Symp. on Logic in Computer Science. Amsterdam: IEEE Computer Society Press, 1991. 406?416.
    [4] Grumberg O, Long DE. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 1994, 16(3):843?871.
    [5] McMillan KL, Dill D, Burch JR, Clark EM, Hwang LJ. Symbolic model checking 1020 states and beyond. In: Proc. of the 5th Annula Symp. on Logic in Computer Science. Philadeliphia: IEEE Computer Society Press, 1990. 428?429.
    [6] Jonson B, Tsay YK. Assumption/Guarantee specifications in linear-time temporal logic. Theoretical Computer Science, 1996, (167):47?72.
    [7] Abadi M, Lamport L. Conjoining specifications. Technical Report 118, SRC DEC, 1993.
    [8] Abadi M, Plotkin GD. A logical view of composition. Theoretical Computer Science, 1993,114(1):3?30.
    [9] Manna Z, Pnueli A. A hierarchy of temporal properties. In: Proc. of the Principles of Distributed Computing, the 9th Annual ACM Symp. PODC’90. Quebec, 1990. 337?410.
    [10] McMillan KL. Verification of an implementation of tomasulo’s algorithm by compositional model checking. In: Hu AJ, Vardi M, eds. Proc. of the Conf. on Computer-Aided Verification (CAV’s’98). LNCS 1427, Springer-Verlag, 1998. 100?121.
    [11] Misra J, Chandy KM. Proofs of networks of processes. IEEE Trans. on Software Engineering, 1981,7(4):417?426.
    [12] Alur R, Henzinger TA, Mang FYC, Qadeer S, Rajamani AK, Tariran S. Mocha: Modularity in model checking. In: Hu AJ, Vardi M, eds. Proc. of the Conf. on Computer-adid Verification (CAV’s’98). LNCS 1427, Springer-Verlag, 1998. 521?525.
    [13] Kazmi SAR, Zhang WH. Intuitionistic linear-time μ-calculus. Journal of Software, 2008,19(12):3122?3133 (in English with Chinese abstract). http://www.jos.org.cn/1000-9825/19/3122.htm
    [14] Rajamani SK, Henzinger TA, Dadeer S, Tasiran S. An assume-guarantee rule for checking simulation. ACM Trans. on Programming Languages and Systems, 2002,24(1):51?64.
    [15] Valmari A. A stubborn attack on state explosion. In: Proc. of the CAV’90. 1990. 156?165.
    [16] Viswanathan M, Viswanathan R. Foundations for circular compositional reasoning. In: Jos JP, Baeten CM, Lenstra JK, Woeginger GJ, eds. Proc. of the 28th Int’l Colloqium on Automata, Languages and Programming (ICALP 2001). LNCS 2719, Springer-Verlag, 2001. 835?847.
    [17] Bochmann GV. Submodule construction for specifications with input assumptions and output guarantees. In: Proc. of the 22nd IFIP WG 6.1 Int’l Conf. Houston on Formal Techniques for Networked and Distributed Systems. LNCS 2529, London: Springer-Verlag, 2002. 17?33.
    [18] Nam W, Alur R. Learning-Based assume-guarantee reasoning with automatic decomposition. In: Graf S, Zhang WH, eds. Proc. of the ATVA 2006. 2006. 17?170.
    [19] Bobaru MG, Pasareanu CS, Giannakopoulou D. Automated assumption-guarantee reasoning by abstraction refinement. In: Proc. of the CAV 2008. Berlin: Springer-Verlag, 2008. 135?148.
    [20] Hayes IJ, Jackson MA, Jones CB. Determining the specification of a control system from that of its environment. In: Proc. of the FME 2003. 2003. 154?169.
    [21] Larsen KG, Nyman U, Wasowski A. Interface input/output automata. In: Proc. of the FM 2006. 2006. 82?97.
    [22] Giannakopoulou D, Pasareanu CS, Cobleigh JM. Assume-Guarantee verification of source code with design-level ssumptions. In: Proc. of the ICSE 2004. 2004. 211?220.
    [23] Wang BY. Automatic derivation of compositional rules in automated compositional reasoning. In: Proc. of the CONCUR 2007. LNCS 4703, Berlin: Springer-Verlag, 2007. 303?316.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

KAZMISyedAsadRaza,张文辉.直觉线性μ-演算中的合成推理.软件学报,2009,20(8):2026-2036

Copy
Share
Article Metrics
  • Abstract:4658
  • PDF: 5895
  • HTML: 0
  • Cited by: 0
History
  • Received:June 03,2008
  • Revised:August 07,2008
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034077Visitors
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