WANG Chao, WU Jinzhao, TAN Hongyan. Revised Singleton Failures Equivalence for Labelled Transition Systems[J]. Chinese Journal of Electronics, 2015, 24(3): 498-501. doi: 10.1049/cje.2015.07.010
Citation: WANG Chao, WU Jinzhao, TAN Hongyan. Revised Singleton Failures Equivalence for Labelled Transition Systems[J]. Chinese Journal of Electronics, 2015, 24(3): 498-501. doi: 10.1049/cje.2015.07.010

Revised Singleton Failures Equivalence for Labelled Transition Systems

doi: 10.1049/cje.2015.07.010
Funds:  This work is supported by the National Natural Science Foundation of China (No.11371003, No.11461006), the Natural Science Foundation of Guangxi (No.2011GXNSFA018154, No.2012GXNSFGA060003), the Science and Technology Foundation of Guangxi (No.10169-1), the Scientific Research Project from Guangxi Education Department (No.201012MS274), and Open Research Fund Program of Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis (No.HCIC201301).
More Information
  • Corresponding author: WU Jinzhao (corresponding author) was born in 1965. He received his Ph.D. degree in science from Institute of Systems Science, Chinese Academy of Sciences. He is now a professor in College of Information Science and Engineering, Guangxi University for Nationalities. His research interests are in the fields of formal methods, symbolic computation, and automated reasoning. (Email: wujz2009@gmail.com)
  • Received Date: 2014-10-14
  • Rev Recd Date: 2015-01-29
  • Publish Date: 2015-07-10
  • Based on previous researches, the set of all traces and Singleton failures (SF) pairs is used to characterize SF equivalence. Since the trace information can not be obtained from the SF information, the set of all SF pairs alone can not characterize SF equivalence. We propose a Revised version of singleton failures (RSF) pair, show that the set of all RSF pairs alone can characterize SF equivalence, RSF equivalence and SF equivalence are equivalent, and discuss the difference between RSF and SF. The main conclusion of this paper is that RSF equivalence algorithm is the most efficient one among all SF equivalence algorithms. We present several examples showing RSF equivalence algorithm is computationally quite efficient.
  • loading
  • S.D. Brookes, C.A. Hoare and A.W. Roscoe, "A theory of communicating sequential processes", Journal of the ACM (JACM), Vol.31, No.3, pp.560-599, 1984.
    S. Dunne, "Termination without√ in CSP", FM 2011: Formal Methods, Springer, pp.278-292, 2011.
    R.J. van Glabbeek, U. Goltz and J. Schicke-Uffmann, "On characterising distributability", arXiv preprint arXiv:1309.3883, 2013.
    W. Chao, L. Yi, W. JinZhao and T. HongYan, "Approximate failures semantics for polynomial labelled transition systems", Journal of Donghua University (English Edition), Vol.6, pp. 472-476, 2013.
    W. Chao, W. JinZhao and T. HongYan, "Approximate trace and singleton failures equivalences for transition systems", Journal of Systems Engineering and Electronics, 2015.
    S. Reeves and D. Streader, "Data refinement and singleton failures refinement are not equivalent", Formal Aspects of Computing, Vol.20, No.3, pp.295-301, 2008.
    E.A. Boiten, "Introducing extra operations in refinement", Formal Aspects of Computing, Vol.26, No.2, pp.305-317, 2014.
    J. Derrick and E. Boiten, "Relational concurrent refinement part III: Traces, partial relations and automata", Formal Aspects of Computing, Vol.26, No.2, pp.407-432, 2014.
    F.S. de Boer, J.N. Kok, C. Palamidessi and J.J. Rutten, "The failure of failures in a paradigm for asynchronous communication", CONCUR'91, Springer, pp.111-126, 1991.
    C. Bolton and J. Davies, "A singleton failures semantics for communicating sequential processes", Formal Aspects of Computing, Vol.18, No.2, pp.181-210, 2006.
    R.J. Van Glabbeek, "The linear time-branching time spectrum i-the semantics of concrete, sequential processes", Handbook of Process Algebra, Chapter 1, Citeseer, 2001.
    Formal Systems Europe. Ltd, "Failures-divergence refinement, FDR2 user manual", available at http://www.fsel.com/documentation/ fdr2, 2010.
    T. Gibson-Robinson, P. Armstrong, A. Boulgakov and A.W. Roscoe, "FDR3A modern refinement checker for CSP", Tools and Algorithms for the Construction and Analysis of Systems, Springer, pp.187-201, 2014.
    M. Butler and M. Leuschel, "Combining CSP and B for specification and property verification", FM 2005: Formal Methods, Springer, pp.221-236, 2005.
    V. Korolev, A. Joshi, V. Korolev, et al., "PROB: A tool for tracking provenance and reproducibility of big data experiments", Reproduce'14. HPCA 2014, Vol.11, pp.264-286, 2014.
    R. Milner, "Communication and concurrency", Prentice Hall New York etc., 1989.
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (200) PDF downloads(703) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return