Two-thirds simulation indexes and modal logic characterization

Yanfang MA, Min ZHANG, Yixiang CHEN, Liang CHEN

PDF(290 KB)
PDF(290 KB)
Front. Comput. Sci. ›› DOI: 10.1007/s11704-011-0140-9
RESEARCH ARTICLE

Two-thirds simulation indexes and modal logic characterization

Author information +
History +

Abstract

Two-thirds simulation provides a kind of abstract description of an implementation with respect to a specification. In order to characterize the approximate two-thirds simulation, we propose the definition of a two-thirds simulation index which expresses the degree to which a binary relation between processes is two-thirds simulation. λ–two-thirds simulation and its substitutivity laws are given in this paper. And, based on λ–two-thirds simulation, we present a measure model for describing the degree of approximation between processes. In particular, we give the modal logical characterization of λ–two-thirds simulation.

Keywords

simulation / metric / two-thirds simulation / process calculus

Cite this article

Download citation ▾
Yanfang MA, Min ZHANG, Yixiang CHEN, Liang CHEN. Two-thirds simulation indexes and modal logic characterization. Front Comput Sci Chin, https://doi.org/10.1007/s11704-011-0140-9

References

[1]
Hoare C A R. Communication Sequential Processes. Englewood Cliffs: Prentice Hall, 1985
[2]
Brookes S D, Hoare C A R, Roscoe A W. A theory of communicating sequential processes. Journal of the ACM, 1984, 31(3): 560–599
CrossRef Google scholar
[3]
Olderog E R, Hoare C A R. Specification-oriented semantics for communicating processes. Acta Informatica, 1986, 23(1): 9–66
CrossRef Google scholar
[4]
Park D. Concurrency and automata on infinite sequences. In: Proceedings of 5th GI-Conference on Theoretical Computer Science. 1981, 167–183
[5]
Bloom B, Istrail S, Meyer A R. Bisimulation can’t be traced. Journal of the ACM, 1995, 42(1): 232–268
CrossRef Google scholar
[6]
Milner R. A calculus of communicating systems. Lecture Notes in Computer Science, 1980, 92: 260–278
[7]
Larsen K G, Skou A. Bisimulation through probabilistic testing. Journal of Information and Computation, 1991, 94(1): 1–28
CrossRef Google scholar
[8]
Glabbeek R J. The linear time-branching time spectrum i-the semantics of concrete, sequential processes.http://theory.stanford.edu/rvg
[9]
He J F, Hoare T. Equating bisimulation with refinement. Technical report, UNU-IIST, Macau, 2003
[10]
Ying M S, Wirshing M. Approximate bisimilarity and its application. Technical report, Institutfur Informatik, Ludwig-Maximilians-Universitat Munchen,1999
[11]
Ying M S. Bisimulation indexes and their applications. Theoretical Computer Science, 2002, 275(1-2): 1–68
CrossRef Google scholar
[12]
Ying M S. Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrency Programs.New York: Springer-Verlag, 2001
[13]
Milner R. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences, 1984, 28(3): 439–466
CrossRef Google scholar
[14]
Hennessy M, Milner R. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 1985, 32(1): 137–161
CrossRef Google scholar
[15]
Milner R. Communication and Concurrency.New York: Prentice Hall,1989
[16]
Minler R. Communicating and Mobile Systems: the π-calculus. Cambridge: Cambridge University Press, 1999
[17]
Plotkin G D. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981
[18]
Engelking R. General Topology. Warszawa: Polish Scientific Publisher, 1977
[19]
Giacalone A, Jou C C, Smolka S A. Algebraic reasoning for probabilistic concurrent systems. In: ProceedingWorking Conference on Programming Concepts and Methods. 1990, 443–458
[20]
Giacalone A, Jou C C, Smolka S A. Probabilistic in processes: an algebraic/operational framework. Technical report, Department of Computer Science, SUNY at Stony Brook, 1988
[21]
Song L, Deng Y X, Cai X. Towards automatic measurement of probabilistic processes. In: Proceedings of the 7th International Conference on Quality Software. 2007, 50–59
[22]
Deng Y X, Chothia T, Palamidessi C, Pang J. Metrics for action-labelled quantitative transition systems. In: Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages. 2005, 79–96
[23]
Alves de Medeiros A.K, van der Aalst W M P, Wejiters A J M M. Quantifying process equivalence based on observed behavior. Data & Knowledge Engineering, 2008, 64(1): 55–74
CrossRef Google scholar
[24]
Zhang J J, Zhu Z H. A modal characterization of λ-bisimilarity. International Journal of Software Informatics, 2007, 1(1): 85–99

Acknowledgements

The work was supported by the Natural Science Foundation of China (Grant No. 61021004), the Fundamental Research Funds for the Central Universities (78210045), the Open Fund of Shanghai Key Laboratory of Trustworthy Computing, the Key Research Foundation of Higher Education of Anhui Province (KJ2011A248). The author would like to express their thanks to Prof. Larsen for his suggestions. The author also would like to thank the referees for their invaluable comments and suggestions about the modal logical characterization on the general metric.

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg
AI Summary AI Mindmap
PDF(290 KB)

Accesses

Citations

Detail

Sections
Recommended

/