\documentclass{article}
\usepackage{graphics}
\usepackage{fancyhdr}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[topbottom,singlearrows]{../logicsym}
\usepackage{multicol}
\usepackage{alltt}


\newcommand{\coursenumber}{081}
\newcommand{\coursetitle}{Computability and Logic}

\topmargin  18pt  	% 27pt
\headheight 12pt  	% 12pt
\headsep    35pt 	% 45pt
\textheight 8.0in
\textwidth  6.2in

\oddsidemargin   22pt      % Left margin on odd-numbered pages.
\evensidemargin  22pt      % Left margin on even-numbered pages.
\marginparwidth  72pt       % Width of marginal notes.
\marginparsep    11pt      % Horizontal space between outer margin and 
                           % marginal note

\pagestyle{fancy}
\lhead{CSCI \coursenumber}
\chead{}
\rhead{\semester}
\lfoot{}
\cfoot{\thepage}
\rfoot{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\newcommand{\semester}[0]{
     \ifnum\month>7{Fall}\fi
     \ifnum\month<8{Spring}\fi\  \number\year
}

\begin{document}

\begin{center}{\Large Homework 9}\\ \vspace{1 ex} Due midnight,
Thursday, 4/9/2015 \end{center}

\vspace{2 ex}
\noindent

Please submit your homework solutions online at  
\texttt{http://www.dci.pomona.edu/tools-bin/cs081upload.php}.  If you 
have more than one file to be turned in, please put it in a folder 
and zip it up before turning it in.

\vspace{2 ex}

\begin{enumerate}

    \item (5 points) \textbf{LTL}
    
    Problem 3.2.3 from H \& R page 246.  You need only show the 
    equivalence for the first formula.  Notice that we don't have 
    proof rules, so you must show the equivalence using our 
    definition of semantics.  I.e., two formulas are equivalent iff 
    the formulas are true of exactly the same models and paths.
    
    \item (10) \textbf{Semantics of LTL}
    
    Problem 3.3.1ab from H \& R page 247.
    
    \item (20) \textbf{Model checking}
    
    We can express four desirable properties of concurrent systems in
    CTL as follows:
    
    \begin{description}
	\item[Safety]  $\phi_{1} = AG \Not(c_{1} \And c_{2})$.
	
	\item[Liveness] $\phi_{2} = AG(t_{1} \Implies AF\, c_{1})$
	
	\item[Non-blocking] $\phi_{3} = AG(n_{1} \Implies EX\, t_{1})$
	
	\item[No strict sequencing] $\phi_{4} = EF(c_{1} \And 
	E[c_{1}\ U (\Not c_{1} \And E[\Not c_{2}\ U\ c_{1}])])$
    \end{description}
    
    Apply the labeling algorithm to check each of $\phi_{1}$,
    $\phi_{2}$ and $\phi_{4}$ in the mutual exclusion model in Figure
    3.7 (page 188) of H \& R.  (Note that we did $\phi_{3}$ in class!)
    
    \item (5 points) \textbf{Understanding TM's}
    
    Problem 17.1b from Rich page 407.
     
    \item (10) \textbf{Computing with TMs}
    
    Problem 17.3c from Rich page 408.
        
\end{enumerate}

\end{document}
