際際滷

際際滷Share a Scribd company logo
A Logical Revolution
Moshe Y. Vardi
Rice University
Logic in Computer Science
During the past 鍖fty years there has been extensive, continuous,
and growing interaction between logic and computer science. In
many respects, logic provides computer science with both a unifying
foundational framework and a tool for modeling computational
systems. In fact, logic has been called the calculus of computer
science. The argument is that logic plays a fundamental role in
computer science, similar to that played by calculus in the physical
sciences and traditional engineering disciplines. Indeed, logic plays
an important role in areas of computer science as disparate as
machine architecture, computer-aided design, programming languages,
databases, arti鍖cial intelligence, algorithms, and computability and
complexity.
1
Why on Earth?
Basic Question: What on earth does an obscure, old intellectual discipline
have to do with the youngest intellectual discipline?
M. Davis (1988): In鍖uences of Mathematical Logic on Computer Science:
When I was a student, even the topologists regarded mathematical logicians
as living in outer space. Today the connections between logic and computers
are a matter of engineering practice at every level of computer organization.
Question: Why on earth?
2
The Fundamental Method of Physical Sciences
The basic method of physical science:
 Construct a mathematical model for physical reality.
 Analyze mathematical model.
 Compare analysis results with physical reality.
Basic Question: What is a mathematical model?
3
What is The Language of Mathematics?
Friedrich Ludwig Gottlob Frege, Begri鍖sschrift, 1879: a universal
mathematical language  鍖rst-order logic  logicism
 Objects, e.g., 2
 Predicates (relationships), e.g., 2 < 3
 Operations (functions), e.g., 2 + 3
 Boolean operations, e.g., and (), or (), implies ()
 Quanti鍖ers, e.g., for all (), exists ()
4
Example: Aristotles Syllogisms
 All men are mortal
 For all x, if x is a man, then x is mortal
 (x)(Man(x)  Mortal(x))
5
First-Order Logic
A formalism for specifying properties of mathematical structures, such as
graphs, partial orders, groups, rings, 鍖elds, . . .
Mathematical Structure: [Tarski, 1933]
A = (D, R1, . . . , Rk, f1, . . . , fl),
 D is a non-empty set  universe
 Ri is an m-ary relation on A, for some m (that is, Ri  Am
)
 fj is an n-ary function on A, for some n (that is, fi : An
 D)
6
Examples
 Graph: G = (V, E)
 V : nodes
 E  V 2
: edges
 (x)(y)E(x, y)
 Group: G = (V, 揃)
 V : elements
 揃 : V 2
 V : product
 (x)(y)x 揃 y = y 揃 x
7
First-Order Logic on Graphs
Syntax:
 First-order variables: x, y, z, . . . (range over nodes)
 Atomic formulas: E(x, y), x = y
 Formulas: Atomic Formulas + Boolean Connectives + First-Order
Quanti鍖ers x, x, . . .
8
Examples:
 node x has at least two distinct neighbors
(y)(z)(測(y = z)  E(x, y)  E(x, z))
Concept: x is free in the above formula, which expresses a property of
nodes. Truth de鍖nition requires a binding 留. G |=留 (x)
 each node has at least two distinct neighbors
(x)(y)(z)(測(y = z)  E(x, y)  E(x, z))
Concept: The above is a sentence, that is, a formula with no free
variables; it expresses a property of graphs. G |= 
9
Russells Letter
A letter from Russell to Frege, June 16, 1902:
I 鍖nd myself in agreement with you in all essentials . . . I 鍖nd in your
work discussions, distinctions, and de鍖nitions that one seeks in vain
in the work of other logicians . . . There is just one point where I have
encountered a di鍖culty.
Appendix to Freges 1903 volume:
There is nothing worse that can happen to a scientist than to have
the foundation collapse just as the work is 鍖nished. I have been placed
in this position by a letter from Mr. Bertrand Russell.
10
Hilberts Program
Hilberts Program (1922-1930): Formalize mathematics and establish
that:
 Mathematics is consistent: a mathematical statement and its negation
cannot ever both be proved.
 Mathematics is complete: all true mathematical statements can be
proved.
 Mathematics is decidable: there is a mechanical way to determine
whether a given mathematical statement is true or false.
11
The Demise of Hilberts Program
 G即odel (1930-3):
 Incompleteness of ordinary arithmetic  There is no systematic way of
resolving all mathematical questions.
 Impossibility of proving consistency of mathematics
G即odel (1930): This sentence is not provable.
 Church and Turing (1936):
Unsolvability of 鍖rst-order logic:
 The set of valid 鍖rst-order sentences is not computable.
12
Entscheidungsproblem
Entscheidungsproblem (The Decision Problem) [Hilbert-Ackermann,
1928]: Decide if a given 鍖rst-order sentence is valid (dually, satis鍖able).
Church-Turing Theorem, 1936: The Decision Problem is unsolvable.
Turing, 1936:
 De鍖ned computability in terms of Turing machines (TMs)
 Proved that the termination problem for TMs is unsolvable (this
machine terminates i鍖 it does not terminate)
 Reduced termination to Entscheidungsproblem.
13
Mathematical Logic  1936
Logic as Foundations of Mathematics:
 Incomplete (example: Continuum Hypothesis)
 Cannot prove its own consistency
 Unsolvable decision problem
Can we get some positive results?
 Focus on special cases!
14
The Fragment-Classi鍖cation Project
Idea: Identify decidable quanti鍖cational fragments of 鍖rst-order logic 
(1915-1983)
 Bernays-Sch即on鍖nkel Class (

)
 Ackermann Class (

)
 G即odel Class (w/o =) (

)
Outcome: Very weak classes! What good is 鍖rst-order logic?
15
Logic of Integer Addition
Integer Addition:
 Domain: N (natural numbers)
 Dyadic predicate: 
 Addition function: +
 y = 2x: y = x + x
 x = 0: (y)(x  y)
 x = 1: x = 0  (y)(y = 0  x  y)
 y = x + 1: (z)(z = 1  y = x + z)
Bottom Line: Theory of Integer Addition can express Integer
Programming (integer inequalities) and much more.
16
Presburger Arithmetics
Moj卒zesz Presburger, 1929:
 Sound and complete axiomatization of integer addition
 Decidability: There exists an algorithm that decides whether a given
鍖rst-order sentence in integer-addition theory is true or false.
 Decidability is shown using quanti鍖er elimination, supplemented by
reasoning about arithmetical congruences.
 Decidability can also be shown using automata-theoretic techniques.
17
Complexity of Presburger Arithmetics
Complexity Bounds:
 Oppen, 1978: TIME(222poly
) upper bound
 Fischer&Rabin, 1974: TIME(22lin
) lower bound
Rabin, 1974: Theoretical Impediments to Arti鍖cial Intelligence: the
complexity results point to a need for a careful examination of the goals
and methods in AI.
18
Monadic Logic
Monadic Class: First-order logic with monadic predicates  captures
syllogisms.
 (x)P(x), (x)(P(x)  Q(x)) |= (x)Q(x)
[L即owenheim, 1915]: The Monadic Class is
decidable.
 Proof: Bounded-model property  if a sentence
is satis鍖able, it is satis鍖able in a structure of
bounded size.
 Proof technique: quanti鍖er elimination.
19
Finite Words  Nondeterministic Finite Automata, I
A = (裡, S, S0, , F)
 Alphabet: 裡
 States: S
 Initial states: S0  S
 Nondeterministic transition function:
 : S  裡  2S
 Accepting states: F  S
20
Finite Words  Nondeterministic Finite Automata, II
Input word: a0, a1, . . . , an1
Run: s0, s1, . . . , sn
 s0  S0
 si+1  (si, ai) for i  0
Acceptance: sn  F
Recognition: L(A)  words accepted by A.
Example: -

6
蔵 臓
0
1-

0


6
蔵 臓
1
 ends with 1s
Fact: NFAs de鍖ne the class Reg of regular languages.
21
Logic of Finite Words
View 鍖nite word w = a0, . . . , an1 over alphabet
裡 as a mathematical structure:
 Domain: 0, . . . , n  1
 Dyadic predicate: 
 Monadic predicates: {Pa : a  裡}
Monadic Second-Order Logic (MSO):
 Monadic atomic formulas: Pa(x) (a  裡)
 Dyadic atomic formulas: x  y
 Set quanti鍖ers: P, P
Example: (x)((y)(測(x  y))  P1(x))  last letter is 1.
22
Automata and Logic
Theorem [B即uchi, Elgot, Trakhtenbrot, 1957-8
(independently)]: MSO  NFA
 Both MSO and NFA de鍖ne the class Reg.
Proof: E鍖ective
 From NFA to MSO (A  A)
 From MSO to NFA (  A)
23
NFA Nonemptiness
Nonemptiness: L(A) = 
Nonemptiness Problem: Decide if given A is nonempty.
Directed Graph GA = (S, E) of NFA A =
(裡, S, S0, , F):
 Nodes: S
 Edges: E = {(s, t) : t  (s, a) for some a 
裡}
Lemma: A is nonempty i鍖 there is a path in GA from S0 to F.
 Decidable in time linear in size of A, using breadth-鍖rst search or
depth-鍖rst search.
24
MSO Satis鍖ability  Finite Words
Satis鍖ability: models() = 
Satis鍖ability Problem: Decide if given  is satis鍖able.
Lemma:  is satis鍖able i鍖 A is nonnempty.
Corollary: MSO satis鍖ability is decidable.
 Translate  to A.
 Check nonemptiness of A.
25
Complexity Barrier
Computational Complexity:
 Naive Upper Bound: Nonelementary Growth
2揃揃揃2n
(tower of height O(n))
 Lower Bound [Stockmeyer, 1974]: Satis鍖ability of FO over 鍖nite words
is nonelementary (no bounded-height tower).
26
Nonelementary Growth
 22
= 4
 223
= 256
 2224
= 4, 294, 967, 296
 22225
 10109
27
Booles Symbolic Logic
Booles insight: Aristotles syllogisms are about classes of objects, which
can be treated algebraically.
If an adjective, as good, is employed as a term of description, let us
represent by a letter, as y, all things to which the description good
is applicable, i.e., all good things, or the class of good things. Let
it further be agreed that by the combination xy shall be represented
that class of things to which the name or description represented by
x and y are simultaneously applicable. Thus, if x alone stands for
white things and y for sheep, let xy stand for white sheep.
28
Boolean Satis鍖ability
Boolean Satis鍖ability (SAT); Given a Boolean expression, using and
() or, () and not (測), is there a satisfying solution (an assignment
of 0s and 1s to the variables that makes the expression equal 1)?
Example:
(測x1  x2  x3)  (測x2  測x3  x4)  (x3  x1  x4)
Solution: x1 = 0, x2 = 0, x3 = 1, x4 = 1
29
Complexity of Boolean Reasoning
History:
 William Stanley Jevons, 1835-1882: I have given much attention,
therefore, to lessening both the manual and mental labour of the process,
and I shall describe several devices which may be adopted for saving trouble
and risk of mistake.
 Ernst Schr即oder, 1841-1902: Getting a handle on the consequences
of any premises, or at least the fastest method for obtaining these
consequences, seems to me to be one of the noblest, if not the ultimate
goal of mathematics and logic.
 1950-60s: Perebor: Futile e鍖ort to show hardness of search
problems.
 Cook, 1971, Levin, 1973: Boolean Satis鍖ability is NP-complete.
30
NP-Completeness
Complexity Class NP: problems where solutions can be checked in
polynomial time.
 Factoring numbers
 Hamiltonian Cycle
Signi鍖cance: Tens of thousands of optimization problems are in NP!!!
 CAD, 鍖ight scheduling, chip layout, protein folding, . . .
NP-complete: Hardest problems in NP.
 If one NP-complete problem can be solved in polynomial time, then
all NP-complete problems can be solved in polynomial time.
31
Is P = NP?
S. Aaronson, MIT: If P = NP, then the world would be a profoundly
di鍖erent place than we usually assume it to be. There would be no special
value in creative leaps, no fundamental gap between solving a problem and
recognizing the solution once it is found. Everyone who could appreciate
a symphony would be Mozart; everyone who could follow a step-by-step
argument would be Gauss.
Common Belief: Boolean SAT cannot be solved in polynomial time.
32
Program Veri鍖cation
The Dream  Hoare, 1969: When the correctness of a program, its
compiler, and the hardware of the computer have all been established with
mathematical certainty, it will be possible to place great reliance on the
results of the program.
The Nightmare  De Millo, Lipton, and Perlis, 1979: We believe that . . .
program veri鍖cation is bound to fail. We cant see how its going to be able
to a鍖ect anyones con鍖dence about programs.
 Basic Argument: Acceptance of proof is a social process!
33
Logic in Computer Science: c. 1980
Status: Logic in CS is not too useful!
 Unsolvable termination problem.
 First-order logic is undecidable.
 The decidable fragments are either too weak or too intractable.
 Even Boolean logic is intractable.
 Program veri鍖cation is hopeless.
34
Post 1980: From Irrelevance to Relevance
A Logical Revolution:
 Relational databases
 Boolean reasoning
 Model checking
 Termination checking
 . . .
35
From Model Theory to Relational Databases
 A sentence  is either true or false on a given graph G. In particular,
sentences specify classes of graphs: models() = {G : G |= }
Model Theory: Logic provides a metatheory for mathematical modeling.
 E.F. Codd, 1970: Formulas (x1, . . . , xk) de鍖ne queries:
(G) = { 留(x1), . . . , 留(xk) : G |=留 (x1, . . . , xk)}
Example: (y)(z)(測(y = z)  E(x, y)  E(x, z))  List nodes that
have at least two distinct neighbors
Turing Awards: Codd, 1981, Stonebraker, 2014
Relational Databases: $30B+ industry
36
Relational Databases
Codds Two Fundamental Ideas:
 Tables are relations: a row in a table is just a tuple in a relation; order
of rows/tuples does not matter!
 Formulas are queries: they speci鍖ed the what rather then the how 
declarative programming!
Reduction to Practice:
 System R, IBM, 1976
 Ingress, UC Berkeley, 1976
 Oracle, Relational Software, 1979
 DB2, IBM, 1982
37
Algorithmic Problems in First-Order Logic
Satis鍖ability Problem: Given a 鍖rst-order formula , is there a graph G
and binding 留, such that G |=留 ?
Truth-Evaluation Problem: Given a 鍖rst-order formula (x1, . . . , xk), a
鍖nite graph G, and a binding 留, does G |=留 (x1, . . . , xk)?
Contrast:
 Satis鍖ability is undecidable [Church, Turing 1936]
 Truth evaluation, which is query evaluation, is decidable.
38
Algorithmic Boolean Reasoning: Early History
 Newell, Shaw, and Simon, 1955: Logic Theorist
 Davis and Putnam, 1958: Computational Methods in The
Propositional calculus, unpublished report to the NSA
 Davis and Putnam, JACM 1960: A Computing procedure for
quanti鍖cation theory
 Davis, Logemman, and Loveland, CACM 1962: A machine program
for theorem proving
DPLL Method: Propositional Satis鍖ability Test
 Convert formula to conjunctive normal form (CNF)
 Backtracking search for satisfying truth assignment
 Unit-clause preference
39
Modern SAT Solving
CDCL = con鍖ict-driven clause learning
 Backjumping
 Smart unit-clause preference
 Con鍖ict-driven clause learning
 Smart choice heuristic (brainiac vs speed demon)
 Restarts
Key Tools: GRASP, 1996; Cha鍖, 2001
Current capacity: millions of variables
40
S. A. Seshia 1
Some Experience with SAT Solving
Sanjit A. Seshia
Speed-up of 2012 solver over other solvers
1
10
100
1,000
Solver
Speed-up(logscale)
41
Applications of SAT Solving in SW Engineering
Leonardo De Moura+Nikolaj Bj即orner, 2012: applications of Z3 at Microsoft
 Symbolic execution
 Model checking
 Static analysis
 Model-based design
 . . .
42
The Temporal Logic of Programs
Crux: Need to specify ongoing behavior rather than input/output relation!
Temporal logic to the rescue [Pnueli, 1977]:
 Linear temporal logic (LTL) as a logic for the
speci鍖cation of non-terminating programs
 Model checking via reduction to MSO
But: nonelementary complexity!
43
Examples
 always not (CS1 and CS2): safety
 always (Request implies eventually Grant): liveness
 always (Request implies (Request until Grant)): liveness
44
Model Checking
Algorithmic veri鍖cation [Clarke  Emerson,
1981, Queille  Sifakis, 1982]: Model checking
programs of size m wrt CTL formulas of size n
can be done in time mn.
Linear-Time Response [Lichtenstein  Pnueli, 1985]: Model checking
programs of size m wrt LTL formulas of size n can be done in time m2O(n)
(tableau heuristics).
Seemingly:
 Automata: Nonelementary
 Tableaux: exponential
45
Back to Automata
Exponential-Compilation Theorem [V.  Wolper, 19831986]: Given an
LTL formula  of size n, one can construct an automaton A of size 2O(n)
such that a trace  satis鍖es  if and only if  is accepted by A.
Automata-Theoretic Algorithms:
1. LTL Satis鍖ability:
 is satis鍖able i鍖 L(A) =  (PSPACE)
2. LTL Model Checking:
M |=  i鍖 L(M  A測) =  (m2O(n)
)
Today: Widespread industrial usage
 Industrial Languages: PSL, SVA (IEEE standards)
46
Solving the Unsolvable
B. Cook, A. Podelski, and A. Rybalchenko, 2011:in contrast to popular
belief, proving termination is not always impossible
 The Terminator tool can prove termination or divergence of many
Microsoft programs.
 Tool is not guaranteed to terminate!
Explanation:
 Most real-life programs, if they terminate, do so for rather simple reasons.
 Programmers almost never conceive of very deep and sophisticated
reasons for termination.
47
Logic: from failure to success
Key Lessons:
 Algorithms
 Heuristics
 Experimentation
 Tools and systems
Key Insight: Do not be scared of worst-case complexity.
 It barks, but it does not necessarily bite!
48
Limits of Logic
Blaise Pascal, 1623-1662:
 Two excesses: to exclude reason, to admit nothing but reason.
 The heart has its reasons, which reason knows not.
49

More Related Content

Logicrevo15

  • 1. A Logical Revolution Moshe Y. Vardi Rice University
  • 2. Logic in Computer Science During the past 鍖fty years there has been extensive, continuous, and growing interaction between logic and computer science. In many respects, logic provides computer science with both a unifying foundational framework and a tool for modeling computational systems. In fact, logic has been called the calculus of computer science. The argument is that logic plays a fundamental role in computer science, similar to that played by calculus in the physical sciences and traditional engineering disciplines. Indeed, logic plays an important role in areas of computer science as disparate as machine architecture, computer-aided design, programming languages, databases, arti鍖cial intelligence, algorithms, and computability and complexity. 1
  • 3. Why on Earth? Basic Question: What on earth does an obscure, old intellectual discipline have to do with the youngest intellectual discipline? M. Davis (1988): In鍖uences of Mathematical Logic on Computer Science: When I was a student, even the topologists regarded mathematical logicians as living in outer space. Today the connections between logic and computers are a matter of engineering practice at every level of computer organization. Question: Why on earth? 2
  • 4. The Fundamental Method of Physical Sciences The basic method of physical science: Construct a mathematical model for physical reality. Analyze mathematical model. Compare analysis results with physical reality. Basic Question: What is a mathematical model? 3
  • 5. What is The Language of Mathematics? Friedrich Ludwig Gottlob Frege, Begri鍖sschrift, 1879: a universal mathematical language 鍖rst-order logic logicism Objects, e.g., 2 Predicates (relationships), e.g., 2 < 3 Operations (functions), e.g., 2 + 3 Boolean operations, e.g., and (), or (), implies () Quanti鍖ers, e.g., for all (), exists () 4
  • 6. Example: Aristotles Syllogisms All men are mortal For all x, if x is a man, then x is mortal (x)(Man(x) Mortal(x)) 5
  • 7. First-Order Logic A formalism for specifying properties of mathematical structures, such as graphs, partial orders, groups, rings, 鍖elds, . . . Mathematical Structure: [Tarski, 1933] A = (D, R1, . . . , Rk, f1, . . . , fl), D is a non-empty set universe Ri is an m-ary relation on A, for some m (that is, Ri Am ) fj is an n-ary function on A, for some n (that is, fi : An D) 6
  • 8. Examples Graph: G = (V, E) V : nodes E V 2 : edges (x)(y)E(x, y) Group: G = (V, 揃) V : elements 揃 : V 2 V : product (x)(y)x 揃 y = y 揃 x 7
  • 9. First-Order Logic on Graphs Syntax: First-order variables: x, y, z, . . . (range over nodes) Atomic formulas: E(x, y), x = y Formulas: Atomic Formulas + Boolean Connectives + First-Order Quanti鍖ers x, x, . . . 8
  • 10. Examples: node x has at least two distinct neighbors (y)(z)(測(y = z) E(x, y) E(x, z)) Concept: x is free in the above formula, which expresses a property of nodes. Truth de鍖nition requires a binding 留. G |=留 (x) each node has at least two distinct neighbors (x)(y)(z)(測(y = z) E(x, y) E(x, z)) Concept: The above is a sentence, that is, a formula with no free variables; it expresses a property of graphs. G |= 9
  • 11. Russells Letter A letter from Russell to Frege, June 16, 1902: I 鍖nd myself in agreement with you in all essentials . . . I 鍖nd in your work discussions, distinctions, and de鍖nitions that one seeks in vain in the work of other logicians . . . There is just one point where I have encountered a di鍖culty. Appendix to Freges 1903 volume: There is nothing worse that can happen to a scientist than to have the foundation collapse just as the work is 鍖nished. I have been placed in this position by a letter from Mr. Bertrand Russell. 10
  • 12. Hilberts Program Hilberts Program (1922-1930): Formalize mathematics and establish that: Mathematics is consistent: a mathematical statement and its negation cannot ever both be proved. Mathematics is complete: all true mathematical statements can be proved. Mathematics is decidable: there is a mechanical way to determine whether a given mathematical statement is true or false. 11
  • 13. The Demise of Hilberts Program G即odel (1930-3): Incompleteness of ordinary arithmetic There is no systematic way of resolving all mathematical questions. Impossibility of proving consistency of mathematics G即odel (1930): This sentence is not provable. Church and Turing (1936): Unsolvability of 鍖rst-order logic: The set of valid 鍖rst-order sentences is not computable. 12
  • 14. Entscheidungsproblem Entscheidungsproblem (The Decision Problem) [Hilbert-Ackermann, 1928]: Decide if a given 鍖rst-order sentence is valid (dually, satis鍖able). Church-Turing Theorem, 1936: The Decision Problem is unsolvable. Turing, 1936: De鍖ned computability in terms of Turing machines (TMs) Proved that the termination problem for TMs is unsolvable (this machine terminates i鍖 it does not terminate) Reduced termination to Entscheidungsproblem. 13
  • 15. Mathematical Logic 1936 Logic as Foundations of Mathematics: Incomplete (example: Continuum Hypothesis) Cannot prove its own consistency Unsolvable decision problem Can we get some positive results? Focus on special cases! 14
  • 16. The Fragment-Classi鍖cation Project Idea: Identify decidable quanti鍖cational fragments of 鍖rst-order logic (1915-1983) Bernays-Sch即on鍖nkel Class ( ) Ackermann Class ( ) G即odel Class (w/o =) ( ) Outcome: Very weak classes! What good is 鍖rst-order logic? 15
  • 17. Logic of Integer Addition Integer Addition: Domain: N (natural numbers) Dyadic predicate: Addition function: + y = 2x: y = x + x x = 0: (y)(x y) x = 1: x = 0 (y)(y = 0 x y) y = x + 1: (z)(z = 1 y = x + z) Bottom Line: Theory of Integer Addition can express Integer Programming (integer inequalities) and much more. 16
  • 18. Presburger Arithmetics Moj卒zesz Presburger, 1929: Sound and complete axiomatization of integer addition Decidability: There exists an algorithm that decides whether a given 鍖rst-order sentence in integer-addition theory is true or false. Decidability is shown using quanti鍖er elimination, supplemented by reasoning about arithmetical congruences. Decidability can also be shown using automata-theoretic techniques. 17
  • 19. Complexity of Presburger Arithmetics Complexity Bounds: Oppen, 1978: TIME(222poly ) upper bound Fischer&Rabin, 1974: TIME(22lin ) lower bound Rabin, 1974: Theoretical Impediments to Arti鍖cial Intelligence: the complexity results point to a need for a careful examination of the goals and methods in AI. 18
  • 20. Monadic Logic Monadic Class: First-order logic with monadic predicates captures syllogisms. (x)P(x), (x)(P(x) Q(x)) |= (x)Q(x) [L即owenheim, 1915]: The Monadic Class is decidable. Proof: Bounded-model property if a sentence is satis鍖able, it is satis鍖able in a structure of bounded size. Proof technique: quanti鍖er elimination. 19
  • 21. Finite Words Nondeterministic Finite Automata, I A = (裡, S, S0, , F) Alphabet: 裡 States: S Initial states: S0 S Nondeterministic transition function: : S 裡 2S Accepting states: F S 20
  • 22. Finite Words Nondeterministic Finite Automata, II Input word: a0, a1, . . . , an1 Run: s0, s1, . . . , sn s0 S0 si+1 (si, ai) for i 0 Acceptance: sn F Recognition: L(A) words accepted by A. Example: - 6 蔵 臓 0 1- 0 6 蔵 臓 1 ends with 1s Fact: NFAs de鍖ne the class Reg of regular languages. 21
  • 23. Logic of Finite Words View 鍖nite word w = a0, . . . , an1 over alphabet 裡 as a mathematical structure: Domain: 0, . . . , n 1 Dyadic predicate: Monadic predicates: {Pa : a 裡} Monadic Second-Order Logic (MSO): Monadic atomic formulas: Pa(x) (a 裡) Dyadic atomic formulas: x y Set quanti鍖ers: P, P Example: (x)((y)(測(x y)) P1(x)) last letter is 1. 22
  • 24. Automata and Logic Theorem [B即uchi, Elgot, Trakhtenbrot, 1957-8 (independently)]: MSO NFA Both MSO and NFA de鍖ne the class Reg. Proof: E鍖ective From NFA to MSO (A A) From MSO to NFA ( A) 23
  • 25. NFA Nonemptiness Nonemptiness: L(A) = Nonemptiness Problem: Decide if given A is nonempty. Directed Graph GA = (S, E) of NFA A = (裡, S, S0, , F): Nodes: S Edges: E = {(s, t) : t (s, a) for some a 裡} Lemma: A is nonempty i鍖 there is a path in GA from S0 to F. Decidable in time linear in size of A, using breadth-鍖rst search or depth-鍖rst search. 24
  • 26. MSO Satis鍖ability Finite Words Satis鍖ability: models() = Satis鍖ability Problem: Decide if given is satis鍖able. Lemma: is satis鍖able i鍖 A is nonnempty. Corollary: MSO satis鍖ability is decidable. Translate to A. Check nonemptiness of A. 25
  • 27. Complexity Barrier Computational Complexity: Naive Upper Bound: Nonelementary Growth 2揃揃揃2n (tower of height O(n)) Lower Bound [Stockmeyer, 1974]: Satis鍖ability of FO over 鍖nite words is nonelementary (no bounded-height tower). 26
  • 28. Nonelementary Growth 22 = 4 223 = 256 2224 = 4, 294, 967, 296 22225 10109 27
  • 29. Booles Symbolic Logic Booles insight: Aristotles syllogisms are about classes of objects, which can be treated algebraically. If an adjective, as good, is employed as a term of description, let us represent by a letter, as y, all things to which the description good is applicable, i.e., all good things, or the class of good things. Let it further be agreed that by the combination xy shall be represented that class of things to which the name or description represented by x and y are simultaneously applicable. Thus, if x alone stands for white things and y for sheep, let xy stand for white sheep. 28
  • 30. Boolean Satis鍖ability Boolean Satis鍖ability (SAT); Given a Boolean expression, using and () or, () and not (測), is there a satisfying solution (an assignment of 0s and 1s to the variables that makes the expression equal 1)? Example: (測x1 x2 x3) (測x2 測x3 x4) (x3 x1 x4) Solution: x1 = 0, x2 = 0, x3 = 1, x4 = 1 29
  • 31. Complexity of Boolean Reasoning History: William Stanley Jevons, 1835-1882: I have given much attention, therefore, to lessening both the manual and mental labour of the process, and I shall describe several devices which may be adopted for saving trouble and risk of mistake. Ernst Schr即oder, 1841-1902: Getting a handle on the consequences of any premises, or at least the fastest method for obtaining these consequences, seems to me to be one of the noblest, if not the ultimate goal of mathematics and logic. 1950-60s: Perebor: Futile e鍖ort to show hardness of search problems. Cook, 1971, Levin, 1973: Boolean Satis鍖ability is NP-complete. 30
  • 32. NP-Completeness Complexity Class NP: problems where solutions can be checked in polynomial time. Factoring numbers Hamiltonian Cycle Signi鍖cance: Tens of thousands of optimization problems are in NP!!! CAD, 鍖ight scheduling, chip layout, protein folding, . . . NP-complete: Hardest problems in NP. If one NP-complete problem can be solved in polynomial time, then all NP-complete problems can be solved in polynomial time. 31
  • 33. Is P = NP? S. Aaronson, MIT: If P = NP, then the world would be a profoundly di鍖erent place than we usually assume it to be. There would be no special value in creative leaps, no fundamental gap between solving a problem and recognizing the solution once it is found. Everyone who could appreciate a symphony would be Mozart; everyone who could follow a step-by-step argument would be Gauss. Common Belief: Boolean SAT cannot be solved in polynomial time. 32
  • 34. Program Veri鍖cation The Dream Hoare, 1969: When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program. The Nightmare De Millo, Lipton, and Perlis, 1979: We believe that . . . program veri鍖cation is bound to fail. We cant see how its going to be able to a鍖ect anyones con鍖dence about programs. Basic Argument: Acceptance of proof is a social process! 33
  • 35. Logic in Computer Science: c. 1980 Status: Logic in CS is not too useful! Unsolvable termination problem. First-order logic is undecidable. The decidable fragments are either too weak or too intractable. Even Boolean logic is intractable. Program veri鍖cation is hopeless. 34
  • 36. Post 1980: From Irrelevance to Relevance A Logical Revolution: Relational databases Boolean reasoning Model checking Termination checking . . . 35
  • 37. From Model Theory to Relational Databases A sentence is either true or false on a given graph G. In particular, sentences specify classes of graphs: models() = {G : G |= } Model Theory: Logic provides a metatheory for mathematical modeling. E.F. Codd, 1970: Formulas (x1, . . . , xk) de鍖ne queries: (G) = { 留(x1), . . . , 留(xk) : G |=留 (x1, . . . , xk)} Example: (y)(z)(測(y = z) E(x, y) E(x, z)) List nodes that have at least two distinct neighbors Turing Awards: Codd, 1981, Stonebraker, 2014 Relational Databases: $30B+ industry 36
  • 38. Relational Databases Codds Two Fundamental Ideas: Tables are relations: a row in a table is just a tuple in a relation; order of rows/tuples does not matter! Formulas are queries: they speci鍖ed the what rather then the how declarative programming! Reduction to Practice: System R, IBM, 1976 Ingress, UC Berkeley, 1976 Oracle, Relational Software, 1979 DB2, IBM, 1982 37
  • 39. Algorithmic Problems in First-Order Logic Satis鍖ability Problem: Given a 鍖rst-order formula , is there a graph G and binding 留, such that G |=留 ? Truth-Evaluation Problem: Given a 鍖rst-order formula (x1, . . . , xk), a 鍖nite graph G, and a binding 留, does G |=留 (x1, . . . , xk)? Contrast: Satis鍖ability is undecidable [Church, Turing 1936] Truth evaluation, which is query evaluation, is decidable. 38
  • 40. Algorithmic Boolean Reasoning: Early History Newell, Shaw, and Simon, 1955: Logic Theorist Davis and Putnam, 1958: Computational Methods in The Propositional calculus, unpublished report to the NSA Davis and Putnam, JACM 1960: A Computing procedure for quanti鍖cation theory Davis, Logemman, and Loveland, CACM 1962: A machine program for theorem proving DPLL Method: Propositional Satis鍖ability Test Convert formula to conjunctive normal form (CNF) Backtracking search for satisfying truth assignment Unit-clause preference 39
  • 41. Modern SAT Solving CDCL = con鍖ict-driven clause learning Backjumping Smart unit-clause preference Con鍖ict-driven clause learning Smart choice heuristic (brainiac vs speed demon) Restarts Key Tools: GRASP, 1996; Cha鍖, 2001 Current capacity: millions of variables 40
  • 42. S. A. Seshia 1 Some Experience with SAT Solving Sanjit A. Seshia Speed-up of 2012 solver over other solvers 1 10 100 1,000 Solver Speed-up(logscale) 41
  • 43. Applications of SAT Solving in SW Engineering Leonardo De Moura+Nikolaj Bj即orner, 2012: applications of Z3 at Microsoft Symbolic execution Model checking Static analysis Model-based design . . . 42
  • 44. The Temporal Logic of Programs Crux: Need to specify ongoing behavior rather than input/output relation! Temporal logic to the rescue [Pnueli, 1977]: Linear temporal logic (LTL) as a logic for the speci鍖cation of non-terminating programs Model checking via reduction to MSO But: nonelementary complexity! 43
  • 45. Examples always not (CS1 and CS2): safety always (Request implies eventually Grant): liveness always (Request implies (Request until Grant)): liveness 44
  • 46. Model Checking Algorithmic veri鍖cation [Clarke Emerson, 1981, Queille Sifakis, 1982]: Model checking programs of size m wrt CTL formulas of size n can be done in time mn. Linear-Time Response [Lichtenstein Pnueli, 1985]: Model checking programs of size m wrt LTL formulas of size n can be done in time m2O(n) (tableau heuristics). Seemingly: Automata: Nonelementary Tableaux: exponential 45
  • 47. Back to Automata Exponential-Compilation Theorem [V. Wolper, 19831986]: Given an LTL formula of size n, one can construct an automaton A of size 2O(n) such that a trace satis鍖es if and only if is accepted by A. Automata-Theoretic Algorithms: 1. LTL Satis鍖ability: is satis鍖able i鍖 L(A) = (PSPACE) 2. LTL Model Checking: M |= i鍖 L(M A測) = (m2O(n) ) Today: Widespread industrial usage Industrial Languages: PSL, SVA (IEEE standards) 46
  • 48. Solving the Unsolvable B. Cook, A. Podelski, and A. Rybalchenko, 2011:in contrast to popular belief, proving termination is not always impossible The Terminator tool can prove termination or divergence of many Microsoft programs. Tool is not guaranteed to terminate! Explanation: Most real-life programs, if they terminate, do so for rather simple reasons. Programmers almost never conceive of very deep and sophisticated reasons for termination. 47
  • 49. Logic: from failure to success Key Lessons: Algorithms Heuristics Experimentation Tools and systems Key Insight: Do not be scared of worst-case complexity. It barks, but it does not necessarily bite! 48
  • 50. Limits of Logic Blaise Pascal, 1623-1662: Two excesses: to exclude reason, to admit nothing but reason. The heart has its reasons, which reason knows not. 49