ICG Chapter 1 Introduction
Questions about the lecture 'Infinte computations and games' of the RWTH Aachen Chapter 1 Introduction
Questions about the lecture 'Infinte computations and games' of the RWTH Aachen Chapter 1 Introduction
-
- 1 / 20
-
Lernkarten
What is the characteristic?
[sofar.motivation]
Theory of regular languages and finite automata on finite words // FoSAP
What is the characteristic?
[now.motivation, 3]
1. Theory of regular languages and finite automata on (one-sided) infinite words
2. Automata on infinite trees
3. Games of infinite duration
List the reasons!
[why.now.motivation, 3]
1. Model executions of non-terminating systems
2. Represent real numbers with infinite words
3. Decision procedure for logics on infinite structures
List them!
[executions.why.now.motivation, 3]
1. One execution is a infinite word
2. All executions are a infinite tree
3. Interaction with environment is a infinite game
What happened 1960?
[history]
Decision problems in logic and circuit design
What happened 1962?
[history]
Program synthesis and Church’s problem
What are the characteristics?
[1962.history, 2]
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)
What happened 1969?
[history]
View Church’s problem as game between player input and player output
What happened 1980s?
[history]
Theoretical foundations for applications in verification
What happened 1990s?
[history]
Industrial applications in verification // Tool “Spin”
What happened 2000s?
[history]
First tools for synthesis
List them!
[notations, 7+2]
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
What are the characteristics?
[infwords.notations, 3]
1. Infinite sequences over a Sigma
2. By help of omega // ababab… = (ab)omega
3. Can formally be defined as functions alpha: N→Sigma
What are the characteristics?
[languages.notations, 3]
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
What are the characteristics?
[büchi, 3]
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
What is the definition?
[DBA.büchi, 4]
1. A=(Q,Sigma,q0,delta,F) with delta: Q x Simga → Q
2. Unique run on alpha in Sigmaomega is rho in Qomega
3. A accepts alpha if rho(i) in F for infinitely many I
4. L(A):={alpha in Sigmaomega| A accepts alpha} the omega-language
What is the definition?
[rho.DBA.büchi, 2]
1. rho(0)=q0
2. rho(i+1)=delta(rho(i),alpha(i))
What is the definition?
[NBA.büchi, 4]
1. A=(Q,Sigma,q0,Delta,F) with Delta \subseteq Q x Simga x Q
2. Run on alpha in Sigmaomega is rho in Qomega
3. A accepts alpha is there is at least one accepting run of A on alpha
4. Language is defined as for DBA
What is the definition?
[rho.NBA.büchi, 2]
1. rho(0)=q0
2. (rho(i),alpha(i),rho(i+1)) in Delta
What is the definition?
[theorem.büchi]
The class of DBA recognizable languages is not closed under complement
