ICG Chapter 1 Introduction

1. Theory of regular languages and finite automata on (one-sided) infinite words

2. Automata on infinite trees

3. Games of infinite duration

1. Model executions of non-terminating systems

2. Represent real numbers with infinite words

3. Decision procedure for logics on infinite structures

1. One execution is a infinite word

2. All executions are a infinite tree

3. Interaction with environment is a infinite game

Decision problems in logic and circuit design

Program synthesis and Church’s problem

1. Running program generates a non-terminating sequence of output beta from input alpha signals

2. Task is to automatically synthesize a program from the specification phi(alpha,beta)

View Church’s problem as game between player input and player output

Theoretical foundations for applications in verification

Industrial applications in verification // Tool “Spin”

First tools for synthesis

1. Sigma is a finite alphabet

2. a,b,c,… represent letters of an alphabet

3. Sigma* is the set of finite words over Sigma

4. u,v,w,… represent finite words

5. eps is the empty word

6. Sigma⁺ is the set of non-empty finite words over Sigma

7. N is the set of natural numbers including 0

8. Infinite words

9. Languages

1. Infinite sequences over a Sigma

2. By help of omega // ababab… = (ab)^omega

3. Can formally be defined as functions alpha: N→Sigma

1. All words with a certain property over Sigma

2. omega defines order type of natural numbers // Two sided infinite words are also possible

3. L is called Büchi recognizable if there is an NBA A with L(A)=L

1. Always NBA if not mentioned explicitly

2. Every DBA can be viewed as NBA

3. There are Büchi recognizable languages that are no DBA recognizable

1. A=(Q,Sigma,q₀,delta,F) with delta: Q x Simga → Q

2. Unique run on alpha in Sigma^omega is rho in Q^omega

3. A accepts alpha if rho(i) in F for infinitely many I

4. L(A):={alpha in Sigma^omega| A accepts alpha} the omega-language

1. rho(0)=q₀

2. rho(i+1)=delta(rho(i),alpha(i))

1. A=(Q,Sigma,q₀,Delta,F) with Delta \subseteq Q x Simga x Q

2. Run on alpha in Sigma^omega is rho in Q^omega

3. A accepts alpha is there is at least one accepting run of A on alpha

4. Language is defined as for DBA

1. rho(0)=q₀

2. (rho(i),alpha(i),rho(i+1)) in Delta

The class of DBA recognizable languages is not closed under complement