- Propositional logic, Boolean algebra, propositional resolution, SAT-2KNF
- Predicate logic, unification, predicate logic resolution
- Temporal Logics (LTL, CTL)
- Deterministic finite automata, definition and construction
- Regular languages, closure properties, word problem, string matching
- Nondeterministic automata:
Rabin-Scott transformation of nondeterministic into deterministic automata - Epsilon automata, minimization of automata,
elimination of e-edges, uniqueness of the minimal automaton (modulo renaming of states) - Myhill-Nerode Theorem:
Correctness of the minimization procedure, equivalence classes of strings induced by automata
- Pumping Lemma for regular languages:
provision of a tool which, in some cases, can be used to show that a finite automaton principally cannot be expressive enough to solve a word problem for some given language
- Regular expressions vs. finite automata:
Equivalence of formalisms, systematic transformation of representations, reductions
- Pushdown automata and context-free grammars:
Definition of pushdown automata, definition of context-free grammars, derivations, parse trees, ambiguities, pumping lemma for context-free grammars, transformation of formalisms (from pushdown automata to context-free grammars and back)
- Chomsky normal form
- CYK algorithm for deciding the word problem for context-free grammrs
- Deterministic pushdown automata
- Deterministic vs. nondeterministic pushdown automata:
Application for parsing, LL(k) or LR(k) grammars and parsers vs. deterministic pushdown automata, compiler compiler
- Regular grammars
- Outlook: Turing machines and linear bounded automata vs general and context-sensitive grammars
- Chomsky hierarchy
- Mealy- and Moore automata:
Automata with output (w/o accepting states), infinite state sequences, automata networks - Omega automata: Automata for infinite input words, Büchi automata, representation of state transition systems, verification w.r.t. temporal logic specifications (in particular LTL)
- LTL safety conditions and model checking with Büchi automata, relationships between automata and logic
- Fixed points, propositional mu-calculus
- Characterization of regular languages by monadic second-order logic (MSO)
|