Temporal logics in computer science. Finite-state systems (Q2805273)

Part I (Models) presents basic theory of abstract models for the temporal logics that are studied here, i.e., transition systems. It includes trace equivalence, bisimulation, bisimulation games and reachability. Part II (Logics) is the core part of the book. In six chapters it presents and studies the most important temporal logics used for specification and verification of discrete transition systems and their variations. After the preparatory chapter it starts with Basic Modal Logic (Chapter 5), its relation to bisimulation, and studies the logical decision problem of model checking and satisfiability testing for BML and model-checking games. Chapter 6 is devoted to Linear Time Temporal Logics (semantics, expressiveness, model checking and testing for satisfiability, validity and axiomatic system). The most interesting extensions of LTL (with past-time operator, automata-based operator, propositional quantification) over linear models are presented as well. The next chapter is devoted to Branching Time Temporal Logics (TLR, CTL, CTL*, model checking for them and axiomatization for TLR and CTL). Chapter 8 deals with the Modal Mu-Calculus, which presents the most expressive of all temporal logics studied in the book (embedding of all of them into mu-calculus is shown). The chapter also offers a comparison with other formalisms, such as monadic second-order logic and linear-time mu-calculus. The second part ends with Alternating-Time Temporal Logics. It introduces also concurrent game structures as multiagent generalization of the transition systems. Part III (Properties) with two chapters deals with two fundamental generic questions about temporal logics: their expressiveness and computational complexity (both upper and lower bounds) of their main logical decision problems (satisfiability and model checking). It presents both positive results as well as negative expressiveness results, i.e., that some property in one logic is not expressible in another. The last part (IV, Methods) presents three fundamental methods for solving decision problems for temporal logics, each of its three chapters deals with one of them. Tableaux-Based Decision Methods for BML, LTL, TLR and CTL are presented. For CTL* and mu-calculus alternative decision methods, using automata and games, have been developed. The chapter on the Automata-Based Approach develops the approach to the main decision problems for temporal logics based on special logical games: model-checking games and satisfiability-checking games. These games are defined by means of an arena on which two players perform plays. The question of whether a given state of an interpreted transition system satisfies a temporal formula is related to the existence of a winning strategy for the proponent player. Except for the first part of the book the subsequent chapters do not need to be read linearly. The authors provide a dependency graph among them what helps readers interested only in some problems covered by the book.