|CompCompl||Computational Complexity||Papadimitriou||1||Nein / (eventuell Stefan fragen)||☐|
|CompComplModern||Computational Complexity - A Modern Approach||Arora, Barak||1||☐|
|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||☐|
|AdvFormVer||Advanced Formal Verification||Drechsler||3||☐|
Computation and ComputabilityBearbeiten
Question + infinite set of possible instances. Decision problem: yes/no answer.
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.
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;
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.
If is a decidable decision problem and is the complement of , then is also decidable.
Proof: Invert outputs of complement decidable program.
If P is a decision problem, is the complement of P, and both P and 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 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:
- there is a program Π that decides P, and Π is such that
- 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
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.
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.
Other Important Complexity ClassesBearbeiten
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
==Basics of Model Checking
==Bounded Model Checking (= SAT-based Model Checking)