diff options
| -rw-r--r-- | Assignment1/assignment1.tex | 9 | ||||
| -rw-r--r-- | Assignment1/exercises.tex | 25 | ||||
| -rw-r--r-- | Assignment1/syntax.tex | 29 |
3 files changed, 62 insertions, 1 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index b4ed04c..e40b064 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -54,8 +54,12 @@ \usepackage{parskip} \usepackage{cleveref} \usepackage{enumitem} +\usepackage{multicol} \usepackage{stackengine} \crefname{figure}{Figure}{Figures} +\crefname{xdefinition}{Definition}{Definitions} +\crefname{xexample}{Example}{Examples} +\crefname{xremark}{Remark}{Remarks} \usepackage[color]{changebar} \newif\ifchangebar\changebarfalse \let\oldcbend\cbend @@ -74,6 +78,11 @@ \DeclareMathOperator{\Sop}{\mathbf{S}} \DeclareMathOperator{\Pop}{\bigcirc^{--1}} +\newcommand{\wff}{\emph{wff}} % Well-formed formula +\newcommand{\wffn}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{0}}} % Pure present wff +\newcommand{\wfff}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$+$}}} % Pure future wff +\newcommand{\wffp}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$-$}}} % Pure past wff + \title{Model Checking} \subtitle{Assignment 1} \author{Camil Staps \and Erin van der Veen} diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex index 371dc0f..9126427 100644 --- a/Assignment1/exercises.tex +++ b/Assignment1/exercises.tex @@ -8,6 +8,31 @@ \camil \begin{exercise} + For the PLTL formulas over $AP=\{a,b\}$ given below, determine whether they are \wffn, \wffp, \wfff\ or neither. + + \begin{multicols}{2} + \begin{enumerate}[label=(\alph*)] + \item $\Xop a$. + \item $a \Sop b$. + \item $(\lnot (a \land b)) \land (\lnot (\lnot a \land \lnot b))$. + \item $a \Uop a$. + \item $a \land ((b \Uop a) \lor \lnot(b \Uop a))$. + \item $\text{false} \rightarrow (a \Uop b)$. + \end{enumerate} + \end{multicols} + + \begin{answer} + (a) \wfff; + (b) \wffp; + (c) \wffn; + (d) \wfff; + (e) neither; + (f) neither. + Note that the definition of the classes is syntactic, not semantic. + \end{answer} +\end{exercise} + +\begin{exercise} On page~\pageref{pltl:dual-modalities}, we discussed informally why the dual modalities $\lozenge^{-1}\square^{-1}\phi$ and $\square^{-1}\lozenge^{-1}\phi$ are both equivalent to \enquote{at the first moment in time, $\phi$}. Prove this formally, i.e.\ that for all infinite words $\sigma$ and $i\in\mathbb N$, \[ diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 6fc0002..833144b 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -13,6 +13,7 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2 and $\phi_1$ held ever after that moment up to and including the current moment. \begin{definition}[Syntax of PLTL] + \label{def:syntax} PLTL formulae over the set $AP$ of atomic propositions are formed according to the following grammar: \[ \phi @@ -31,10 +32,36 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2 \end{definition} \camil +We additionally define $\lor, \rightarrow, \leftrightarrow, \text{false}$ using this syntax as usual. + The precedence order of the operators borrowed from LTL remains the same. $\Pop$ binds equally strong as $\Xop$ and $\lnot$. $\Sop$ takes precedence over $\Uop$, and like $\Uop$ is right-associative. +In discourse, it can be helpful to distinguish different kinds of PLTL formulas. + +\begin{definition}[Well-formed PLTL formulas (following \citet{Gabbay1989})] + A well-formed PLTL formula (\wff) is any formula adhering to the syntax of \cref{def:syntax} (ignoring, for simplicity, parentheses). + Additionally, we define the classes + \wffn\ (pure present \wff), + \wfff\ (pure future \wff) and + \wffp\ (pure past \wff) inductively as the smallest classes conforming to the following rules: + \begin{itemize} + \item + Atomic propositions and $\text{true}$ are \wffn. + \item + If $\phi,\psi \in \wffn \cup \wfff$, then $\phi \Uop \psi, \Xop\phi \in \wfff$. + \item + If $\phi,\psi \in \wffn \cup \wffp$, then $\phi \Sop \psi, \Xop^{-1}\phi \in \wffp$. + \item + If $\phi,\psi \in W$, then $\lnot\phi, \phi\land\psi \in W$, for all $W \in \{\wffn,\wffp,\wfff\}$. + \qedhere + \end{itemize} +\end{definition} + +Note that the classes \wffn, \wffp\ and \wfff\ are mutually disjoint. +Furthermore, there are \wff\ which are neither, like $\Xop a \land \Xop^{-1} a$. + As with LTL, we can also derive additional operators in PLTL. They can be seen as counterparts of the derived LTL modalities $\square$ and $\lozenge$: $\square^{-1}$ (\enquote{was always}, since the beginning until now) and @@ -126,7 +153,7 @@ The reason that dual modalities in PLTL are less useful is that we still conside Thus, while with future modalities it is possible to look infinitely far in the future, it is not possible to look infinitely far in the past. %TODO: Give examples of semantics along the lines of subsection 5.1.1. -Before turning to the formal semantics in the next subsection, we provide some examples. +Before turning to the formal semantics in the next subsection, we provide some examples of PLTL formulae and their uses. \begin{example}[Properties for a Traffic Light] We return to the traffic light of Example 5.4. |