[f01853]: thys / TLA / document / root.tex Maximize Restore History

Download this file

root.tex    85 lines (64 with data), 3.0 kB

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
\documentclass[11pt,a4paper]{article}
%\usepackage{amssymb, amsfonts}
%\usepackage{hyperref}
\usepackage{isabelle,isabellesym}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage[greek,english]{babel}
%option greek for \<euro>
%option english (default language) for \<guillemotleft>, \<guillemotright>
%\usepackage[latin1]{inputenc}
%for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
%\<threesuperior>, \<threequarters>, \<degree>
\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
\usepackage{textcomp}
%for \<cent>, \<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
\newcommand{\tlastar}{TLA$^{*}$}
\begin{document}
\title{A Definitional Encoding of TLA in Isabelle/HOL}
\author{Gudmund Grov \& Stephan Merz}
\maketitle
\begin{abstract}
We mechanise the logic \tlastar{} \cite{Merz99}, an extension of Lamport's Temporal Logic of Actions (TLA) \cite{Lamport94} for specifying
and reasoning about concurrent and reactive systems. Aiming at a framework for mechanising the verification
of TLA (or \tlastar{}) specifications, this contribution reuses some elements from a
previous axiomatic encoding of TLA in Isabelle/HOL by the second author \cite{Merz98}, which has been part of the
Isabelle distribution. In contrast to that previous work, we give here a shallow, definitional
embedding, with the following highlights:
\begin{itemize}
\item a theory of infinite sequences, including a formalisation of the concepts of stuttering invariance central to TLA and TLA*;
\item a definition of the semantics of TLA*, which extends TLA by a mutually-recursive definition of formulas and pre-formulas, generalising TLA action formulas;
\item a substantial set of derived proof rules, including the TLA* axioms and Lamport's proof rules for system verification;
\item a set of examples illustrating the usage of Isabelle/TLA* for reasoning about systems.
\end{itemize}
Note that this work is unrelated to the ongoing development of a proof system for the specification language TLA+,
which includes an encoding of TLA+ as a new Isabelle object logic \cite{chaudhuri:tlaps}.
A previous version of this embedding has been used heavily in the work described in \cite{Grov09}.
\end{abstract}
\tableofcontents
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
% generated text of all theories
\input{session}
% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: