Revised Singleton Failures Equivalence for Labelled Transition Systems

WANG Chao; WU Jinzhao; TAN Hongyan

doi:10.1049/cje.2015.07.010

Volume 24 Issue 3

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2015 > 24(3): 498-501

WANG Chao, WU Jinzhao, TAN Hongyan, “Revised Singleton Failures Equivalence for Labelled Transition Systems,” Chinese Journal of Electronics, vol. 24, no. 3, pp. 498-501, 2015, doi: 10.1049/cje.2015.07.010

Citation:

WANG Chao, WU Jinzhao, TAN Hongyan, “Revised Singleton Failures Equivalence for Labelled Transition Systems,” Chinese Journal of Electronics, vol. 24, no. 3, pp. 498-501, 2015, doi: 10.1049/cje.2015.07.010

Citation:

PDF( 222 KB)

Revised Singleton Failures Equivalence for Labelled Transition Systems

doi: 10.1049/cje.2015.07.010

1.
School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China;
2.
Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning 530006, China;
3.
Institute of Acoustics, Chinese Academy of Sciences, Beijing 100190, China

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

Abstract

Abstract

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.
- Singleton failures,
- Equivalence,
- Labelled Transition systems

FullText(HTML)

References(16)

References

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.

Relative Articles

Supplements(0)

Cited By

Proportional views