Two-thirds simulation indexes and modal logic characterization
Yanfang MA, Min ZHANG, Yixiang CHEN, Liang CHEN
Two-thirds simulation indexes and modal logic characterization
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.
simulation / metric / two-thirds simulation / process calculus
[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
|
/
〈 | 〉 |