Semantics and applications of process and program algebra

作者: T.D. Vu

DOI:

关键词: Infimum and supremumComputer scienceThread (computing)Program algebraMonotonic functionTheoretical computer scienceDiscrete mathematicsMonotone polygonServerApproximations of πAbstraction operator

摘要: ion in BTA Abstraction [73, 20, 8] plays an important role process algebras. It allows a simpler view of thread, ignoring internal details. In [17] abstraction is used to emulate the interaction between clients and servers, assuming that servers are threads BTA. We assume existence concrete action tau ∈ Σ does not have any side effects always replies true after its execution. This can be abstracted away by operator called defined as follows. Definition 5.20 Let τtau : BTAΣ → τtau(S) = S, τtau(D) D, τtau(P Q) ), ) τtau(Q) (a 6= Σ). 5.3. complete ultra-metric space 59 shown monotone, i.e.: Lemma 5.21 For all P,Q BTAΣ, P ⊑ Q ⇒ τtau(Q). suggests definition infinite thread given supremum monotone sequence below. 5.22 (Pn)n finite approximations . Then ⊔

参考文章(86)
Roland Bol, Jan Friso Groote, The meaning of negative premises in transition system specifications Journal of the ACM. ,vol. 43, pp. 863- 914 ,(1996) , 10.1145/234752.234756
J.A. Bergstra, J.W. Klop, Process algebra for synchronous communication Information & Computation. ,vol. 60, pp. 109- 137 ,(1984) , 10.1016/S0019-9958(84)80025-X
Christel Baier, Mila Majster-Cederbaum, The connection between initial and unique solutions of domain equations in the partial order and metric approach Formal Aspects of Computing. ,vol. 9, pp. 425- 445 ,(1997) , 10.1007/BF01211300
J.A. Bergstra, I. Bethke, Polarized process algebra with reactive composition formal methods. ,vol. 343, pp. 285- 304 ,(2005) , 10.1016/J.TCS.2005.06.014
Matthew Hennessy, Robin Milner, Algebraic laws for nondeterminism and concurrency Journal of the ACM. ,vol. 32, pp. 137- 161 ,(1985) , 10.1145/2455.2460
Rob J. van Glabbeek, W. Peter Weijland, Branching time and abstraction in bisimulation semantics Journal of the ACM. ,vol. 43, pp. 555- 600 ,(1996) , 10.1145/233551.233556
M.C. Browne, E.M. Clarke, O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic Theoretical Computer Science. ,vol. 59, pp. 115- 131 ,(1988) , 10.1016/0304-3975(88)90098-9
J. Heering, P. R. H. Hendriks, P. Klint, J. Rekers, The syntax definition formalism SDF—reference manual— Sigplan Notices. ,vol. 24, pp. 43- 75 ,(1989) , 10.1145/71605.71607
Brenda S. Baker, S. Rao Kosaraju, A Comparison of Multilevel break and next Statements Journal of the ACM. ,vol. 26, pp. 555- 566 ,(1979) , 10.1145/322139.322151
Harlan D. Mills, The new math of computer programming Communications of The ACM. ,vol. 18, pp. 43- 48 ,(1975) , 10.1145/360569.360659