×
Mazurkiewicz, Antoni; Ochmański, Edward; Penczek, Wojciech

Concurrent systems and inevitability. (English) Zbl 0675.68015

Theor. Comput. Sci. 64, No. 3, 281-304 (1989).
A concurrent system is a poset \(S=(S,\leq)\), where S is the set of states of the system (histories of its activity) and \(\leq\) is the dominating relation between states. A process is any maximal directed subposet of S, the family of all processes in S is called the behaviour of S. Processes correspond to full executions, namely they display concurrency fairness. In order to speak of eventual properties of processes the authors define the concept of observation of processes. If P \(\subseteq\) S is a process, a line (i.e. a maximal linearly ordered subposet of S) V is an observation if \(\downarrow V=P\) with \(\downarrow V=\cup (\downarrow \sigma |\) \(\sigma\in V)\), where \(\downarrow \sigma =\{\tau \in S|\) \(\tau\leq \sigma \}\). This is a case for processes in terminating and strongly synchronized systems, which, therefore, are observable. In this framework, the authors introduce the notion of inevitability. A property is inevitable if an observer of the system will notice, soon or later, a state with this property. The authors discuss conditions on processes and observers and their relationship with inevitability. One of these conditions characterizes inevitability in the interesting case of diamond discrete systems.
Reviewer: A.Maggiolo-Schettini

Cited in 11 Documents

MSC:

68N25 Theory of operating systems
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q55 Semantics in the theory of computing

Keywords:

concurrent processes; partial order semantics; inevitability; observers
PDF BibTeX XML Cite
\textit{A. Mazurkiewicz} et al., Theor. Comput. Sci. 64, No. 3, 281--304 (1989; Zbl 0675.68015)
Full Text: DOI

References:

[1] Alpern, B.; Schneider, F. B., Defining liveness, Inform. Process. Lett., 21, 181-185 (1985) · Zbl 0575.68030
[2] Best, E., Fairness and conspiracies, Inform. Process. Lett., 18, 215-220 (1984) · Zbl 0558.68052
[3] Goltz, U.; Reisig, W., The non-sequential behaviour of Petri nets, Inform. Contr., 57, 2/3, 125-147 (1983) · Zbl 0551.68050
[4] Kuratowski, K., Une méthode d’élimination des nombres transfinis des raisonnements mathématiques, Fund. Math., 3, 76-108 (1922) · JFM 48.0205.04
[5] Kuratowski, K.; Mostowski, A., Set Theory (1967), North-Holland: North-Holland Amsterdam · Zbl 0165.01701
[6] Lehmann, D.; Pnueli, A.; Stavi, A., Impartially, justice and fairness: The ethics of concurrent termation, (Proc. Internat. Conf. Automata, Languages and Programming. Proc. Internat. Conf. Automata, Languages and Programming, Lecture Notes in Computer Science, 115 (1981), Springer: Springer Berlin), 264-277 · Zbl 0468.68026
[7] Manna, Z.; Pnueli, A., Verification of concurrent programs: Temporal proof principles, (Kozen, D., Logic of Programs. Logic of Programs, Lecture Notes in Computer Science, 154 (1982), Springer: Springer Berlin), 200-252 · Zbl 0481.68019
[8] Marek, W., Private communication (1986)
[9] Mazurkiewicz, A., Traces, histories, graphs: Instances of a process monoid, (Chytil, M., Mathematical Foundations of Computer Science 1984. Mathematical Foundations of Computer Science 1984, Lecture Notes in Computer Science, 176 (1984), Springer: Springer Berlin), 115-133 · Zbl 0577.68061
[10] Mazurkiewicz, A., Complete processes and inevitability, (Report 86-06 (1986), University of Leiden)
[11] Mazurkiewicz, A., Trace theory, (Brauer, W.; Reisig, W.; Rozenberg, G., Advances in Petri Nets 1986, Part II. Advances in Petri Nets 1986, Part II, Lecture Notes in Computer Science, 255 (1987), Springer: Springer Berlin), 279-324
[12] Merceron, A., Fair processes, (Rozenberg, G., Advances in Petri Nets 1987. Advances in Petri Nets 1987, Lecture Notes in Computer Science, 266 (1987), Springer: Springer Berlin), 181-195
[13] Nielsen, M.; Plotkin, G.; Winskel, G., Petri nets, event structures and domains, Theoret. Comput. Sci., 13, 85-108 (1981), Part 1 · Zbl 0452.68067
[14] Ochmański, E., Inevitability in concurrent systems, Inform. Process. Lett., 25, 221-225 (1987) · Zbl 0653.68011
[15] Owicki, S.; Lamport, L., Proving liveness properties of concurrent programs, ACM Trans. Programming Languages and Systems, 4, 3, 455-495 (1982) · Zbl 0483.68013
[16] Penczek, W., Inevitability in diamond-discrete systems, ICS PAS Report 598 (1986)
[17] Petri, C. A., Non-sequential processes, GMD-ISF Report 77-05 (1977)
[18] Pnueli, A., The temporal semantics of concurrent programs, Theoret. Comput. Sci., 13, 45-60 (1981) · Zbl 0441.68010
[19] Reisig, W., Petri Nets—An Introduction, (EATCS Monographs on Theoretical Computer Science (1985), Springer: Springer Berlin) · Zbl 0521.68057
[20] Shields, M. W., Nonsequential Behaviour, (Tech. Rept. CSR-120-82 (1982), Dept. of Computer Science, University of Edinburgh), Part 1 · Zbl 0562.68061
[21] Winkowski, J., Behaviours of concurrent systems, Theoret. Comput. Sci., 12, 39-60 (1980) · Zbl 0445.68044
[22] Zorn, M., A remark on method in transfinite algebra, Bull. Amer. Math. Soc., 41, 667-670 (1935) · JFM 61.1028.01
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.