Two-thirds simulation indexes and modal logic characterization
Two-thirds simulation indexes and modal logic characterization
Yanfang MA1(), Min ZHANG2, Yixiang CHEN2, Liang CHEN3
1. School of Computer Science and Technology, Huaibei Normal University, Huaibei 235000, China; 2. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China; 3. School of Mathematical Sciences, Huaibei Normal University, Huaibei 235000, China
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.
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 doi: 10.1145/828.833
3
Olderog E R, Hoare C A R. Specification-oriented semantics for communicating processes. Acta Informatica , 1986, 23(1): 9–66 doi: 10.1007/BF00268075
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 doi: 10.1145/200836.200876
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 doi: 10.1016/0890-5401(91)90030-6
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 doi: 10.1016/S0304-3975(01)00124-4
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 doi: 10.1016/0022-0000(84)90023-0
14
Hennessy M, Milner R. Algebraic laws for nondeterminism and concurrency. Journal of the ACM , 1985, 32(1): 137–161 doi: 10.1145/2455.2460
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 doi: 10.1016/j.datak.2007.06.010
24
Zhang J J, Zhu Z H. A modal characterization of λ-bisimilarity. International Journal of Software Informatics , 2007, 1(1): 85–99
