Model Checking Reading Club/Baier, Katoen: Principles of Model Checking/03: Linear-Time Properties

These pages contain remarks and comments – many typos and errata, some proposals for change – that we have found during reading the book:

Principles of model checking / Christel Baier; Joost-Pieter Katoen. – Cambridge, Mass.: MIT Press, 2008.

ISBN 978-0-262-02649-9.

For more details, see the table of contents.

Chapter 3: Linear-Time Properties

• 89, 9 ] As Pnueli observed, the issue is not sequential programs versus parallel programs, but rather reactive programs versus non-reactive programs. Sequential programs may be used to control non-terminating activity, and parallel programs often do terminate (Google's map-reduce is an important class of recent examples). Frits Vaandrager

• 89, –10sqq.: Sequential programs ... have a terminal state... Parallel systems ... do not terminate ] The real distinction is between transformational programs and reactive systems: transformational programs receive a single input, compute a well-defined function of it, produce a single output, and terminate (e. g., a compiler). Reactive systems receive a sequence of inputs and react to each input, but keep on running (e. g., an operating system). Typically, transformational programs are sequential, and many reactive systems have multiple threads. David Jansen

• 89, –5: deadlock ] This definition of deadlock is in my opinion incorrect. According to the standard definition, deadlock is a cyclic dependency of processes waiting for each other. A concurrent system may reach a deadlock while some processes can still continue computation and transitions are possible. The identification of deadlocks with terminal states is a misconception: a deadlock does not mean you have a terminal state and vice versa. Frits Vaandrager

• 90, 1, Fault Designed Traffic Lights ] read: Traffic Lights Designed Wrongly

• 90 ] This page is much shorter than page 91.

• 91, unnumbered figure on top of the page ] This figure uses fonts that are quite different from the rest of the book. Further, it should have a number and a caption.

• 91, 3–5 To take some rice out of the bowl, a philosopher needs two chopsticks. ... Thus, at any time only one of two neighboring philosophers can eat. ] Actually, only one of the two can take rice out of the bowl in your formulation of the problem. David Jansen

• 91, 7: Note that a deadlock scenario occurs when all philosophers posses a single chopstick. ] May be misunderstood as: there is just one chopstick which is in the shared possession of all philosophers. Clearer: ... when each philosopher possesses a single chopstick. David Jansen

• 91, 7: Note that a deadlock scenario occurs when all philosophers posses a single chopstick ] This is not true. A deadlock may occur in this case. A necessary condition for deadlock is hold-and-wait: philosophers that posses one chopstick keep it until they've also got the second one. In the randomized version of the dining philosophers it may occur that all philosophers pick up their left fork. Still there is no deadlock in this case since philosophers will put down a fork if they cannot get the other one as well. Frits Vaandrager

• 91, –9 Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle (i-1)} th stick and –5 Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle i-1} th stick ] Please use one variant consistently. See also page 783, 17.

• 92, Figure 3.2 ] Please use action names consistently: either request and release, or req and rel. Frits Vaandrager

• 92, 4 all philosophers pick up their left stick at the same time] This is impossible in the interleaving model. At best, it can be “almost at the same time”. David Jansen

• 92, 6 and 8 ] The names of actions and locations in the text does not match the names that appear in Figure 3.2 and that were introduced earlier. Frits Vaandrager

• 93, Figure 3.3 ] The left part is equal to the left part of Figure 3.2. Why is it repeated here? A reader is searching for the differences. Jasper Berendsen

• 93, Figure 3.3 ] The states should be named: available_i,i and available_i,i+1. Jasper Berendsen

• 93, footnote ] Why do you need to add a transition in order to express that a philosopher may think forever? You have stated no requirement that a TS always should continue performing transitions. There is also no need to add such a requirement. Frits Vaandrager

It may happen that all philosophers become “defective”. However, in the solution you propose it may happen that a philosopher first decides to defect and then gets “repaired”. It would be better to add a new absorbing or terminal state that is reachable from state Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle think_i} . David Jansen

• 94 ] This page is much shorter than page 95.

• 95, 14: reachable ] Note that this equals the set of states reachable in TS. (I wonder why you need the definition of state graph at all.) Frits Vaandrager

• 95, 18, notation Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle Reach(TS)} ] unelegant. I propose to write: noted as Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle Reach(TS)}

• 95, Definition 3.3 ] Is this definition really needed? I think you could use TS everywhere you now use state graphs. Jasper Berendsen

• 95, –5, finite path fragment ] This is the notion you define; please print it in italics.

• 95, Definitions 3.4, 3.5, and 3.6 ] Do you really need these definitions? Why not use execution (fragments) everywhere. When unimportant labels of execution (fragments) can be left out. Jasper Berendsen

• 96, 3 and 4, finite paths ... infinite path ] Read: finite path fragments ... infinite path fragment

• 96, 4, length ] Add: that is, the number of transitions occurring in Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \pi} . (Note that the number of elements occurring in sequence Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \pi} equals Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle n+1} ). Frits Vaandrager
• 96, 8sq., A path fragment is called initial if it starts in an initial state, i.e., if Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle s_0 \in I} . ] Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle s_0} is undefined here. Proposal: A path fragment Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \pi} is called ... if Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle first(\pi) \in I} . David Jansen

• 97, Section 3.2.2 ] Do you really need these definitions? Why not use execution (fragments) everywhere. When unimportant states of execution (fragments) can be left out. Jasper Berendsen

• 97, section 3.2.2, final lines ] If Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle TS} has an empty set of initial states, the set must be extended to include Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle s_{stop}} as an initial state. Tim Leonard

• 97, footnote ] The footnote is continued on the next page. This is ugly.

• 98, 1, Trace and Tace Fragment ] This definition only defines traces, not trace fragments. David Jansen

• 98, 2, Let ] Before this word, there is some spurious white space. Similarly before “Consider” in the first line of Example 3.9.

• 98, continuation of footnote ] Please try to change the page break such that this last half line of the footnote doesn't appear on a new page, for example by reducing the white space between drawing and caption in Figure 3.5 (in Figures 3.6 and 3.7, this space is much smaller), or by using the LaTeX command \enlargethispage (The LaTeX companion, p. 99sq.) David Jansen

• 99 ] This page is much smaller than page 98.

• 100, Definition 3.10, the infinite concatenation of words in Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle 2^{AP}} ] should be “the infinite concatenation of values from the alphabet Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle 2^{AP}} ”. Tim Leonard

• 100, definition 3.11 ] This definition includes transition systems with no traces (as, for example, those with empty initial state sets). Such systems satisfy all LT properties, and are easy to unintentionally produce (as by including a contradiction in the description of the initial states). They’re just hard to implement. Tim Leonard

• 101, –3 Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \{ red_1 \; green_2 \} \{ green_1, green_2 \} , \ldots} ] Read: Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \{ red_1, green_2 \} \{ green_1, green_2 \} \ldots} (comma after Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle red_1} , no comma towards the end)

• 102, 2, Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle P'} and 102, 7, Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle AP'} ] The space between Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle P} and Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle '} is different.

• 102, 2 autonomously ] What is meant is arbitrary: the correct autonomous behavior could very well make the property hold. Jasper Berendsen

• 103, example 3.14, line 7 ] Should be “Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall j. wait_i \in A_j \Rightarrow \exists k \geq j. crit_i \in A_k} for each Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle i \in \{ 1, 2 \}} .” Tim Leonard

• 103, 11 ] I believe lwait should be changed to wait, and the second Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \in} should be changed to Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \not\in} . Frits Vaandrager

• 104, 13 stepwise system design ] Please elaborate on this point. It is unclear for non-experts. Jasper Berendsen

• 105, example 3.16, line 4 ] The notation for this transition doesn’t match the notation in Figure 3.6 on page 99, which it’s referring to. Tim Leonard

• 107, 14: invariant ] There is an imbalance in your approach in that the set of atomic propositions may be infinite and traces consists of infinite sequences of (potentially infinite) sets of propositions, whereas a propositional logic formula may only refer to a finite number of propositions. If, for instance, we consider mutual exclusion with an infinite number of processes the mutex property is not an invariant according to your definition. Frits Vaandrager

• 109, Algoritm 3, ”always Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \Phi} ” ] read LaTeX code: ``always $\Phi$''.

• 109, 110, Algorithms 3 and 4 ] Why is I no input? I have a strong believe that these algorithms can be simplified, making them shorter but also more readable. Why is a sub procedure visit needed? Jasper Berendsen

• 110, Algorithm 4, ”yes” ... ”always Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \Phi} ” ... ”no” ] opening quotation marks are `` in LaTeX. Please correct them in the specification of the output and in the program code.

• 111, 19 Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \textstyle M = \sum_{s \in S} |Post(s)|} ]Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle S} denotes all reachable states here, but all states otherwise. David Jansen

• 111, Theorem 3.21 ] M is not the number of transitions in the reachable fragment of S, since S may have unreachable states. Jasper Berendsen

• 111, 22 ] Your claim that Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle s \models \Phi} can be checked in time linear in the length of Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \Phi} depends on an implicit assumpion namely that Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a \in L(s)} can be checked in constant time. This need not be the case. In fact this predicate does not even have to be decidable (consider an atomic proposition “halt” that holds in a state exactly when all outgoing computation from that state halt). I think you should devote a sentence or so to this issue. Frits Vaandrager

• 111, subsection 3.3.2 to 126, end of 3.4 ] I propose to change the definitions of safety and liveness altogether. I understand that you do not want to start with topology, but you may start with the closure operator in 3.26: “Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle closure(P)} contains all traces that cannot be distinguished from Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle P} in finite time.” Then describe the properties of closure, which can be given an easy intuitive meaning. Then define safety and liveness in terms of this closure operator; the definitions will be much simpler than now. Instead of remark 3.39, you can then add that closure operators with the properties given also define a topology. David Jansen

• 112, 7 ] This definition, and in fact the whole section, is notationally a bit heavy. For German students this is no problem, but elsewehere students may give up. Notation would already improve a bit by the introduction of a special symbol for the set Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle 2^{AP}} . Even better, you can introduce safety and liveness abstractly in a setting of infinatary languages, and then instantiate it to either words overParsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle 2^{AP}} or words over Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle Act} . This would have the additional advantage that you can discuss the link between fairness and liveness properties later on. It is very unsatisfactory that safety, liveness and fairness properties are presented in a single chapter but the first two live in a world of traces over sets of propositions, and the last one lives in a world of traces over actions. Frits Vaandrager

• 112, example 3.23, third line from the bottom ] The specification depends on Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle AP} being Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \{ red, yellow, green \}} and containing no other propositions, though the value of Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle AP} has only been implied, not stated explicitly. Tim Leonard

• 117, –3 ] for any transition system TS without terminal states. Frits Vaandrager

• 121, 2, Several (nonequivalent) notions of liveness ] The sentence sounds as if there is still disagreement about which notion of liveness should be used. We think that Alpern and Schneider's definition is the current standard definition, not just one of the schools. Please also include some literature reference to those nonequivalent definitions. I found this via Google. David Jansen

• 121, –8 to –5, In the context of ... an invariant.) ] I don't understand this sentence. Please reword. David Jansen

• 122, –3 to 123, 10 ] This whole paragraph looks almost superfluous to me. It is at least too wordy. David Jansen

• 123, 1, Is any linear-time property a safety or liveness property? ] I suspect that the authors intended “For an arbitrarily chosen linear-time property Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle P} , is it necessarily true that either Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle P} is a safety property or Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle P} is a liveness property?” But their wording has the alternative reading “Does there exist a linear-time property that is a safety or liveness property?” A better wording would be “Is every linear-time property a safety or liveness property?” Tim Leonard

• 123, 2, answered affirmatively ] Read: answered almost affirmatively

• 123, Lemma 3.36 ] The proof of this lemma becomes trivial once you have defined the topology correctly. – It may be preferable to move this lemma to page 115, where you define closure. David Jansen

• 124, 11, “the machine ... in a row” ] Read: “The ... row.”

• 124, –3, By definition, Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle P_{safe} = closure(P)} is a safety property. ] uses that Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle closure} is idempotent. David Jansen

• 125, 11, ”sharpest” ] Read LaTeX code: ``sharpest''

• 125, middle ] It would be quite instructive to illustrate the construction in the proof of Theorem 3.37 using the example of the beverage vending machine on the previous page. Frits Vaandrager

• 125, –9, Venn diagram ] Figure 3.11 is not a Venn diagram.

• 126, Figure 3.11 ] You are using bitmaps for shading. If you do so, it is better to use horizontal or vertical strokes.

• 126, Fairness ] In all of this section, fairness is always bound to processes. While this is often the case, it is not necessarily so. In particular, in Chapter 10, you assume a different (state-based) notion of fairness. David Jansen

• 127, –8 sq. while ... while ] Unelegant language. Please reword without repetition.

• 127, –2, the fact that ] Read: the possible behaviour where

• 128, –3, a queue (or another “fair” medium) ] This is only the case in a typical implementation by a benevolent programmer who is aware of fairness problems. A lazy, ignorant or cheating programmer may do otherwise by chance or on purpose. David Jansen

• 129, –2, Weak fairness ] Be careful: Weak fairness excludes behaviour where a process is enabled always but doesn't get its turn. However, in practice, weak fairness often implies that the system only produces runs where no process is enabled continuously. David Jansen

• 131, 5, also the enabled actions ... need to be considered. ]It is enough to consider those enabled actions that only happen finitely often.

• 131, 11, Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \langle \ldots \rangle} ] You can remove atomicity if the Reset process sets Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle x} to Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle -2} . Jasper Berendsen, David Jansen and Pieter Koopman

• 131, 17 assignment Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle x = -1} ] Read: assignmentParsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle x:= -1}

• 131, 18 ] This example is not an illustration of the preceding definition, which is what one would expect. The notion of unconditional process fairness has not yet been defined formally. A potential problem is that the process Reset is finite. Thus there are no fair executions anyway. Frits Vaandrager

• 132, 1 an execution fragment that only visits finitely many states in which some Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} -actions are enabled ... is ... not stronglyParsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} -fair. ] Wrong! This execution fragment is also strongly Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} -fair! You probably wanted to say something like: an execution fragment that visits infinitely many states in which noParsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} -action is enabled is weakly Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} -fair but may not be strongly Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} -fair. David Jansen

• 132, –14, the premise of strong fairness is vacuously false ]Mixing of two expressions. Either read: the premise is false, or read: The implication is vacuously true because its premise is false.

• 133, 4, Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \mathcal{F}} ] Please make clear that these are sets of sets of actions. On slide 17 of Katoen's Lecture #7, there is an error: Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \in 2^{Act}} should be replaced by Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \subseteq 2^{Act}} .

• 133, –2 Weak, and unconditional ] Weak and unconditional (no comma)

• 134, 10, any finite trace is fair by default ] I think this does not hold for unconditional fairness. David Jansen

• 134, –4, when both processes are waiting ] Read: when both processes are trying infinitely often

• 135, –13, we are confronted with a situation ] add: where, for some Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle P} ,

• 135, –1 ] You may want to add Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle TS \models P \Rightarrow} at the beginning of the line.

• 135 ] This page is much smaller than page 134.

• 136, –15, never leave its noncritical section ] This is a perfectly valid assumption that may even hold for some initial conditions of the processes. In more cases, it may happen that a process only wants to enter its critical section a finite number of times. What you probably wanted to forbid is that a process never leaves its critical section. To this end, a weak fairness requirement on the transition leaving the critical section is more appropriate. David Jansen

• 136, –7, Peterson's algorithm satisfies the strong fairness property] I cannot see why this requirement is a strong fairness property. Note that the requirement is weaker than the one stated in line –11, as it does not require that a process requests access to its critical section infinitely often. David Jansen

• 137, –9, (In case there are terminal states, each finite execution is considered to be fair.) ] Please move this fundamental assumption to a more prominent place. David Jansen

• 138, 4 ] Synchronization actions only have to take place infinitely often in case they are infinitely often enabled. Frits Vaandrager

• 138, 9sq., Whereas (3.2) allows processes to always synchronize on the same action, (3.1) does not permit this. ] except if Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle Syn_{i,j}} is a singleton. David Jansen

• 138, –14 ] Strong fairness does not require that synchronization is infinitely often enabled! Frits Vaandrager

• 138, –2 ] In general it is not the case that the ability to perform an internal action is enabled until it is executed. An internal action may be disabled due to the occurrence of a synchronization. Frits Vaandrager

• 141, –4 ] Where is the subsection linking fairness and liveness? There are several results in this area (for instance mypaper with Judi Romijn). Maybe it goes too far to discuss there results in detail, but right now the reader is leaving this chapter in a state of confusion. In fact, I think the concept of a scheduler that extends each finite execution into a fair one is instructive (in particular that such schedulers do not always exist for unconditional fairness, for fairness wrt an uncountable class of fairness sets, etc). Cf also the wonderful paper of Apt, Francez and Katz. At least you should define how a fairness property can be viewed as a safety property. Frits Vaandrager

• 143, 11 van de Snepscheut ] read: Van de Snepscheut (“van” in Dutch names with capital if not preceded by first name). [anonymous comment]

... but this may confuse English readers. David Jansen

• 146, figure on top of page ] Please add arrows to make clear in what direction the data flows. David Jansen
• 147, Exercise 3.15, –3, on the right ] The figure is actually on the next page.