Modelling Computing Systems

This chapter provides an introduction to propositional logic. Its main emphasis is on describing how formal logical reasoning in terms of statements, arguments and deductions can be obtained from natural language; on discussing the advantages of this formalisation by looking at ambiguities of natural languages; and on clarifying the important role of logic in computer science and computational modelling through a number of examples. The first section introduces, in a light-weight way, the syntax or language of propositional logic and its semantics, which explains the truth of logical statements. The connectives of propositional logic (negation, disjunction, conjunction, implication and equivalence) are presented together with conditions for the truth and falsity of statements that contain them. Their use in natural language is illustrated by examples. In a more formal approach, the syntax of propositional logic is then introduced, including formation rules and well-formedness checks for formulae, precedences for connectives and syntax trees. The semantics of propositional logic is formally defined via truth tables. Semantic concepts such as satisfiability, logical equivalence and validity of statements, tautologies and contradictions are defined as well. Finally, algebraic laws of logical equivalences, similar to those of Boolean algebra, are presented.

This chapter introduces the fundamental notation, concepts and operations for reasoning with sets and applies these in a number of modelling examples. The first section presents set builder notation to declare the set of all elements with a certain property; introduces the notion of cardinality of a finite set; and introduces notation for common sets in mathematics such as the empty set and the set of natural numbers. The next section discusses the notion of set membership and defines what it means for two sets to be equal, and for one set to be a subset of another set. The correspondence between sets and properties is further explored in the next two sections, including a discussion of Russell’s paradox. Next, the standard operations of union, intersection, difference and complementation are defined and more advanced properties such as power sets, generalised unions and intersections, as well as ordered pairs, tuples and Cartesian products are introduced. Modelling and reasoning with sets is practiced in a number of puzzles and examples. Algebraic laws for reasoning with sets, essentially those of Boolean algebras, are explored in the final section.

Algebraic reasoning in propositional logic and with sets is further abstracted in this optional chapter which studies the principles of Boolean algebras and their application in modelling computing systems through hardware design. A Boolean algebra is formally defined as a set with operations of join, meet and complementation as well as two distinguished elements 1 and 0 that satisfy a number of equational axioms. Three examples of Boolean algebra are presented to illustrate the axioms: the two-element Boolean algebra; the power set Boolean algebras; and the Boolean algebra of proposition. Next, fundamental laws of Boolean algebra, including absorption and De Morgan laws, are derived from the axioms by equational reasoning; and a duality principle is used to yield some of these theorems for free. Boolean algebra is then used for modelling basic logic gates (and gates, or gates and not gates), and it is shown how these elementary gates can be used to implement more complex circuitry, including half adders and full adders. It is also explored how Boolean algebra can play a role in implementing hardware circuits with a minimal numbers of basic gates.

This chapter contains a gentle introduction to the basics of predicate logic. The main emphasis is on the translation of natural language sentences and the use of predicate symbols and quantifiers to express natural language and mathematical properties. The notions of predicates, free and bound variable, and universal and existential quantification are introduced by example. The truth and falsity of universal and existential statements are explained and explored informally. Next, notions of bounded and restricted quantification are introduced, where quantifiers range over the elements of some given set or state that precisely one element has a certain property, and related with standard quantification. A few rules for reasoning with quantifiers, e.g. for pushing quantifiers into and out of formulae, are presented and a few logical puzzles and modelling examples are given.

This chapter introduces some elementary proof strategies for deriving theorems in propositional and predicate logic from assumptions, and these strategies are illustrated on a number of example proofs. A general distinction is made between strategies that introduce a certain logical connective into a proof and those that eliminate a connective from a proof; the former is used to derive a proof goal in a compositional way from simpler ones, while the latter is used to decompose an assumption or statement into simper ones on the way to deriving a goal. The strategies include well known principles such as modus ponens, modus tollens, proof by contradiction, contraposition and case analysis. Proof examples examined include Pythagoras’ proof that the square root of two is irrational, Euclid’s fundamental theorem of arithmetic, a proof that there are infinitely many prime numbers, and a non-constructive argument that one irrational number raised to the power of another can be rational.

This chapter reviews the fundamental properties of functions. After this concept has been defined, basic concepts such as the domain, codomain, range, image, preimage and arity of a function are introduced. Through the notion of graphs, functions are then related to sets of ordered pairs. Next, injective (one-to-one), surjective (onto) and bijective functions are defined and various of their basic properties are derived, such as the fact that bijective functions have inverses. Function composition is introduced and its algebraic properties are investigated. The connection between bijections and cardinalities of sets is explored, including the Schröder-Bernstein theorem and Cantor’s diagonalisation argument. Fixed points of monotonic functions are also explored, with a presentation of the Knaster-Tarski theorem and a method for computing fixed points by iteration.

This chapter introduces relations between sets with an emphasis on binary relations. Formally, n-ary relations are defined as sets of n-tuples, hence binary relations as sets of ordered pairs. In the latter case, the notion of source and target sets is introduced and a distinction between general heterogeneous relations and homogeneous relations, where the source and target set are the same, is made. Graphical ways of presenting relations are introduced and it is shown that functions arise as special cases of binary relations through their graphs. Next, various operations on binary relations are explained; beyond Boolean operations such as union, intersection and complementation these are the composition of relations, the converse of a relation and the domain and range of a relation. After that, special binary relations, such as reflexive and irreflexive relations, symmetric and antisymmetric relations as well as transitive relations are introduced. They are then used to define order and equivalence relations, as well as advanced notions such as equivalence classes and partitions.

This chapter introduces inductively defined sets and simple inductive data types such as natural numbers, words, lists and trees with emphasis on definition patterns. For these sets and data types, recursive equations in Backus-Naur form are introduced and it is shown how, e.g., propositional formulae and simple while programs can be specified in this format. Next it is explained how functions can be defined inductively on such sets and data types. Examples include the factorial function, Harmonic numbers, Fibonacci numbers, addition and multiplication on natural numbers and functions that compute the length of a word or list and the height of a tree. In contrast, recursive functions are defined in a way that does not necessarily lead to terminating evaluations. Recursive procedures are also described, with examples presented of various sorting algorithms and the Towers of Hanoi puzzle.

This chapter explores the fact that properties of inductively defined objects can often be verified by inductive proofs, which is of fundamental importance to computing. The induction principle is motivated by examples based on natural numbers and then expanded to other data types and generalised to principles of structural, strong and well-founded induction. As a motivating example an inductive argument for verifying the closed formula for adding up n consecutive numbers is considered. Based on this, the induction principle is developed from different points of view, and further basic examples are explored. The principle of strong induction, where the induction hypothesis for all predecessor numbers can be used, is then presented and applied. Next, the correspondence between inductive definitions and inductive proofs is examined in detail and various inductive proofs about Fibonacci numbers are presented. The two last sections are devoted to pseudo-proofs such as the Sorites paradox and inductive proofs in computer science applications.

This chapter introduces notions of games and strategies from a computational point of view through many examples based on board games and puzzles. More specifically the games considered are two-player perfect information games. Notions of games and (winning) strategies are first explained in an informal way and simple facts about such games are presented. After that several examples of games are presented, including variants of Nim, Chomp, Hex and Bridg-It. In the case of Nim, winning strategies for the first or the second player are presented. In the case of Chomp, it is shown that the first player always has a winning strategy although the proof does not explain this strategy in any way. Similar proofs are then presented in the cases of Hex and Bridg-It.

This chapter introduces labelled transition systems as a simple graphical formalism for modelling processes. Labelled transition systems consist of states and transitions between states that are labelled by action symbols; they describe how computing systems change their states when performing certain actions. Various puzzles are modelled using labelled transition systems, followed by more serious examples including a program for computing greatest common divisors, a lamp controller, and an elevator controller. Next, a simple language for describing processes that are formed from the actions in labelled transition systems is introduced. It is shown abstractly and in several concrete examples how processes correspond to labelled transition systems by writing down process equations. The most important operations on processes are action prefix and choice. Using the example of a simple vending machine it is then examined at an informal level how processes or behaviours of computing systems could be identified or distinguished, and a simple necessary criterion for process equivalence is introduced.

In this chapter, two-player games are used as a tool for distinguishing between processes: in a simple copy-cat game, the first player aims at showing that two processes are different while the second player tries to show that they are equivalent. Such games, in which the second player must replicate each move by the first player on one process by a move along the same label in the other process, prepare for a more formal definition of bisimulation equivalence. Games can either be limited to a finite number of moves or be infinite, and notions of game equivalences parametrised by the length of the game are defined in terms of the existence of a winning strategy for the second player. It is then shown that properties of finite bisimulation games can be established by induction whereas those of infinite games require a different, coinductive approach. Next, a bisimulation relation on processes or labelled transition systems is formally defined and a proof principle for infinite games based on bisimulation relations is provided. Finally, a partition-refinement algorithm for infinite game equivalence based on bisimulation colourings is introduced, and bisimulation games for arbitrary ordinals are investigated.

In this chapter a Hennessy-Milner style modal logic for specifying properties of processes is introduced. These properties express specific capabilities of a process. After the definition of the syntax of this logic and its semantics with respect to processes or labelled transition systems, the power of this logic in distinguishing processes is illustrated by a number of examples, including the vending machines from the previous chapter. It is shown that any property expressed in this logic can be expressed without negation. Next, the logic is related to bisimulation equivalence; specifically, it is shown that no formula of modal depth n can distinguish n-game equivalent processes on that system. Characteristic formulae for processes are explored, as well as an alternative approach to defining the semantics of properties.

This chapter expands the process language by an operation of concurrent composition of processes. The operation considered is called synchronisation merge because it allows processes to synchronise on particular actions, while others can be performed independently of another. This operation is then applied in several examples to model concurrent processes in computing systems. Counters of bounded capacity are implemented as concurrent compositions of counters of capacity one. A simple controller for a railway level crossing is design, with the system modelled as the concurrent composition of the road, the rail and the controller; safety and liveness properties of the controller are considered in detail. Various mutual exclusion algorithms are considered, including for the dining philosophers problem and Peterson’s algorithm for two processes attempting to access a shared critical section. Simple sender-receiver protocols are also presented, including a version of the alternating bit protocol.

This chapter considers expanding modal logic by operators that allow one to express standard global and temporal properties of a process or labelled transition system. These include temporal operators for expressing when a property is always, possibly, or eventually true in the future. These operators are associated with fixed point equations over the modal logic, and it is shown how solutions for these equations can be obtained by evaluating these equations over a given labelled transition system. Next, the syntax and semantics of the modal mu-calculus are formally introduced and it is shown how, for the negation-free fragment, solutions for modal formulae can be computed. It is then discussed how recursive properties of processes can be encoded by using least and greatest fixed points and how these fixed points can be computed iteratively. As examples, it is shown how the standard temporal operators considered can be defined in the modal mu-calculus, as well as various other advanced properties.