diff options
| author | Erin van der Veen | 2018-04-08 16:29:24 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-04-08 16:29:24 +0200 |
| commit | ebf17c432de4177bf4acd36c2beb6e7bdc5003ef (patch) | |
| tree | cb05bb6b4312e615bb17d173ba2a82fb768c47c5 /Assignment1 | |
| parent | Introduction 1 and 2 (diff) | |
Syntax of LTLP
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/assignment1.tex | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index a7a2eea..78e049c 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -3,6 +3,9 @@ \usepackage[backend=biber,natbib]{biblatex} \bibliography{library} +\usepackage{amsthm} +\newtheorem{definition}{Definition} + \title{Model Checking} \subtitle{Assignment 1} \author{Camil Staps \and Erin van der Veen} @@ -30,9 +33,15 @@ but $\Omega(2^n)$ in LTL. Markey achieves this proof by providing an formula that is in exactly this class. \subsection{Syntax and Semantics} -%TODO: Provide formal syntax +% Provide formal syntax %TODO: Provide intuitive semantics %TODO: Provide formal semantics +Let $P$ be the set of atomic propositions $\{p, q, r, \dots\}$, +then the syntax of LTLP is defined as: +\begin{definition} + Given $\phi, \psi \in LTLP$, then: +$$LTLP ::= \neg\phi \mid \phi \vee \psi \mid \phi \mathbf{U} \psi \mid \mathbf{X} \phi \mid \phi \mathbf{S} \psi \mid \mathbf{X}^{-1} \phi \mid p \mid q$$ +\end{definition} \subsection{LTL and LTL-Past} %TODO: Consider/Analyse differences between LTL and LTL-Past |