Brainscape's Knowledge GenomeTM

Browse over 1 million classes created by top students, professors, publishers, and experts.


See full index

IN.5021 Formal Methods > IN.5021 Formal Methods > Flashcards

IN.5021 Formal Methods Flashcards

1
Q

Hoare triple

A

{P} S {Q}
P = a precondition, assumed to be true before execution of S
S = a sequence of statements
Q = a postcondition, will be true after execution of S

indicate: if P is true, then executing S will make Q true

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

primed notation: x’

A

x’ refers to the value after the execution of a program and its unprimed notation x refers to its value before the program execution

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

primed notation: x’

A

x’ refers to the value after the execution of a program and its unprimed notation x refers to its value before the program execution

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

program annotation

A

a predicate, an assertion

it states what is assumed to be true when the program reaches that point of execution

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

partial correctness

A

a desired result is achieved

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

program verification

A

in general impossible to do

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

partial correctness

A

a desired result is achieved (after a loop has come to an end)

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

termination

A

when a loop definitely will come to an end

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

total correctness

A

= partial correctness + termination

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

partial correctness: (loop) invariant

A

a loop invariant is a logical formula that is true

  • before the loop
  • before each execution of the loop body
  • after each execution of the loop body
  • after the loop

-> you have to invent an invariant!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

(loop) variant

A
  • an integer-valued expression
  • value that can change over time
  • is decreased at least by 1 in each execution of the loop body
  • cannot go below 0
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
12
Q

invariant inv

A

an invariant is something you have to find, invent

  • true after initialization
  • precondition to the loop body
  • true after execution of loop body
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

interpretation I

A

is a truth-value assignment to propositional variables P, Q, …

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
14
Q

satisfiability

A

F is satisfiable iff notF is not valid

  • > there is some interpretation I that makes F true
  • > I makes notF false
  • > not all interpretations make notF true (because I doesn’t)
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
15
Q

validity

A

F is valid iff notF is not satisfiable

  • > all interpretations make F true
  • > no interpretation makes F not true (false)
  • > no interpretation makes notF true
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
16
Q

negation normal-form

A

if and only if negations appear only directly in front of variables, i.e. they appear only in literals, and the formulas contain only disjunctions and conjunctions

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
17
Q

domain and range

A

incl. negation normal form

cf. 2-Proposi…pdf slide 14

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
18
Q

disjunctive normal form

A

A formula F is in disjunctive normal-form, if and only if it is in negation normal-form and it is the disjunction (OR) of conjunctions (AND).

-> incl. negation normal form

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
19
Q

resolution

A

aims at deciding satisfiability

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
20
Q

deciding satisfiability

A
  • via truth table (but O(2^n) space)

- SAT algorithm (only O(n) space)

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
21
Q

SAT algorithm

A

capable of checking the satisifability of a formula

  • recursive
  • tries out truth table but sequentially
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
22
Q

busy beaver

A

just a TM that can write a sequence of 1’s on the tape

  • > when it stops: the output is the number of 1’s it wrote on the tape
  • > is non-computable because …
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
23
Q

busy beaver function

A

given a number n, what is the MAXIMAL output such a busy beaver can produce when the BB has n+1 states

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
24
Q

decision problem

A

TM only says “yes” or “no”

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
25
Q

turn computational problem into decision problem

A

by giving the TM two strings v and w and ask whether the TM on input v will produce output w

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
26
Q

language acceptance

A

about decidability

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
27
Q

language acceptance

A

about decidability

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
28
Q

recursively enumerable languages

A

languages that are accepted by Turing machines

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
29
Q

recursive language

A

like r.e. language but guaranteed to stop in a non-accepting state

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
30
Q

when is a problem decidable?

A

the languages that encode the problem must be recursive for the problem itself to be decidable

if language is r.e. then the TM might not stop for a given input w and then we would not know whether w is a solution to the problem or not or whether we had just not waited long enough

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
31
Q

intractable

A

(also called “NP-hard”)
is a problem to which an algorithm solving the
problem does exist, but it is so inefficient that it is considered as practically useless
i.e. it takes so much time for bigger instances of the problem that it’s useless
-> also called beyond-polynomial-time algorithms

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
32
Q

tractable

A
  • polynomial-time algorithms are perceived as tractable

- beyond-polynomial-time algorithms are perceived as intractable

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
33
Q

diagonalization language

A

no TM accepts it

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
34
Q

acceptance by a TM

A

such a language L is recursive

the TM always stops

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
35
Q

pseudo/partial algorithm

A

could run forever

–> for recursively enumerable languages

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
36
Q

reduction

A
  • a reduction is an algorithm for transforming one problem into another problem
  • a reduction from one problem to another may be used to show that the second problem is at least as difficult as the first
  • is a transformation from one input alphabet to another input alphabet such that this transformation must be computable
  • > there is a TM that always stops and does the transformation
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
37
Q

if the complement of a language L is not RE

A

then the language L is not recursive only RE

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
38
Q

L_u’s complement is not RE

A

by reduction from L_d

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
39
Q

partial algorithm vs algorithm

A

may run forever vs always stops

a partial algorithm = a strategy that may be successful or may not, if successful we can trust the outcome, otherwise we cannot because it may never say yes or no

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
40
Q

property of the RE languages

A

is just a set of RE languages (those that satisfy the property).
e.g. there is at least a word in the language that contains a symbol the digit 2

41
Q

property of the RE languages

A

is just a (sub-)set of RE languages (those that satisfy the property).

e. g. there is at least a word in the language that contains a symbol the digit 2
- if the property were false then it would be the empty set (no language will satisfy false)

42
Q

a language

A

a set of strings all of which are chosen from some E*, where E is a particular alphabet

43
Q

a recursively enumerable language

A

a language has a TM that accepts it

  • > the TM is a finite representation of that language
  • > that TM has the property that its encoding is just a string of 0’s and 1’s
  • > the encoding of TM (a single string) is a representation of the language (= a set of strings)
44
Q

decidability

A

tbd…

45
Q

TM

A

a R/RE language has a TM that accepts it

  • > the TM is a finite representation of that language
  • > that TM has the property that its encoding is just a string of 0’s and 1’s
  • > the encoding of TM (a single string) is a representation of the language (= a set of strings)
  • > a TM is a finite representation of something that is infinite (e.g. a TM that accepts all even numbers)
46
Q

a decidable property P

A

a property P is decidable iff the language L_p, which represents P, is a decidable language => if it is recursive

47
Q

Rice theorem

A

Every nontrivial property of the RE languages is undecidable

48
Q

an undecidable problem

A

a problem to which no algorithm solving the problem exists

49
Q

L_u

A

a RE language -> there is a partial algorithm (= a strategy that may be successful or may not, if successful we can trust the outcome, otherwise we cannot because it may never say yes or no)

50
Q

a “problem”

A

is about membership of a string in a language

in automata theory, a “problem” is the question of deciding whether a given string is a member of some particular language

=> anything we more colloquially call a “problem” can be expressed as membership in a language

51
Q

an intractable problem

A

a problem to which an algorithm solving the

problem does exist, but it is so inefficient that it is considered as practically useless

52
Q

an intractable problem

A

a problem to which an algorithm solving the

problem does exist, but it is so inefficient that it is considered as practically useless

53
Q

beyond-polynomial-time = intractable

A

in general, beyond-polynomial means “exponential”

but there are functions that are between the polynomials and exponential functions

54
Q

complexity classes

A

P and NP

55
Q

complexity class P

A

-> P is class of all problems aka all languages that are recursive s.t. the algorithm does not take more than polynomially many steps, that algorithm is represented by a deterministic TM

If for a problem P there exists a deterministic TM M such that M solves P (i.e. L(M) = P) in polynomial time, then we say that P is in complexity class P

56
Q

complexity class NP

A

-> NP is class of all problems that can be solved by non-deterministic TM in polynomial time (remember: there is this unbounded parallelism!)

If for a problem P there exists a non-deterministic TM M such that M solves P (i.e. L(M) = P) in polynomial time, then we say that P is in complexity class NP

57
Q

P is contained in NP but not vice versa, why?

A

-> there are problems in NP that cannot be solved by a deterministic TM in polynomial time

58
Q

unbounded parallelism

A

possible in NTM

59
Q

is there a witness in NP but not in P?

A

no ones knows.
But if NP != P then I can characterize problems that would have to be outside of P
-> describe most difficult problems in NP -> then, are those problems outside of P?
we know that P is a subset of NP (just by definition of those two classes)

60
Q

polynomial-time reductions

A

sl, 63 in 4-pdf

P1 reduces to P2 in polynomial-time

61
Q

running time of algorithms

A

is equivalent to running time of deterministic TM

algorithms as we have them in CS are those that are represented by deterministic TMs

62
Q

NP-hard

A
  • a problem H is NP-hard when every problem L in NP can be reduced in polynomial time to H
  • for a problem Q it is proved that any other problems of NP can be reduced to Q, but the first line (slide 67) is not yet proved (i.e. that Q is in NP), then such a problem Q is called NP-hard
63
Q

NP-complete problem

A

a decision problem is NP-complete when it is both in NP and NP-hard

believed to be intractable
-> there does not exist a polynomial time algorithm that solves the NP-complete problems

64
Q

satisfiability problem for propositional logic

A

is an NP-complete problem!

65
Q

SAT problem

A
  • SAT is an NP-complete problem
  • > can be solved by an NTM in polynomial time (all truth assignments are tested in parallel)
  • > it is NP-hard meaning that all problems in NP can be reduced in polynomial time to this problem SAT
66
Q

NP problem characterized

A

an NP problem increases in difficulty in a non-polynomial way (-> NP) / the rate at which a problem gets harder defines it as a truly difficult problem
e.g. factorization

67
Q

nature of computation

A

we’re talking about how the difficulty scales up as you make the problem bigger and bigger

68
Q

polynomial time

A

An algorithm is said to be of polynomial time if its running time is upper bounded by a polynomial expression in the size of the input for the algorithm, i.e., T(n) = O(n^k) for some constant k.

Problems for which a deterministic polynomial time algorithm exists belong to the complexity class P.

Polynomial time is a synonym for “tractable”, “feasible”, “efficient”, or “fast”.

E.g. maximum matchings in graphs;

69
Q

The complexity class NP

A

The complexity class NP is a set of problems whose solutions can be verified in polynomial time, even if finding those solutions takes — as far as anyone knows — exponential time

70
Q

partial correctness and invariant

A
  • A meaningful invariant will make the postcondition of the loop true
  • partical correctness: When, after the loop has come to an end, a desired result is achieved (desired result: the post condition)
71
Q

termination and (loop) variant

A
  • (loop) variant is an expression that is decreased at least by 1 in each execution of the loop body
  • cannot go below 0
  • by means of the variant and 1 Hoare triple termination of a program is proved
72
Q

computable vs decidable

A

a problem is computable if and only if its corresponding decision problem is decidable

73
Q

decidable problem

A

a TM can answer yes or no to a given input.

So decidability has to do with “language acceptance”

74
Q

a language encodes a problem

A

…

75
Q

problem vs language

A

a problem is really a language

76
Q

direction of reduction

A

the only way to prove a new problem P2 to be undecidable is to reduce a known problem P1 to P2 (and not reduce P2 to some known undecidable problem P1!).
That way, we prove the statement “if P2 is decidable, then P1 is decidable”. The contrapositive of that statement is “if P1 is undecidable, then P2 is undecidable”. Since we know that P1 is undecidable, we can deduce that P2 is undecidable.

If we are given a problem P1, for which we can show that if it were decidable, an already known undecidable problem P2 would be decidable, then P1 must be undecidable. We say we reduced P2 to P1.

e.g. We do so by reducing SAT first to CSAT and then CSAT to 3SAT.

77
Q

contrapositive

A

every if-then statement has an equivalent form that in some circumstances is easier to prove.
The contrapositive of the statement “if H then C” is “if not C then not H”
-> a statement and its contrapositive are either both true or both false, so we can prove either to prove the other

78
Q

system state

A

the purpose of a state is to remember the relevant portion of the system’s history

79
Q

automata

A

study the limits of computation

80
Q

decidability

decidable

A

what can a computer do at all?

the problems that can be solved by a computer

81
Q

intractability

tractable

A

what can a computer do efficiently?
the problems that can be solved by a computer using no more time than some polynomial growing function of the size of the input.

82
Q

deductive proofs

A

p. 6

83
Q

proof by contradiction

A

you assume that the conclusion is false
- then use that assumption, together with parts of the hypothesis, to prove the opposite of one of the given statements of the hypothesis. Then show that it is impossible for the conclusion to be false. The only possibility that remains is for the conclusion to be true whenever the hypothesis is true. That is, the theorem is true.

84
Q

a formal proof

A

the purpose is to convince someone about the correctness of a strategy you are using in your code. If it is convincing, then it is enough; if it fails to convince the “consumer” of the proof, then the proof has left out too much.

85
Q

prove if-else

prove while-loop

A

2 Hoare triples

3+1 Hoare triples

86
Q

complexity theory

A

in this field, we are interested in proving lower bounds on the complexity of certain problems.

87
Q

NP-hard vs NP-complete?

A

A decision problem H is NP-hard if there is a polynomial-time reduction from an NP-complete problem G to H.
As any problem L in NP reduces in polynomial time to G, L reduces in turn to H in polynomial time

88
Q

P: polynomial time
NP: nondeterministic polynomial time

A

P: quickly solvable problems (e.g. multiplication, sorting)
NP: quickly checkable problems (includes search problems such as graph coloring, TSP, scheduling), solved with searching (hard)

89
Q

is P1 more difficult than P2?

A

problem P1 is more difficult than a problem P2 when P1 cannot be solved in polynomial time whereas P2 can

90
Q

P1 <

A

P1 reduces to P2 in polynomial time (P2 is the known problem here)

91
Q

BCP

A

Boolean Constraint Propagation

92
Q

Idea of Cook’s theorem

A

Construct the propositional formula (phi) that is satisfiable IFF the truth values assigned to its propositional values correspond to a correct
encoding of an accepting computation of NTM M, i.e. some input w is in P

93
Q

polynomial algorithm

A

e.g. n, n log n, n^2, n^10

An algorithm is said to be of polynomial time if its running time is upper bounded by a polynomial expression in the size of the input for the algorithm, i.e., T(n) = O(n^k) for some constant k
->  Problems for which a deterministic polynomial time algorithm exists belong to the complexity class P
94
Q

a problem is NP-hard…

A

some problems L are so hard that although condition (2) (=every language in NP reduces to L in polynomial time) is proven, condition (1) is not: that L is in NP.
If so, we call L NP-hard.
L is very likely to require exponential time or worse.

NP-hard =~ intractable

95
Q

what does “undecidable” mean?

A

if a language L is not recursive, then we call the problem expressed by that language “undecidable”

a decidable "problem" is really membership of a string in a language L which is recursive, i.e. there exists a TM (informally "an algorithm") s.t. if w is in L, M accepts and if w is not in L, then M halts without accepting. 
So problem (=language) L is "decidable" if it is a recursive language, and it is called "undecidable" if it is not a recursive language (e.g. a RE language whose TM may not halt and give us a sense that "the problem is not solved")
RE languages (e.g. L_u) have some TM, non-RE languages (e.g. L_d) have no TM
96
Q

a problem that is in RE but not recursive

a language that is not in RE

A

L_u

L_d (no TM accepts it)

97
Q

recursive and RE languages

A

the languages accepted by Turing machines are called recursively enumerable (RE), and the subset of RE languages that are accepted by a TM that always halts are called recursive

98
Q

FOL is undecidable

A

proof by reduction from L_u to validity of FOL

99
Q

FOL can represent a TM

A

yes
logical view vs operational view
-> machines and logic are very frequently the same

IN.5021 Formal Methods (1 decks)

Brainscape helps you reach your goals faster, through stronger study habits.
© 2024 Bold Learning Solutions. Terms and Conditions