# HG changeset patch # User Eugen Sawin # Date 1310502053 -7200 # Node ID 2309d82bb4a7b1fad78c0aa43ff1ee7f83f87987 # Parent 84007e289e19286ac58b956f10d82e45a83499d3 Discussion draft. diff -r 84007e289e19 -r 2309d82bb4a7 paper/comments.txt --- a/paper/comments.txt Tue Jul 12 17:54:45 2011 +0200 +++ b/paper/comments.txt Tue Jul 12 22:20:53 2011 +0200 @@ -7,6 +7,7 @@ - no introduction to omega-regular languages - short introduction to LTL semantics - no automata complement construction +- on-the-fly construction is too short - error on page 5: there must not be a state g in G along r - error on page 12: V : S -> 2^P diff -r 84007e289e19 -r 2309d82bb4a7 paper/src/paper.tex --- a/paper/src/paper.tex Tue Jul 12 17:54:45 2011 +0200 +++ b/paper/src/paper.tex Tue Jul 12 22:20:53 2011 +0200 @@ -102,7 +102,7 @@ The fifth section interweaves automata theory and modal logics for the formalisation of the automata constructions, i.e., we construct automata depicting the program design and the specified properties. Based on this constructions, we apply the methods presented in the model checking section. The last section is a short excursion into the practical considerations of automated verification. For a successful application of automated verification, we consider ways of reducing the complexity of the automata-theoretic approach. -The formal frame of this text is mostly based on Madhavan Mukund's \cite{ref:ltl&büchi} and Moshe Y. Vardi's \cite{ref:handbook} work. We will conclude this paper with a discussion of \cite{ref:ltl&büchi}. +The formal frame of this text is mostly based on Madhavan Mukund's \cite{ref:ltl&büchi} and Moshe Y. Vardi's \cite{ref:handbook} work. We conclude this paper with a discussion of \cite{ref:ltl&büchi}. \section{$\omega$-regular languages} For the formalisation of non-terminating, reactive systems, we need to get familiar with the concept of infinity. When a system is persistently active, the conceptual model of its input becomes an infinite structure, and likewise the description of its computational path. We want to settle this infinite structures within a formal corset. @@ -198,7 +198,7 @@ \section{Linear temporal logic} Nothing escapes time, but time has successfully escaped its formalisation in computer science until the rise of the modal logics in the second half of the 20th century \cite{ref:handbook}. All arts and sciences interpret time in some way; where historians prefer the past tense, do science-fiction novels live in the future. Physics knows many time arrows, one of which constitutes the thermodynamic arrow of time, which happens to be the one we perceive by remembering the past and not the future. We compensate our inability to control the direction of time, by the use of rigorous language constructs when reasoning about temporal events. -When natural language fails in providing unambiguousness, we have to resort to formal languages. To handle time, we use \emph{propositional logic} as the base and extend it by some more or less modal connectives. There are two major temporal logics used in the specification of system properties, \emph{linear temporal logic (LTL)} and \emph{branching temporal logic (CTL - for Computation Tree Logic)}. Temporal logics are interpreted over computation paths; in LTL such a path depicts a linear sequence, where in CTL the path is a tree, with branching connectives. Throughout this text, we will restrict our attention to LTL. +When natural language fails in providing unambiguousness, we have to resort to formal languages. To handle discrete time, we use \emph{propositional logic} as the base and extend it by some more or less modal connectives. There are two major temporal logics used in the specification of system properties, \emph{linear temporal logic (LTL)} and \emph{branching temporal logic (CTL - for Computation Tree Logic)}. Temporal logics are interpreted over computation paths; in LTL such a path depicts a linear sequence, where in CTL the path is a tree, with branching connectives. Throughout this text, we will restrict our attention to LTL. \subsection{Syntax} Let $\Prop$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(\Prop)$ is $\Prop \cup \{\neg, \lor, \X, \U\}$. We define the $L_{LTL}(\Prop)$-\emph{formulae} $\varphi$ using following productions: @@ -497,6 +497,32 @@ \noindent The soundness and completeness proofs are provided in \cite{ref:ltl&büchi}; the equivalance of the partial automata and the specification automata as defined in \ref{sec:specification automata} follows from the proofs. \subsection{On-the-fly construction} +So. +\begin{algorithm} +\caption{expand} +\label{alg:expand} +\begin{algorithmic} +\REQUIRE $Node, NodeSet$ +\IF {$New(Node) = \emptyset$} + \IF {$\exists{N \in NodeSet}: Old(N) = Old(Node)$ and $Next(N) = Next(Node)$} + \STATE $Incoming(N) = Incoming(N) \cup Incoming(Node)$ + \ENDIF +\ELSE + \STATE $n \in New$ + \IF {$i+k\leq maxval$} + \STATE $i\gets i+k$ + \ENDIF +\ENDIF +\end{algorithmic} +\end{algorithm} + +\section*{Discussion} +Linear-Time Temporal Logic and B\"uchi Automata \cite{ref:ltl&büchi} is an in-depth introduction to automated verification. It delivers the core concepts of model checking in a readable way. The formal proofs are clean and absorbable. The introduction section provides a good overview of the structure of the text and the basic theory behind all concepts. + +However, the author does not make any efforts to deliver a motivation for the topic. From the beginning, the substance of the text resides within the world of model checking, without an external view on the practical applications and their significance. + +At some points, the definitions are either lacking formality or are inconsistent. It seemes like several concepts are introduced ad-hoc and without rigor. In an introductory text, such inaccuracies may lead to confusion and diminished confident in the reader's own understanding of the discussed topics. + \begin{thebibliography}{99}