1.1 --- a/paper/src/paper.tex	Fri Jul 08 14:53:15 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Fri Jul 08 14:54:53 2011 +0200
     1.3 @@ -71,37 +71,7 @@
     1.4  %\normalfont
     1.5  \newpage
     1.6  \section{Introduction}
     1.7 -Program verification is a fundamental area of study in computer science. The broad goal
     1.8 -is to verify whether a program is ``correct''--i.e., whether the implementation of a program
     1.9 -meets its specification. This is, in general, too ambitious a goal and several assumptions
    1.10 -have to be made in order to render the problem tractable. In these lectures, we will focus
    1.11 -on the verification of finite-state reactive programs. For specifying properties of programs,
    1.12 -we use linear time temporal logic.
    1.13  
    1.14 -What is a reactive program? The general pattern along which a conventional program
    1.15 -executes is the following: it accepts an input, performs some computation, and yields an
    1.16 -output. Thus, such a program can be viewed as an abstract function from an input domain
    1.17 -to an output domain whose behaviour consists of a transformation from initial states to
    1.18 -final states.
    1.19 -
    1.20 -In contrast, a reactive program is not expected to terminate. As the name suggests, such
    1.21 -systems “react” to their environment on a continuous basis, responding appropriately to
    1.22 -each input. Examples of such systems include operating systems, schedulers, discrete-event
    1.23 -controllers etc. (Often, reactive systems are complex distributed programs, so concurrency
    1.24 -also has to be taken into account. We will not stress on this aspect in these lectures—we
    1.25 -take the view that a run of a distributed system can be represented as a sequence, by
    1.26 -arbitrarily interleaving concurrent actions.)
    1.27 -
    1.28 -To specify the behaviour of a reactive system, we need a mechanism for talking about
    1.29 -the way the system evolves along potentially infinite computations. Temporal logic 
    1.30 -has become a well-established formalism for this purpose. Many varieties of temporal logic
    1.31 -have been defined in the past twenty years—we focus on propositional linear time temporal
    1.32 -logic (LTL).
    1.33 -
    1.34 -There is an intimate connection between models of LTL formulas and languages of
    1.35 -infinite words—the models of an LTL formula constitute an ω-regular language over an
    1.36 -appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking
    1.37 -for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
    1.38  
    1.39  \section{$\omega$-regular languages}
    1.40  \begin{def:finite words}