×

zbMATH — the first resource for mathematics

Concurrent systems and inevitability. (English) Zbl 0675.68015
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.

MSC:
68N25 Theory of operating systems
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
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 Amsterdam · Zbl 0165.01701
[6] Lehmann, D.; Pnueli, A.; Stavi, A., Impartially, justice and fairness: the ethics of concurrent termation, (), 264-277
[7] Manna, Z.; Pnueli, A., Verification of concurrent programs: temporal proof principles, (), 200-252
[8] Marek, W., Private communication, (1986)
[9] Mazurkiewicz, A., Traces, histories, graphs: instances of a process monoid, (), 115-133
[10] Mazurkiewicz, A., Complete processes and inevitability, ()
[11] Mazurkiewicz, A., Trace theory, (), 279-324
[12] Merceron, A., Fair processes, (), 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, () · Zbl 0521.68057
[20] Shields, M.W., Nonsequential behaviour, (), 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.