×

The equational theory of pomsets. (English) Zbl 0669.68015

A labeled partial order is a partially ordered set together with a labeling of each element (by a symbol from some alphabet). A partially- ordered multiset, or pomset, is an isomorphism class of some labeled partial order.
Pomsets have been used as a model of concurrency and as an aid in understanding the semantics of parallel programs The author investigates the axiomatic properties of pomsets, sets of pomsets and ideals of pomsets. He shows, for example, that the equational theory of pomsets under the operations of concatenation, parallel composition and union is finitely axiomatizable. Similar results are obtained for ideals of pomsets.
Reviewer: G.Slutaki

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
06A06 Partial orders, general
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrahamson, K., Modal logic of concurrent nondeterministic programs, (Proc. Symp. on Semantics of Concurrent Computation. Proc. Symp. on Semantics of Concurrent Computation, Lecture Notes in Computer Science, 70 (1979), Springer: Springer Berlin), 21-33 · Zbl 0402.68010
[2] Araki, T.; Kagimasa, T.; Tokura, N., Relations of flow languages to Petri net languages, (Programming Languages Group Memo No. 79-01 (1979), Department of Information and Computer Sciences, Osaka University) · Zbl 0473.68075
[3] (Brauer, W., Net Theory and Applications. Net Theory and Applications, Lecture Notes in Computer Science, 84 (1980), Springer: Springer Berlin) · Zbl 0434.68040
[4] Brock, J. D.; Ackerman, W. B., Scenarios: a model of nondeterministic computation, (Diaz, J.; Ramos, I., Formalization of Programming Concepts. Formalization of Programming Concepts, Lecture Notes in Computer Science, 107 (1981), Springer: Springer Berlin), 252-259
[5] Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, J. ACM, 31, 3, 560-599 (1984) · Zbl 0628.68025
[6] Conway, J. H., Regular Algebra and Finite Machines (1971), Chapman & Hall: Chapman & Hall London · Zbl 0231.94041
[7] Gischer, J. L., Shuffle languages, Petri nets, and context-sensitive languages, Comm. ACM, 24, 9, 597-605 (1981) · Zbl 0471.68063
[8] Gischer, J. L., Partial orders and the axiomatic theory of shuffle, (Tech. Rept. No. STAN-CS-84-7033 (1984), Stanford University)
[9] Grabowski, J., On partial languages, Ann. Soc. Math. Polon. Ser. IV. Fund. Math., IV, 2, 427-498 (1981) · Zbl 0468.68088
[10] Greif, I., Semantics of communicating parallel processes, (Ph.D. Thesis (1975), Massachusetts Institute of Technology), (Project MAC TR-154) · Zbl 0362.68036
[11] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[12] Ito, T.; Ando, S., A complete axiom system of super-regular expressions, (Rosenfeld, J. L., Proc. IFIP 74 (1974), North-Holland: North-Holland Amsterdam), 661-665 · Zbl 0301.02033
[13] Ito, T., On behaviors of parallel processes with duration, (Proc. Conf. on Information Sciences and Systems (1985), Johns Hopkins University: Johns Hopkins University Baltimore)
[14] Jantzen, M., The power of synchronizing operations on strings, Theoret. Comput. Sci., 14, 2, 127-154 (1981) · Zbl 0477.68034
[15] Jantzen, M., Extending regular expressions with iterated shuffle, Theoret. Comput. Sci., 38, 223-247 (1985) · Zbl 0574.68069
[16] Kahn, G.; MacQueen, D. B., Coroutines and networks of parallel processes, (Gilchrist, B., Proc. IFIP 77 (1977), North-Holland: North-Holland Amsterdam), 993-998 · Zbl 0363.68076
[17] Kimura, T., An algebraic system for process structuring and interprocess communication, Proc. 8th Ann. Symp. on Theory of Computing, 92-100 (1976) · Zbl 0365.68066
[18] Lamport, L., Time, clocks, and the ordering of events in a distributed system, Comm. ACM, 21, 7, 558-564 (1978) · Zbl 0378.68027
[19] Lamport, L., The mutual exclusion problem: Part I—A theory of interprocess communication, J. ACM, 33, 2, 313-326 (1986) · Zbl 0627.68017
[20] Milner, R., A Calculus of Communicating Systems, (Lecture Notes in Computer Science, 92 (1980), Springer: Springer Berlin) · Zbl 0452.68027
[21] Milner, R., A complete inference system for a class of regular behaviours, J. Comput. System Sci., 28, 439-466 (1984) · Zbl 0562.68065
[22] Pratt, V. R., On the composition of processes, Proc. 9th Ann. Symp. on Principles of Programming Languages, 213-223 (1982)
[23] Pratt, V. R., Some constructions for order-theoretic models of concurrency, (Proc. Conf. on Logics of Programs. Proc. Conf. on Logics of Programs, Lecture Notes in Computer Science, 193 (1985), Springer: Springer Berlin), 267-283 · Zbl 0565.68014
[24] Pratt, V. R., Modelling concurrency with partial orders, Internat. J. Parallel Programming, 15, 33-71 (1987) · Zbl 0622.68034
[25] Redko, V. N., On defining relations for the algebra of regular events, Ukrain. Mat. Ž, 16, 120-126 (1964), in Russian. · Zbl 0199.04302
[26] Salomaa, A., Two complete axiom systems for the algebra of regular events, J. ACM, 13, 1, 158-169 (1966) · Zbl 0149.24902
[27] Shaw, A. C., Software description with flow expressions, IEEE Trans. Software Engineering, SE-4, 3, 242-254 (1978) · Zbl 0381.68035
[28] Slutzki, G., Descriptional complexity of concurrent processes, (Lecture Notes in Computer Science, 88 (1980), Springer: Springer Berlin), 601-611 · Zbl 0441.68019
[29] Valdes, J.; Tarjan, R. E.; Lawler, E. L., The recognition of series parallel digraphs, SIAM J. Comput., 11, 2, 298-313 (1981) · Zbl 0478.68065
[30] Winskel, G., Events in computation, (Ph.D. Thesis (1980), University of Edinburgh)
[31] Winskel, G., Categories of models for concurrency, (Lecture Notes in Computer Science, 197 (1985), Springer: Springer Berlin), 246-267 · Zbl 0567.68017
[32] Graham, R. L.; Knuth, D. L.; Motzkin, T. S., Complements and transitive closures, (Tech. Rept. No. STAN-CS-71-214 (1971), Stanford University) · Zbl 0309.04002
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.