×

Denotational semantics for thread algebra. (English) Zbl 1131.68069

Summary: This paper gives a denotational semantics for thread algebra (TA), an algebraic framework for the description and analysis of recent programming languages such as C# and Java [J. A. Bergstra and C. A. Middelburg, “Thread algebra for strategic interleaving”, Formal Asp. Comput. 19, 445–474 (2007; Zbl 1131.68067)]. We illustrate the technique taken from the metric topology of de Bakker and Zucker [J. W. de Bakker and J. I. Zucker, “Processes and the denotational semantics of concurrency”, Inf. Control 54, 70–120 (1982; Zbl 0508.68011)] to turn the domains of TA into complete metric spaces. We show that the complete metric space consisting of projective sequences is an appropriate domain for TA. By using Banach’s fixed-point theorem, we prove that the specification of a regular thread determines a unique solution. We also give a structural operational semantics for thread algebra and its relation to our denotational semantics. Finally, we present a particular interleaving strategy for TA that deals with abstraction in a natural way.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N15 Theory of programming languages
68Q55 Semantics in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aceto, L.; Fokkink, W. J.; Verhoef, C., Structural operational semantics, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier), 197-222 · Zbl 1062.68074
[2] Baeten, J. C.M.; Weijland, W. P., Process Algebra. Cambridge Tracts in Theoretical Computer Science, vol. 18 (1990), Cambridge University Press · Zbl 0716.68002
[3] Baier, C.; Majster-Cederbaum, M., The connection between initial and unique solutions of domain equations in the partial order and metric approach, Formal Aspects Comput., 9, 425-445 (1997) · Zbl 0889.68098
[4] Bakker, J. W.; Zucker, J. I., Processes and the denotational semantics of concurrency, Inform. and Control, 54, 1/2, 70-120 (1982) · Zbl 0508.68011
[5] Bergstra, J. A.; Bethke, I., Polarized process algebra and program equivalence, (Baeten, Jos C. M.; Jan Karel, Lenstra; Parrow, Joachim; Woeginger, Gerhard J., ICALP. ICALP, Lecture Notes in Computer Science, vol. 2719 (2003), Springer), 1-21 · Zbl 1039.68040
[6] Bergstra, J. A.; Bethke, I., Polarized process algebra with reactive composition, Theoretical Computer Science, 343, 3, 285-304 (2005) · Zbl 1077.68057
[7] Bergstra, J. A.; Klop, J. W., Process algebra for synchronous communication, Inform. and Control, 60, 1-3, 109-137 (1984) · Zbl 0597.68027
[8] Bergstra, J. A.; Loots, M. E., Program algebra for sequential code, J. Log. Algebr. Program., 51, 125-156 (2002) · Zbl 1008.68079
[9] J.A. Bergstra, C.A. Middelburg, Thread algebra with multi-level strategic interleaving. in: S.B. Cooper, B.Loewe, L. Torenvliet (Eds.), CiE, LNCS, vol. 3526, 2005, pp. 35-48. Journal version to appear in Theory of Computing Systems. Preliminary version: Computing Science Report 200441: Department of Mathematics and Computing Science, Eindhoven University of Technology.; J.A. Bergstra, C.A. Middelburg, Thread algebra with multi-level strategic interleaving. in: S.B. Cooper, B.Loewe, L. Torenvliet (Eds.), CiE, LNCS, vol. 3526, 2005, pp. 35-48. Journal version to appear in Theory of Computing Systems. Preliminary version: Computing Science Report 200441: Department of Mathematics and Computing Science, Eindhoven University of Technology. · Zbl 1113.68426
[10] J.A. Bergstra, C.A. Middelburg, Thread algebra for strategic interleaving Formal Aspects Comput., in press. Preliminary version: Computing Science Report PGR0404: Sectie Software Engineering, University of Amsterdam.; J.A. Bergstra, C.A. Middelburg, Thread algebra for strategic interleaving Formal Aspects Comput., in press. Preliminary version: Computing Science Report PGR0404: Sectie Software Engineering, University of Amsterdam.
[11] Bethke, I.; Ponse, A., Programma-algebra, een inleiding tot de programmatuur (2003), Amsterdam University Press: Amsterdam University Press Vossiuspers, (in Dutch)
[12] Engelking, R., General Topology (1977), Polish Scientific Publishers
[13] Kirk, W. A.; Sims, B., Handbook of Metric Fixed Point Theory (2001), Kluwer Academic: Kluwer Academic London · Zbl 0970.54001
[14] Milner, R., A Calculus of Communicating System, LNCS, vol. 92 (1980), Springer-Verlag: Springer-Verlag Berlin
[15] D.M.R. Park, Concurrency and automata on infinite sequences, in: P. Deussen (Ed.), Proceedings 5th GI Conference, LNCS, vol. 104, 1982, pp. 167-183.; D.M.R. Park, Concurrency and automata on infinite sequences, in: P. Deussen (Ed.), Proceedings 5th GI Conference, LNCS, vol. 104, 1982, pp. 167-183.
[16] G. Plotkin, A structural approach to operational semantics, Aarhus DAIMI FN-19, Computing Science Department, 1981.; G. Plotkin, A structural approach to operational semantics, Aarhus DAIMI FN-19, Computing Science Department, 1981.
[17] Stoltenberg-Hansen, V.; Lindstrom, I.; Griffor, E. R., Mathematical Theory of Domains. Mathematical Theory of Domains, Cambridge Tracts in Theoretical Computer Science, vol. 22 (1994), Cambridge University Press · Zbl 0828.06001
[18] T.D. Vu, Semantics and applications of process and program algebra, Ph.D. thesis, University of Amsterdam, 2007.; T.D. Vu, Semantics and applications of process and program algebra, Ph.D. thesis, University of Amsterdam, 2007.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.