Transition systems are widely used to model computer programs and systems. They consist of states, representing possible configurations, and transitions, representing possible state changes. Such changes may be governed by an action induced by the system itself or by an external event. This is a fundamental model to define the semantics of computer systems or abstract computational devices such as finite statemachines, pushdown systems, Turing machines, counter machines, timed automata, etc. Besides, many other models of sequential, parallel, reactive and interactive processes and computations, such as Petri nets, process calculi such as CCS and CSP, etc., can naturally be recast as transition systems.

Transition systems are mathematically quite simple, as they can be viewed as (possibly infinite) directed graphs with labels on vertices or on edges. Yet, theoretical tools developed for them have allowed striking breakthroughs to be made for software verification, in particular due to the approach of verification by model checking.

In the context of this book, transition systems appear in two capacities: as object of primary interest and study, in Part I of the book, and as models for the temporal logics which we will study further. A real system can be modelled by different abstract transition systems and in different levels of detail. It is therefore important to have precise criteria whether a given abstract model faithfully captures the formally specified behaviour of the given real transition system. For that it is necessary to have a precise notion of behaviour of a transition system, so later in this chapter we also address the question:

When should two transition systems be considered to be behaviourally equivalent?

This question does not have a unique answer, as the notion of equivalence depends on the behavioural features of transition systems that are considered of importance for the real systems they model. Such features may involve local behaviour (pre- and postconditions), generated paths and computations, as well as reachability, safety, liveness, fairness, etc., types of system properties. Accordingly, a variety of natural notions of behavioural equivalence arise. We will concentrate on two of them – bisimilarity and trace equivalence – because they are inherently linked to the notion of logical equivalence.

Temporal logics provide a generic logical framework for modelling and reasoning about time and temporal aspects of the world. While stemming from philosophical considerations and discussions, temporal logics have become over the past 50 years very useful and important in computer science, and particularly for formal specification, verification and synthesis of computerised systems of various nature: sequential, concurrent, reactive, discrete, real time, stochastic, etc. This book provides a comprehensive exposition of the most popular discrete-time temporal logics, used for reasoning about transition systems and computations in them.

Temporal Logics and Computer Science: A Brief Overview

We begin with a brief historical overview of temporal reasoning and logics and their role in computer science.

Historical Origins of Temporal Reasoning and Logics

The study of time and temporal reasoning goes back to the antiquity. For instance, some of Zeno's famous paradoxical arguments refer to the nature of time and the question of infinite divisibility of time intervals. Perhaps the earliest scientific reference on temporal reasoning, however, is Aristotle's ‘Sea Battle Tomorrow’ argument in the Organon II – On Interpretation, Chapter 9, claiming that future contingents, i.e. statements about possible future events which may or may not occur, such as ‘There will be a sea-battle tomorrow’, should not be ascribed definite truth values at the present time. A few decades later the philosopher Diodorus Cronus from the Megarian school illustrated the problem of future contingents in his famous Master Argument where he, inter alia, defined ‘possible’ as ‘what is or will ever be’ and ‘necessary’ as ‘what is and will always be’.

Philosophical discussions on temporality, truth, free will and determinism, and their relationships continued during the Middle ages. In particular, William of Ockham held that propositions about the contingent future cannot be known by humans as true or false because only God knows their truth value now. However, he argued that humans can still freely choose amongst different possible futures, thus suggesting the idea of a futurebranching model of time with many possible time-lines (histories), truth of propositions being relativised to a possible actual history. This model of time is now often called Ockhamist or actualist.

In this chapter we outline some common terminology, notation and facts about syntactic and semantic logical concepts that are used, mutatis mutandis, in all chapters in the part.

We assume that the reader has basic background on propositional and first-order classical logic. Some general references are listed in the bibliographic notes.

Preliminaries on Modal Logic

Modal Logical Languages and Connectives

Throughout the book we assume that the generic notion of modal logic subsumes the one of temporal logic. That applies, in particular, to modal languages, operators, formulae, etc. For instance, whenever we say ‘modal formulae’, that also refers, in particular, to temporal formulae, unless otherwise specified.

Modal languages. Hereafter we assume an arbitrarily fixed multimodal language L with an alphabet containing a possibly infinite set of atomic propositions PROP, a sufficient set of propositional connectives from which all others are definable – typically something like conjunction and negation – plus an abstract family of (usually, unary or binary) modal operators O.We call the pair (O, PROP) the signature of the language. For instance, given the set of actions Act, we will use the set of modal operators O = ﹛EXa, AXa | a ∈ Act﹜. The modal μ-calculus introduced in Chapter 8 follows a slightly different syntax for modal operators, see Section 8.1.1.

Logical connectives. Throughout this book we will use standard notation for the propositional logical connectives, as follows.

1. • _ for truth;

2. • ⊥ for falsum;

3. • ￢ for negation;

4. • ∧ for conjunction;

5. • ∨ for disjunction;

6. • →for implication (a.k.a., conditional);

7. • ↔for bi-implication (a.k.a., bi-conditional). Often this is also called ‘equivalence’.We will reserve the use of this word for relations of equivalence, e.g. between formulae.

In this chapter we will develop a game-theoretic approach to themain decision problems for temporal logics. We will present model-checking games and satisfiability-checking games and use them to characterise the model checking and the satisfiability-checking problem for temporal logics. These games are defined by means of an arena on which two players perform plays. The characterisations then relate the model-checking problem, i.e. the question of whether a given state of an interpreted transition system satisfies a temporal formula, to the existence of a winning strategy for the proponent player in the respective modelchecking game. Likewise, the satisfiability problem, asking the question of whether a given temporal formula is satisfiable, corresponds to the question of whether the proponent player has a winning strategy in the respective satisfiability game.

These game-theoretic characterisations are of particular interest in the context of program verification. Consider the model-checking problem which is used to prove whether some (abstracted) system is correct with respect to a property formulated as a temporal formula. Ifmodel checking returns true, i.e. the property is satisfied and the system is therefore verified, then one can continue the system development process and consider another property for instance. However, if the property is not satisfied, i.e. model checking has returned false, then typically the system needs to be redesigned so that the error causing the nonsatisfaction of the formula is rectified. In order to do this successfully, it is important to know why the property is not satisfied. Game-theoretic characterisations are designed to yield such explanations: the certificate for nonsatisfaction of a property is a winning strategy for the opponent player, called here Refuter and denoted by R. Failure certificates are also important in satisfiability problems, for instance in checking whether a program specification made up of several parts is realisable.

While satisfiability of a temporal formula of BML seems easy to certify by giving a model, it is usually more difficult for logics like CTL and LTL, and much more so for complex logics like CTL* and Lμ. Again, winning strategies in satisfiability games yield certificates that can be used for building such satisfying models.

Before we actually consider temporal logics and their associated games, we introduce the game-theoretic framework abstractly and present the basic concepts like players, plays, winning conditions, winning strategies, etc.

In this chapter we set the stage for the rest of the book. We start by reviewing the notion of a function, then introduce the concept of functional programming, summarise the main features of Haskell and its historical background, and conclude with three small examples that give a taste of Haskell.

Functions

In Haskell, a function is a mapping that takes one or more arguments and produces a single result, and is defined using an equation that gives a name for the function, a name for each of its arguments, and a body that specifies how the result can be calculated in terms of the arguments.

For example, a function double that takes a number x as its argument, and produces the result x + x, can be defined by the following equation:

When a function is applied to actual arguments, the result is obtained by substituting these arguments into the body of the function in place of the argument names. This process may immediately produce a result that cannot be further simplified, such as a number. More commonly, however, the result will be an expression containing other function applications, which must then be processed in the same way to produce the final result.

For example, the result of the application double 3 of the function double to the number 3 can be determined by the following calculation, in which each step is explained by a short comment in curly parentheses:

Similarly, the result of the nested application double (double 2) in which the function double is applied twice can be calculated as follows:

Alternatively, the same result can also be calculated by starting with the outer application of the function double rather than the inner:

In this chapter we introduce types and classes, two of the most fundamental concepts in Haskell. We start by explaining what types are and how they are used in Haskell, then present a number of basic types and ways to build larger types by combining smaller types, discuss function types in more detail, and conclude with the concepts of polymorphic types and type classes.

Basic concepts

A type is a collection of related values. For example, the type Bool contains the two logical values False and True, while the type Bool -> Bool contains all functions that map arguments from Bool to results from Bool, such as the logical negation function not. We use the notation v :: T to mean that v is a value in the type T, and say that v has type T. For example:

More generally, the symbol :: can also be used with expressions that have not yet been evaluated, in which case the notation e :: T means that evaluation of the expression e will produce a value of type T. For example:

In Haskell, every expression must have a type, which is calculated prior to evaluating the expression by a process called type inference. The key to this process is the following simple typing rule for function application, which states that if f is a function that maps arguments of type A to results of type B, and e is an expression of type A, then the application f e has type B:

For example, the typing not False :: Bool can be inferred from this rule using the fact that not :: Bool -> Bool and False :: Bool. On the other hand, the expression not 3 does not have a type under the above rule, because this would require that 3 :: Bool, which is not valid because 3 is not a logical value. Expressions such as not 3 that do not have a type are said to contain a type error, and are deemed to be invalid expressions.

Because type inference precedes evaluation, Haskell programs are type safe, in the sense that type errors can never occur during evaluation.

It is nearly a century ago that Alonzo Church introduced the lambda calculus, and over half a century ago that John McCarthy introduced Lisp, the world's second oldest programming language and the first functional language based on the lambda calculus. By now, every major programming language including JavaScript, C++, Swift, Python, PHP, Visual Basic, Java, … has support for lambda expressions or anonymous higher-order functions.

As with any idea that becomes mainstream, inevitably the underlying foundations and principles get watered down or forgotten. Lisp allowed mutation, yet today many confuse functions as first-class citizens with immutability. At the same time, other effects such as exceptions, reflection, communication with the outside world, and concurrency go unmentioned. Adding recursion in the form of feedback-loops to pure combinational circuits lets us implement mutable state via flip-flops. Similarly, using one effect such as concurrency or input/output we can simulate other effects such as mutability. John Hughes famously stated in his classic paper Why Functional Programming Matters that we cannot make a language more powerful by eliminating features. To that, we add that often we cannot even make a language less powerful by removing features. In this book, Graham demonstrates convincingly that the true value of functional programming lies in leveraging first-class functions to achieve compositionality and equational reasoning. Or in Graham's own words, “functional programming can be viewed as a style of programming in which the basic method of computation is the application of functions to arguments”. These functions do not necessarily have to be pure or statically typed in order to realise the simplicity, elegance, and conciseness of expression that we get from the functional style.

While you can code like a functional hacker in a plethora of languages, a semantically pure and lazy, and syntactically lean and terse language such as Haskell is still the best way to learn how to think like a fundamentalist. Based upon decades of teaching experience, and backed by an impressive stream of research papers, in this book Graham gently guides us through the whole gambit of key functional programming concepts such as higher-order functions, recursion, list comprehensions, algebraic datatypes and pattern matching. The book does not shy away from more advanced concepts.

In this appendix we present some of the most commonly used definitions from the Haskell standard prelude. For expository purposes, a number of the definitions are presented in simplified form. The full version of the prelude is available from the Haskell home page, http://www.haskell.org.

Basic classes

Equality types:

Ordered types:

Showable types:

Readable types:

Numeric types:

Integral types:

Fractional types:

Booleans

Type declaration:

Logical conjunction:

Logical disjunction:

Logical negation:

Guard that always succeeds:

Characters

Type declaration:

The definitions below are provided in the library Data.Char, which can be loaded by entering the following in GHCi or at the start of a script:

Decide if a character is a lower-case letter: