Temporal logic and state systems (Q2517767): Difference between revisions

The book presents various (mostly) linear-time temporal logics, their syntax, semantics, theory and applications. In Chapter 1 (Basic concepts and notations of logics) some basic notions of propositional and first-order logic are recalled. The next chapter (Basic propositional linear temporal logic) introduces the basic language and its semantics, axiomatization, completeness and decidability results. At the end, initial validity semantics -- validity is connected only with the initial state -- is discussed. Chapter 3 (Extensions of LTL) deals with various extensions (variants of until operators, fixpoint operators, past operators etc.). In Chapter 4 (Expressiveness of propositional linear temporal logic) various automata, like Büchi automata and weak alternating automata, are exploited to study expressiveness of logics. Chapter 5 (First-order linear temporal logic), besides giving basic notions of the logic, discusses also its incompletness and several extensions. Chapter 6 (State systems) deals with labeled/rooted/state transition systems and their specifications by means of temporal logics. Chapter 7 (Verification of state systems) explains techniques of deductive verification for some typical classes of system properties and illustrate them on two examples -- a self-stabilizing network and the alternating bit protocol. Verification of two types of concurrent programs (shared variable and message passing) is studied in Chapter 8 (Verification of concurrent programs) and illustrated by the properties of two examples -- a mutual exclusion and a producer-consumer program. In Chapter 9 (Structured specification) three structuring concepts (refinement, hiding and composition) are addressed and it is studied how these specification methods can be covered within temporal logic in general and with temporal logic of actions in particular. Chapter 10 (Other temporal logics) deals with interval and branching-time temporal logic, CTL, CTL\(^\star\), logics for true concurrency etc. The last chapter (System verification by model checking) is devoted to model checking for some of the above-mentioned logics. Besides the main text, the book contains also paragraphs, called ``second reading'', which bring some additional or complementary points of view and which can be skipped without loss of continuity.