Concurrent systems and inevitability (Q1122355)

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.