Notes and Further Reading

In Chapter 7, we mentioned that the general LTL model-checking procedure – that of translating the negation of the required LTL formula into a Büchi automaton, composing this automaton with the target model and then searching for connected components containing acceptance states – is due to Gribomont and Wolper (1989). We also mentioned that this technique has found widespread usage in the SPIN model checker (Holtzmann, 1991, 1997). Indeed, as far as possible, we have followed the syntax of LTL formulae used in SPIN. The use of fluents in the context of LTL model checking is due to Giannakopoulou and Magee (2003) and the component used in the LTSA to translate LTL formulae into Büchi automata is due to Giannakopoulou and Lerda (2002). A version of FLTL for specifying the properties of the timed models of Chapter 12 can be found in Letier, Kramer, Magee, et al. (2005). The term “fluent” originally comes from the time-varying quantity in Newton’s calculus but has more recently been adopted by the Artificial Intelligence community with a meaning consistent with the one used here (Sandewall, 1995).

Most properties specified in LTL conform to a restricted set of forms or patterns. A set of patterns used in specifying properties has been codified by Dwyer, Avrunin and Corbett (1999). These patterns are coded in a number of formalisms that include linear temporal logic and computation tree logic (CTL). While LTL is defined with respect to infinite execution sequences or linear time, CTL is a temporal logic defined with respect to a branching tree of execution paths or branching time. CTL was used in the model-checking work originated by Clarke, Emerson and Sistla (1986). There has been much academic debate on the relative advantages of LTL and CTL, starting with the classic paper by Lamport (1980) entitled “Sometime” Is Sometimes “Not Never”: On the Temporal Logic of Programs to the more recent Branching vs. Linear Time: Final Showdown by Vardi (2001). Pnueli (1977) was responsible for the original idea of using temporal logic as the logical basis for proving correctness properties of concurrent programs.

Finally, it should be noted that the database ring is due to Bill Roscoe (1998). The example, which was used to illustrate an approach to modeling change in the form of safe node deletion and creation, appears in a paper by Kramer and Magee (1998).