Back

Applied logic (2018/2019)

Lectures take place on odd Wednesday 9:15 - 11:00 in room 21/C-3.
This course is for Master students in Faculty of Electronics.

Materials and literature

  1. G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual
  2. M. Ben-Ari, Principles of the Spin Model Checker
  3. spinroot.com
  4. M. Ben-Ari, Mathematical Logic for Computer Science
  5. J. Cichoń, Wykład ze Wstępu do Matematyki (in Polish)

Final mark

There will be homeworks during the semester.
Each solution should be written by hand on a piece of paper (no pdf files!).

Homework 1 (deadline 3.04)

  1. (2 points) Write a sentence $(p\rightarrow q)\leftrightarrow r$ in CNF and DNF.
  2. (2 points) Using a resolution method check if $S=\{\overline{p}qr, p\overline{q}r, p\overline{q}\overline{r}, \overline{p}s\}$ is satisfiable. If yes, find a valuation $\pi$ such that $\forall \varphi\in S\; \pi(\varphi)=1$.
Results

Homework 2 (deadline 8.05)

  1. (2 points) Is it true that $\models_K \Box p\lor\neg\Diamond p$?
  2. (2 points) Prove that $R$ is a transitive relation on $X$ if and only if $(X,R)\models\Box p\rightarrow\Box\Box p$.
Results

Homework 3 (deadline 05.06)

  1. (2 points)Is it true that $\models_{LTL}(pUq)\rightarrow (p\lor q)$?
  2. (2 points) Let $\mathbb{A}=(\{s,t,u\},\Sigma,\{s\},\delta,\{u,t\}),$ where $\Sigma=\{0,1\}$ and $\delta $ is described by the following tabular:
    $S$ $\Sigma$ $\delta$
    $s$ $0$ $\{t\}$
    $s$ $1$ $\emptyset$
    $t$ $0$ $\{u\}$
    $t$ $1$ $\{u\}$
    $u$ $0$ $\{s,t\}$
    $u$ $1$ $\{s\}$
    Find $L(\mathbb{A})$ and $L_{\omega}(\mathbb{A})$.
-->

Marks

0-4 2.0
5 3.0
6-7 3.5
8 4.0
9-10 4.5
11-12 5.0
Activity during classes can increase mark up to +1.0.

Final test

The final mark is equal to 40%C+60%T, where C is a mark of classes, T - a mark of final test. To get a positive mark ($\ge 3.0$) both C and T must be positive.

Schedule

  1. Propositional logic
    1. Propositional variables, connectives, sentences, valuations
    2. Tautologies, satisfiable sentences
    3. Conjunctive normal form CNF
    4. Resolvent, resolution method
    5. Connection to $P=NP$ problem
  2. Modal logic
    1. Kripke's frame, Kripke's model
    2. Language ${\mathcal L}_{ML}(\mathcal P)$, special connectives $\Box, \Diamond$
    3. Semantics
    4. Modal tautologies
    5. Kripke's frames with reflexive, transitive and symetric relation
    6. Logic $S4,\; S5$
    7. Theory of a class of Kripke's frames
    8. Tautologies of $S4$
  3. Linear Temporal Logic
    1. Language ${\mathcal L}_{LTL}(\mathcal P)$, new connectives $\bigcirc,\ U$
    2. Semantics
    3. Tautologies of $LTL$
    4. Examples of $LTL$-sentences describing special behaviour of given system
    5. Wolper's example
  4. Finite automatons
    1. Deterministic and nondeterministic finite automatons
    2. Regular expressions and regular languages
  5. Buchi automatons
    1. NBA and DBA
    2. $\omega$-regular languages
  6. LTL and Buchi automatons
    1. Automaton $A_\varphi$ which accepts $mod(\varphi)=\{\pi:\ \pi,0\models\varphi\}$
    2. Examples
    3. General construction
    4. Discrete system of states
    5. Spin
    -->

Back