FANDOM


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
AdvFormVer Advanced Formal Verification Drechsler 3 PDF


Complexity TheoryBearbeiten

Computation and ComputabilityBearbeiten

DefinitionsBearbeiten

Problem

Question + infinite set of possible instances.
Decision problem: yes/no answer.

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.

Proof: Contradiction.

Halting ProblemBearbeiten

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.

ReductionsBearbeiten

NP-CompletenessBearbeiten

Other Important Complexity ClassesBearbeiten

Turing MachinesBearbeiten

SATBearbeiten

Preparatory ConceptsBearbeiten

Techniques of Modern SAT-SolversBearbeiten

Recap: First-Order Logic and TheoriesBearbeiten

Decision Procedure for Equality LogicBearbeiten

Equality Logic and Uninterpreted FunctionsBearbeiten

Formal Specification and VerificationBearbeiten

WTFBearbeiten

Model CheckingBearbeiten

IntroductionBearbeiten

==Basics of Model Checking

Program ModelingBearbeiten

AbstractionBearbeiten

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

Temporal LogicBearbeiten

Störung durch Adblocker erkannt!


Wikia ist eine gebührenfreie Seite, die sich durch Werbung finanziert. Benutzer, die Adblocker einsetzen, haben eine modifizierte Ansicht der Seite.

Wikia ist nicht verfügbar, wenn du weitere Modifikationen in dem Adblocker-Programm gemacht hast. Wenn du sie entfernst, dann wird die Seite ohne Probleme geladen.

Auch bei FANDOM

Zufälliges Wiki