7 Seiten

LiteraturBearbeiten

Abkürzung Titel Autor Block vorhanden? gelesen?
CompCompl Computational Complexity Papadimitriou 1 Nein / (eventuell Stefan fragen)
CompComplModern Computational Complexity - A Modern Approach Arora, Barak 1 PDF
DecProc Decision Procedures Kroening, Strichman 2 PDF + geliehen
LogicInCS Logic in Computer Science Huth, Ryan 3+4 PDF + geliehen
SciPro The Science of Programming Gries 3 PDF + gekauft
PrincModCheck Principles of Model Checking Baier, Katoen 4 PDF

Complexity TheoryBearbeiten

Computation and ComputabilityBearbeiten

DefinitionsBearbeiten

Problem

Question + infinite set of possible instances.


Decidability

A decision problem P is called decidable if there exists an algorithm for P.
Otherwise, if there doesn’t exist an algorithm for P, then P is called undecidable.


Semi-Decidability

A decision problem P is called semi-decidable if we can build a program Π such that:
* Π takes as input instances I of P;
* if I is a “yes” instance, then Π returns true;
* if I is a “no” instance, then Π returns false or does not terminate;


Algorithm

An algorithm for a problem P is a description of computation steps that allow to solve any given instance of the problem P.


Programming Languages and Programs

Programming languages allow us to write programs, which are formal descriptions of computation steps.


TheoremsBearbeiten

If $P$ is a decidable decision problem and $\overline P$ is the complement of $P$, then $\overline P$ is also decidable.


Proof: Invert outputs of complement decidable program.

If P is a decision problem, $\overline P$ is the complement of P, and both P and $\overline P$ are semi-decidable, then P is decidable.


Proof: Run both semi-decidable programs in parallel.

If P is a decision problem such that

1. P is undecidable, and
2. P is semi-decidable,

then the complement $\overline P$ of P is not semi-decidable.


Complexity of Problems and AlgorithmsBearbeiten

• tractable -> P
• intractable -> NP
• provable intractable -> EXPTIME

The Class PBearbeiten

The class P consists of all decision problems P satisfying the following:

1. there is a program Π that decides P, and Π is such that
2. for all instances I of P, the run time of Π on I is polynomial in |I|,

ie. the run time is O(|I|^k), where k is a constant.

The Class NPBearbeiten

Certificate Relation

Polynomially decidable

We say R is polynomially decidable if there is a polynomial-time algorithm that checks, given a pair v1 , v2 of objects, whether (v1 , v2 ) ∈ R.

Polynomially balanced

We say R is polynomially balanced if (v1 , v2 ) ∈ R implies |v2 | ≤ |v1 |k for some fixed k ≥ 1.

Decision Problems + Optimization Problems

Binary Search can be used to reduce Optimization Problems to Decision Problems.

Model CheckingBearbeiten

IntroductionBearbeiten

==Basics of Model Checking

AbstractionBearbeiten

==Bounded Model Checking (= SAT-based Model Checking)