References
Temporal Logics and Model Checking
Logic in Computer Science Modelling and Reasoning
about Systems, Michael Huth and Mark Ryan, Second
Edition, Cambridge University Press, 2004.
Model Checking, Edmund M. Clarke, Orna Grumberg
and Doron A Peled, The MIT Press, 1999.
(Lan: Turning Award was once given to Model Checking.)
Reasoning about Action and
Change
To reason formally about situations we need languages
to describe or specify 刻画 the situation and ways to
construct arguments about these situations.
We use a variety of logics as this language.
(Lan: Here it seems natural language is stronger then
logics, because one natural language can describe most
of the situations. However, natural languages are
ambiguous and often lack of precision. For example, 中国足
球队谁也赢不了；中国乒乓球队谁也赢不了；粮食不卖给八路军；起码二十元)
Initially we consider the specification of problems using
propositional logic 命题逻辑 and a method for reasoning
about such problems.
To deal with action and change we consider temporal
logics 时态逻辑, which allow change over time.
Typical Problems
Often typical problems can be represented by a number
of states that the system can be in and transitions that
link these states together.
Here is an example that shows the behaviour of a
microwave oven (from Clarke, Grumberg, Peled).
(Lan: Let’s read the graph. Start from the center state)
状态机 state machine
Typical Examples–Blocks World
Another well-known example involving actions (relating to
planning) is that of the block world.
We might want to specify the initial situation and what
hold following some sequence of actions.
Typical Problems SKIP
Whilst these are toy problems many real world examples
are of this form (but larger).
Consider:
telephone protocols;
controllers for nuclear reactors, aeroplanes, rockets etc;
life support systems;
chip design;
etc
Specification and Verification
Formal specification is the description of a problem or
system (or its requirements) in a formal language such
as logic.
Informal specifications eg descriptions in English, may be
ambiguous which could lead to errors in design or
implementations which may be expensive.
Formal specifications are unambiguous.
Verification is the process of ensuring that the system
behaves as expected, i.e. the task of showing that the
required properties follow from the formal specification.
Testing may detect bugs in the developed system but is
not guaranteed to cover all paths through the system or
all possible situations.
Why Bother? SKIP
We need assurances that systems will behave as
required particularly in the following situations:
safety-critical systems eg nuclear reactors, aeroplanes,
road and air traffic control, space systems, life support
systems;
commercially critical eg mass produced chips, bank
systems, telephone networks;
mission critical etc
Failure may be costly in terms of life, money, reputation
etc
Examples of Software Failure
Therac-25 accident 1985-7, where a software failure
caused the wrong dosages of x-rays costing human lives.
The fault in the division algorithm in the Pentium chip in
1994 which cost Intel over 300M pounds.
The Ariane 5 rocket exploded in 1996 40 seconds after
take off due to an unexpected software exception which
cost 300m pounds.
(Lan: Soviet Union, a fault in the defensive systems)
Arguments
Consider the following argument
If it is sunny and it is the weekend Sean goes camping.
Sean does not go camping. It is sunny. Therefore it is
not the weekend.
Is this a valid argument?
In the next few lectures we will show how to formulate
this in propositional logic and show whether this
argument is valid (or not).
