1: \documentclass[11pt]{article} 

2: %\documentclass[10pt,twocolumn]{article} 

3: %\usepackage{latex8}

4: %\usepackage{times}

5: \usepackage{a4,fullpage}

6: \usepackage{times}

7: \usepackage{url}

8: \usepackage{epsfig}

9: \usepackage{amssymb}

10: %\newtheorem{definition}{Definition}

11: \newtheorem{note}{Note}

12: \newtheorem{mfproposition}{Proposition}

13: %\newtheorem{example}[lemma]{Example}

14: \usepackage{bbm}

15: \usepackage{amstext}

16: \usepackage{color}

17: \usepackage{xspace}

18: %

19: \usepackage{amsfonts}

20: \usepackage{amssymb}

21: \usepackage{graphicx}

22: %\usepackage{algo}

23: \usepackage{accents}

24: \usepackage{scalefnt}

25: %

26: \DeclareRobustCommand\bfsf{\normalfont\bfseries\sf\boldmath}

27: %

28: \newcommand*{\bffotlx}{\hbox{\bfsf FOTLX}}

29: %\newcommand*{\fotl}{\ensuremath{\mathrm{FOTL}}\xspace}

30: \newcommand*{\fotlx}{\textsf{FOTLX}\xspace}

31: \newcommand{\gb}{\mathfrak{b}}

32: %

33: %% \newcommand*{\nb}[1]{$|$\marginpar{\parbox{1cm}{\hspace{0pt}\tiny #1}}}

34: \newcommand*{\FF}{\mathbb{F}}

35: \newcommand*{\lstart}{\hbox{\bf start}}

36: \newcommand*{\ltrue}{\hbox{\bf true}}

37: \newcommand*{\lfalse}{\hbox{\bf false}}

38: \newcommand*{\imp}{\Rightarrow}

39: \newcommand*{\xor}{\otimes}

40: \newcommand*{\plus}{\ensuremath{+}}

41: \newcommand*{\minus}{\ensuremath{-}}

42: \DeclareRobustCommand\bfsc{\normalfont\bfseries\scshape\boldmath}

43: \def\Until{\mbox{\(\mathcal U\)}}

44: \def\Unless{\mbox{\(\mathcal W\)}}

45: \newcommand{\const}{\ensuremath{\mathrm{const}}}

46: \newcommand{\next}{\!\raisebox{-.2ex}{ %possibly add a little space before

47:                         \mbox{\unitlength=0.9ex

48:                         \begin{picture}(2,2)

49:                         \linethickness{0.06ex}

50:                         \put(1,1){\circle{2}} % Draws circle with

51:                         \end{picture}}}       % diameter 2 at centre 1,1

52:                         \,}

53: %%%%%%%%%%%%%%%%

54: \newtheorem{thm}{Theorem}

55: \newtheorem{lem}[thm]{Lemma}

56: %% \newtheorem{example}{Example}

57: \newtheorem{cor}[thm]{Corollary}

58: \newtheorem{axiom}{Axiom}

59: \newtheorem{remark}{Remark}

60: %% \newtheorem{proposition}[thm]{Proposition}

61: 

62: \newenvironment{proofsketch}

63: {\par\vspace*{0.5ex}\noindent\rm {\bf Proof (sketch):} }%

64:          {{\hfill\tiny$\Box$}\par\vspace*{1ex}}

65: \newenvironment{proof}{\par\vspace*{0.5ex}\noindent\rm {\bf Proof:} }%

66:          {{\hfill\tiny$\Box$}\par\vspace*{1ex}}

67: 

68: \DeclareRobustCommand\bfsc{\normalfont\bfseries\scshape\boldmath}

69: \def\sturn{\mathit{turn_s}}

70: \def\tturn{\mathit{turn_t}}                   

71: \def\agree{\mathit{agree}}

72: \def\lland{\,\land\,}

73: \def\bland{\ \land\ }

74: \def\llor{\,\lor\,}

75: %

76: \fboxsep=0.5em

77: \newtheorem{lemma}{Lemma}

78: \newtheorem{theorem}[lemma]{Theorem}

79: \newtheorem{corollary}[lemma]{Corollary}

80: \newtheorem{proposition}[lemma]{Proposition}

81: \newtheorem{mnote}{Note}

82: \newtheorem{slproposition}[lemma]{Proposition}

83: \newtheorem{sldefinition}{Definition}

84: \newtheorem{definition}{Definition}

85: \newtheorem{example}{Example}

86: 

87: \def\endmark{\hskip 2em\begin{picture}(8,10)

88: \put(0,0){$\Box$}

89: \put(2,0){\rule{1.9mm}{0.3mm}}

90: \put(6.5,0){\rule{0.3mm}{1.9mm}}

91: \end{picture}

92: \par}

93: \def\proof{\trivlist \item[\hskip \labelsep{\bf Proof\ }]}

94: \def\endproof{\null\hfill\endmark\endtrivlist}

95: 

96: %\newenvironment{proof}{

97: %    \emph{Proof}.}{

98: %    \hfill $\Box${\vspace{4mm}}

99: 

100: %}

101: 

102: %%\newcommand{\mydef}[2]{\textbf{\textit{#1}}\index{#2}}

103: %\newcommand{\xone}[2]{{#1_{1},\ldots,#1_{#2}}}

104: \newcommand{\setof}[1]{{\{#1\}}}

105: %\newcommand{\eqref}[1]{(\ref{#1})}

106: %\newcommand{\biglpar}{\bigl(}

107: %\newcommand{\bigrpar}{\bigr)}

108: 

109: 

110: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

111: %

112: %

113: %   Logical notation

114: %

115: %

116: 

117: %\newcommand{\imply}{\supset}

118: %\newcommand{\implies}{\supset}

119: \newcommand{\orl}{\vee}

120: \newcommand{\bigorl}{\bigvee}

121: \newcommand{\bigandl}{\bigwedge}

122: \newcommand{\andl}{\wedge}

123: \newcommand{\notl}{\neg}

124: \newcommand{\entail}{\Longrightarrow}

125: 

126: \newcommand{\iffl}{\equiv}

127: \newcommand{\Subst}[1]{[#1]}   % for substitutions

128: \newcommand{\subst}[2]{#1 \mapsto #2}   % for substitutions

129: 

130: \newcommand{\true}{\textsc{true}}

131: \newcommand{\false}{\textsc{false}}

132: 

133: 

134: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

135: %

136: %

137: %

138: %                           Local notation

139: %

140: %

141: 

142: \newcommand{\voc}{\sigma}

143:                           % vocabulary

144: 

145: \newcommand{\FOLang}[1]{\protect\mathcal{L}(#1)}

146:                           % first-order language with vocabulary #1

147: 

148: \newcommand{\FO}{\mathrm{FO}}

149:                           % FO

150: 

151: \newcommand{\FOT}{\mathrm{FO^{T}}}

152:                           % FO over trees

153: 

154: \newcommand{\str}[1]{\protect\mathcal{S}(#1)}

155:                           % the set of finite structures for vocabulary #1

156: 

157: \newcommand{\sig}{\sigma}

158:                           % simplified vocabulary

159: 

160: \newcommand{\sigp}{\sig^\ast}

161:                           % extended simplified vocabulary

162: 

163: \newcommand{\lr}{(l\protect\textit{-}r)}

164:                           % lr- (terms)

165: 

166: \newcommand{\Ur}{\mathit{Ur}}

167: 

168: 

169: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

170: 

171: %   Temporal notations

172: 

173: \newcommand{\uP}{\ensuremath{\mathcal{U}}}

174: \newcommand{\tP}{\ensuremath{\mathcal{T}}}

175: \newcommand{\eP}{\ensuremath{\mathcal{E}}}

176: \newcommand{\sP}{\ensuremath{\mathcal{S}}}

177: \newcommand{\iP}{\ensuremath{\mathcal{I}}}

178: \newcommand{\pP}{\ensuremath{\mathcal{P}}}

179: \newcommand{\mU}{\ensuremath{\mathcal{U}}}

180: \newcommand{\mT}{\ensuremath{\mathcal{T}}}

181: \newcommand{\mS}{\ensuremath{\mathcal{S}}}

182: \newcommand{\mP}{\ensuremath{\mathcal{P}}}

183: \newcommand{\mQ}{\ensuremath{\mathcal{Q}}}

184: \newcommand{\mL}{\ensuremath{\mathcal{L}}}

185: \newcommand{\mA}{\ensuremath{\mathcal{A}}}

186: \newcommand{\mB}{\ensuremath{\mathcal{B}}}

187: \newcommand{\mC}{\ensuremath{\mathcal{C}}}

188: \newcommand{\mF}{\ensuremath{\mathcal{F}}}

189: \newcommand{\mG}{\ensuremath{\mathcal{G}}}

190: \newcommand{\mH}{\ensuremath{\mathcal{H}}}

191: \newcommand{\mM}{\ensuremath{\mathcal{M}}}

192: \newcommand{\mD}{\ensuremath{\mathcal{D}}}

193: \newcommand{\mR}{\ensuremath{\mathcal{R}}}

194: \newcommand{\gD}{\mathfrak{D}}

195: \newcommand{\gI}{\mathfrak{I}}

196: \newcommand{\mI}{\mathcal{I}}

197: \newcommand{\gM}{\mathfrak{M}}

198: \newcommand{\ga}{\mathfrak{a}}

199: \newcommand{\gma}{\models^{\mathfrak{a}}}

200: \newcommand{\gA}{\mathfrak{V}}

201: \newcommand{\gB}{\mathfrak{B}}

202: \newcommand{\gF}{\mathfrak{F}}

203: \newcommand{\gC}{\mathfrak{C}}

204: \newcommand{\gn}{\mathfrak{n}}

205: \newcommand{\gR}{\mathfrak{R}}

206: \newcommand{\gJ}{\mathfrak{J}}

207: 

208: \newcommand{\auf}{\left\langle}

209: \newcommand{\zu}{\right\rangle}

210: \newcommand{\bydef}{\rightleftharpoons}   % equal by definition

211: \newcommand{\Nat}{\mathbbm{N}}

212: \newcommand{\sometime}{\lozenge}

213: \newcommand{\sometimes}{\lozenge}

214: %\newcommand{\sometimes}{\Diamond}

215: \newcommand{\sometimep}{\blacklozenge}

216: 

217: \newcommand{\until}{\mathcal{U}}

218: 

219: \newcommand{\while}{\mathcal{W}}

220: %\newcommand{\unless}{\mathcal{W}}

221: 

222: %\newcommand{\next}{\bigcirc}

223: 

224: \newcommand{\since}{\mathcal{S}}

225: 

226: \newcommand{\union}{\cup}

227: 

228: \def\true{\hbox{\bf true}}

229: \def\false{\hbox{\bf false}}

230: \def\start{\hbox{\bf start}}

231: \def\IFF{\quad\hbox{\rm iff}\quad}

232: \newcommand{\wfQ}{\ensuremath{\mathit{waitforQ}}}

233: \newcommand{\wfL}{\ensuremath{\mathit{waitforL}}}

234: \newcommand{\wfphi}{\ensuremath{\mathit{waitfor\phi}}}

235: %\newcommand{\TProb}{\ensuremath{\;\mathcal{P}\;}}

236: \newcommand{\TProb}{\textsf{P}}

237: \newcommand{\TSpec}{\textsf{SP}}

238: \newcommand{\SNF}{SNF}

239: \newcommand{\implies}{\Rightarrow}

240: \newcommand{\EAAE}{\ensuremath{\exists^*\forall^2\exists^*}\xspace}

241: \newcommand{\AAE}{\ensuremath{\forall^2\exists^*}\xspace}

242: \newcommand{\TEAAE}{\ensuremath{T\exists^*\forall^2\exists^*}\xspace}

243: \newcommand*{\fotl}{\ensuremath{\mathsf{FOTL}}\xspace}

244: %% To be changed (probably):

245: \newcommand{\Grounded}{Derived\xspace}

246: \newcommand{\grounded}{derived\xspace}

247: % 

248: % Paper finalizing:

249: % Boris' comments:

250: % Choose one of the two:

251: \newcommand{\boris}[1]{{#1}\marginnote{}\xspace}

252: %\newcommand{\boris}[1]{\textcolor[gray]{0.3}{#1}\marginnote{\textcolor[gray]{0.5}{changed by Boris}}\xspace}

253: %\newcommand{\moreboris}[1]{\textcolor{blue}{#1}\xspace}

254: \newcommand{\moreboris}[1]{{#1}\xspace}

255: %

256: \newcommand{\ar}[1]{\ensuremath{\mathcal{AR}[#1]}}

257: \newcommand{\mgu}{\textrm{most general unifier\xspace}}

258: \newcommand{\LT}{\ensuremath{\mathrm{LT}}}

259: \newcommand{\Prepro}{\ensuremath{\mathrm{\mathbf{S}}}}

260: %

261: %\definecolor{darkblue}{rgb}{0.09766, 0.09766, 0.5375}

262: \newcommand*{\New}{\color{black}}

263: \newcommand*{\EndNew}{\color{black}}

264: \makeatletter

265: \newenvironment{descriptionlist}[1]%

266:         {\begin{list}{}{

267:               \setlength{\itemsep}{0pt}

268:                 \settowidth{\labelwidth}{#1}

269:                 \settowidth{\leftmargin}{#1\hspace{\labelsep}}}

270:         }{

271:         \end{list} }

272: \makeatother

273: 

274: \newcommand{\TRPpp}{\textbf{TRP\protect\raisebox{0.35ex}{\ensuremath{\scriptstyle{+}{+}}}}\xspace}

275: \newcommand{\Vampire}{\textbf{Vampire}\xspace}

276: \newcommand{\TRPppV}{\textbf{TRP\protect\raisebox{0.35ex}{\ensuremath{\scriptstyle{+}{+}\;}}V}\xspace}

277: 

278: \newcommand{\nb}[1]{$|$\marginpar{\raggedright\small #1}}

279: 

280: \def\until{\hbox{$\,\mathsf{U} \,$}}

281: \def\unless{\hbox{$\,\mathsf{W} \,$}}

282: \def\since{\hbox{$\,\cal S \,$}}

283: 

284: %\def\sometime{\mathord{\hbox{\Large$\mathchar"0\cmsy@7D$}}} % PS \diamondsuit

285: %							    % is too small

286: \newcommand{\always}{\raisebox{-.2ex}{

287: 			   \mbox{\unitlength=0.9ex

288: 			   \begin{picture}(2,2)

289: 			   \linethickness{0.06ex}

290: 			   \put(0,0){\line(1,0){2}}

291: 			   \put(0,2){\line(1,0){2}}

292: 			   \put(0,0){\line(0,1){2}}

293: 			   \put(2,0){\line(0,1){2}}

294: 			   \end{picture}}}

295: 		      \,}

296: 

297: \newcommand*{\Next}{\!\raisebox{-.2ex}{ %possibly add a little space before

298: 			\mbox{\unitlength=0.9ex%

299: 			\begin{picture}(2,2)%

300: 			\linethickness{0.06ex}%

301: 			\put(1,1){\circle{2}} % Draws circle with

302: 			\end{picture}}}       % diameter 2 at centre 1,1

303: 			\,}

304: 

305: 

306: 

307: 

308: \def\start{\hbox{\bf start}}

309: \def\IFF{\quad\hbox{\rm iff}\quad}

310: \let\prv=\vdash

311: \let\imp=\Rightarrow

312: %\let\imp=\implies

313: \def\lland{\,\land\,}

314: \def\llor{\,\lor\,}

315: \def\ltrue{\hbox{\rm\bf true}}

316: \def\lfalse{\hbox{\rm\bf false}}

317: \def\wff#1#2{\hbox{$\hbox{\sc wff}_{#1}^{#2}$}}

318: \def\ptlwff{\wff{p}{}}

319: 

320: 

321: \newcommand{\ran}[1]{\protect\mathit{ran}(#1)}  % range of substitution #1

322: \newcommand{\dom}[1]{\protect\mathit{dom}(#1)}  % domain of substitution #1

323: \newcommand{\var}[1]{\protect\mathit{var}(#1)}  % set of variables of #1

324: \newcommand{\free}[1]{\protect\mathit{free}(#1)} % set of free variables of #1

325: %\newcommand{\mgu}[1]{\protect\mathrm{mgu}(#1)}  % mgu of #1

326: \newcommand{\wmgu}[1]{\protect\mathrm{wmgu}(#1)}% weak mgu of #1

327: 

328: \newcommand{\ml}[1]{\ensuremath{\mathsf{#1}}}

329: \newcommand{\pltl}{\ml{PLTL}\xspace}

330: %\newcommand{\classOne}{\ensuremath{\mathcal{C}^1_{\mathit{ran}}}\xspace}

331: %\newcommand{\classTwo}{\ensuremath{\mathcal{C}^2_{\mathit{ran}}}\xspace}

332: \newcommand{\trp}{TRP\xspace}

333: \renewcommand{\TRPppV}{TeMP\xspace}

334: %%%%%%

335: % \title{Towards the Tractable Temporal Verification of Infinite-State

336: % Systems} 

337: \title{Efficient First-Order Temporal Logic for Infinite-State Systems}

338: %

339: \author{Clare Dixon\quad Michael Fisher\quad Boris Konev\quad Alexei 

340:   Lisitsa\\[1ex]

341: Department of Computer Science, University of Liverpool\\

342: Liverpool L69 3BX, United Kingdom\\[1ex]

343: {\normalsize\texttt{\{C.Dixon,$\;$M.Fisher,$\;$B.Konev,$\;$A.Lisitsa\}@csc.liv.ac.uk}}}

344: \date{  }

345: %

346: \begin{document}

347: \maketitle

348: %

349: \begin{abstract}

350: In this paper we consider the specification and verification of

351: infinite-state systems using temporal logic. In particular, we

352: describe parameterised systems using a new variety of first-order

353: temporal logic that is both powerful enough for this form of

354: specification and tractable enough for practical deductive

355: verification. Importantly, the power of the temporal language allows

356: us to describe (and verify) asynchronous systems, communication delays

357: and more complex properties such as liveness and fairness

358: properties. These aspects appear difficult for many other approaches

359: to infinite-state verification.

360: \end{abstract}

361: 

362: \section{Introduction}

363: %

364: First-order temporal logic (\fotl) has been shown to be a powerful

365: formalism for expressing sophisticated dynamic

366: properties. Unfortunately, this power also leads to strong

367: intractability. Recently, however, a fragment of \fotl{}, called

368: \emph{monodic} \fotl{}, has been investigated, both in terms of its

369: theoretical~\cite{HWZ00,Hodkinson:Packed} and

370: practical~\cite{DFK03:ToCL,KDDFH05:IC,HKRV04:IJCAR} properties.

371: Essentially, monodicity allows for one free variable in every temporal

372: formula. Although clearly restrictive, this fragment has been shown to

373: be useful in expressive description logics, infinite-state

374: verification, and spatio-temporal

375: logics~\cite{AFWZ02,SturmW02,Kontchakovetal02,GKKWZ03,FKL06:VISSAS}.

376: 

377: We here develop a new temporal logic, combining decidable fragments of

378: monodic \fotl{}~\cite{HWZ00} with recent developments in XOR temporal

379: logics~\cite{DFK07:IJCAI}, and apply this to the verification of

380: parameterised systems. We use a communicating finite state machine

381: model of computation, and can specify not only basic synchronous,

382: parameterised systems with instantaneous broadcast

383: communication~\cite{esparza99verification}, but the powerful temporal

384: language allows us also to specify asynchronously executing machines

385: and more sophisticated communication properties, such as delayed

386: delivery of messages. In addition, and in contrast to many other

387: approaches~\cite{maidl01unifying,Del03,AbdullaJRS06}, not only safety,

388: but also liveness and fairness properties, can be verified through

389: automatic deductive verification. Finally, in contrast to work on

390: regular model checking~\cite{AbdullaJNdS04} and constraint based

391: verification using counting abstraction~\cite{esparza99verification},

392: the logical approach is both complete and decidable.

393: 

394: The verification of concurrent systems often comes down to the

395: analysis of multiple finite-state automata, for example of the following

396: form. 

397: %

398: \begin{center}

399: \includegraphics[width=0.25\textwidth]{automaton-s1.eps}

400: \end{center}

401: %

402: In describing such automata, both automata-theoretic and logical

403: approaches may be used. While \emph{temporal logic}~\cite{emerson:90a}

404: provides a clear, concise and intuitive description of the system,

405: automate-theoretic techniques such as \emph{model

406:   checking}~\cite{Clarke00:MC} have been shown to be more useful in

407: practice. Recently, however, a propositional, linear-time temporal

408: logic with improved deductive properties has been

409: introduced~\cite{DFK06:TIME,DFK07:IJCAI}, providing the possibility of

410: practical deductive verification in the future. The essence of this

411: approach is to provide an XOR constraint between key

412: propositions. These constraints state that exactly one proposition from a XOR

413: set can be true at any moment in time. Thus, the automaton above can be

414: described by the

415: following clauses which are implicitly in the scope of a `$\always$' (`always

416: in the future') operator. 

417: %

418: $$

419: \begin{array}{ll}

420: 1.  & \start\imp s_t\\

421: 2.  & s_t\imp \Next(s_t\lor s_a)\\

422: 3.  & s_b\imp \Next s_t\\

423: 4.  & s_a\imp \Next s_w\\

424: 5.  & s_w\imp \Next(s_w\lor s_b)

425: \end{array}

426: $$

427: %

428: Here `$\next$' is a temporal operator denoting `at the next moment' and 

429: `$\start$' is a temporal operator which holds only at the initial moment in

430: time. The inherent assumption that at any moment in time exactly one of 

431: $s_a$, $s_b$, $s_t$ or $s_w$ holds, is denoted by the following.

432: $$

433: \always(s_a \oplus s_b \oplus s_t \oplus s_w)

434: $$

435: %

436: With the complexity of the decision problem (regarding $s_a$, $s_b$,

437: etc) being polynomial, then the properties of any finite collection of

438: such automata can be tractably verified using this

439: \emph{propositional} XOR temporal logic.

440: 

441: However, one might argue that this deductive approach, although

442: elegant and concise, is still no better than a model checking

443: approach, since it targets just \emph{finite} collections of (finite)

444: state machines. Thus, this naturally leads to the question of whether

445: the XOR temporal approach can be extended to \emph{first-order

446:   temporal logics} and, if so, whether a form of tractability still

447: applies. In such an approach, we can consider \emph{infinite} numbers

448: of finite-state automata (initially, all of the same

449: structure). Previously, we have shown that \fotl{} can be used to

450: elegantly specify such a system, simply by assuming the argument to

451: each predicate represents a particular

452: automaton~\cite{FKL06:VISSAS}. Thus, in the following $s_a(X)$ is true

453: if automaton $X$ is in state $s_a$:

454: %

455: $$

456: \begin{array}{ll}

457: 1.  & \start\imp \exists x. s_t(x)\\

458: 2.  & \forall x.\ (s_t(x)\imp \Next(s_t(x)\lor s_a(x)))\\

459: 3.  & \forall x.\ (s_b(x)\imp \Next s_t(x))\\

460: 4.  & \forall x.\ (s_a(x)\imp \Next s_w(x))\\

461: 5.  & \forall x.\ (s_w(x)\imp \Next(s_w(x)\lor s_b(x)))

462: \end{array}

463: $$

464: %

465: Thus, \fotl{} can be used to specify and verify broadcast protocols

466: between synchronous components~\cite{esparza99verification}. In this

467: paper we define a logic, \fotlx, which allows us to not only to

468: specify and verify systems of the above form, but also to specify and

469: verify more sophisticated asynchronous systems, and to carry out

470: verification with a reasonable complexity.

471: 

472: 

473: \section{\bffotlx}

474: 

475: \subsection{First-Order Temporal Logic}

476: %

477: First-Order (discrete, linear time) Temporal Logic, \fotl, is an

478: extension of classical first-order logic with operators that deal with

479: a discrete and linear model of time (isomorphic to the Natural

480: Numbers, $\Nat$).

481: 

482: \paragraph{Syntax.}

483: The symbols used in \fotl{} are

484: \begin{itemize}

485: \item \emph{Predicate symbols:} $P_0, P_1,\dots$ each of which is of a

486:   fixed arity (null-ary predicate symbols are \emph{propositions});

487: \item \emph{Variables:} $x_0, x_1,\dots$;

488: \item \emph{Constants:} $c_0,c_1,\dots$;

489: \item \emph{Boolean operators:} $\land$, $\lnot$, $\lor$, $\implies$,

490:   $\equiv$, $\true$ (`true'), $\false$ (`false');

491: \item \emph{First-order Quantifiers:} $\forall$ (`for all') and

492:   $\exists$ (`there exists'); and

493: \item \emph{Temporal operators:} $\always$ (`always in the future'),

494:   $\sometime$ (`sometime in the future'), $\next$ (`at the next

495:   moment'), $\until$ (until),  $\unless$ (weak until), and $\start$ (at the

496:   first moment in time).

497: \end{itemize}

498: %

499: Although the language contains constants, neither equality nor

500: function symbols are allowed. 

501: 

502: The set of well-formed \fotl{}-formulae is defined in the standard

503: way~\cite{HWZ00,DFK03:ToCL}:

504: \begin{itemize}

505: \item Booleans $\true$ and $\false$ are atomic \fotl-formulae;

506: \item if $P$ is an $n$-ary predicate symbol and

507: $t_i$, $1\leq i \leq n$, are variables or 

508: constants, then $P(t_1,\dots,t_n)$ is an atomic \fotl-formula;

509: \item if $\phi$ and $\psi$ are \fotl-formulae, so are 

510: $\lnot \phi$, $\phi\land\psi$, $\phi\lor\psi$, $\phi\implies\psi$,

511: and $\phi\equiv\psi$; 

512: \item if $\phi$ is an \fotl-formula and $x$ is a variable, then 

513: $\forall x \phi$ and $\exists x \phi$ are \fotl-formulae;

514: \item if $\phi$ and $\psi$ are \fotl-formulae, then so are 

515: $\always\phi$, $\sometime\phi$, $\next\phi$, $\phi\until\psi$, 

516: $\phi\unless\psi$, and $\start$.

517: \end{itemize}

518: %

519: A \emph{literal} is an atomic \fotl-formula or its negation.

520: 

521: \paragraph{Semantics,}

522: %

523: Intuitively, \fotl formulae are interpreted in \emph{first-order

524:   temporal structures} which are sequences $\gM$ of \emph{worlds},

525: $\gM = \gM_0,\gM_1,\dots$ with truth values in different worlds being

526: connected via temporal operators.

527: 

528: More formally, for every moment of time $n\geq 0$, there is a corresponding 

529: \emph{first-order} structure, $\gM_n = \langle D_n, I_n\rangle$, where

530: every $D_n$ is a non-empty set such that whenever $n<m$, $D_n\subseteq  D_m$,

531: %, the \emph{domain} of $\gM$, 

532: and $I_n$ is  an interpretation of predicate and constant symbols over $D_n$.

533: We require that the interpretation of constants is \emph{rigid}. Thus, for

534: every constant $c$ and all moments of time $i,j\geq 0$, we have $I_i(c)=

535: I_j(c)$.

536: 

537: A \emph{(variable) assignment} $\ga$ is a function from the set of individual

538: variables to $\cup_{n\in\Nat} D_n$. We denote the set of all assignments by 

539: $\gA$. The set of variable assignments $\gA_n$ corresponding to

540: $\gM_n$ is a subset of the set of all assignments,

541: $\gA_n = \{\ga\in\gA\;|\; \ga(x)\in D_n \textrm{ for every variable $x$}\}$; 

542: clearly, $\gA_n\subseteq\gA_m$ if $n<m$.

543: 

544: The \emph{truth} relation $\gM_n\models^\ga \phi$ in a structure $\gM$,

545: is defined inductively on the construction of $\phi$ 

546: \emph{only for those assignments $\ga$ that satisfy the condition

547: $\ga\in\gA_n$}. See Fig.~\ref{fig:sem} for details.

548: %

549: \begin{figure*}[t]

550: \begin{small}$$

551: \begin{array}{|lcl|}\hline

552: & &  \\ 

553: \gM_n\models^\ga \true&& \gM_n\not\models^\ga\false\\

554: \gM_n\models^\ga

555: \start &\textrm{iff} & n=0 \\

556: \gM_n\models^\ga P(t_1,\dots,t_m) & \textrm{iff} & 

557: \langle I_n^\ga(t_1),\dots I_n^\ga(t_m)\rangle \in I_n(P), \textrm{ where }\\

558: & &I_n^\ga(t_i)=I_n(t_i),

559: \textrm{ if $t_i$ is a constant, and } I_n^\ga(t_i) = \ga(t_i),

560: \textrm{ if $t_i$ is a variable}\\ 

561: \gM_n\models^\ga \lnot \phi & \textrm{iff}& \gM_n\not\models^\ga\phi\\

562: \gM_n\models^\ga \phi\land \psi & \textrm{iff}& \gM_n\models^\ga\phi\textrm{ and } \gM_n\models^\ga\psi\\

563: \gM_n\models^\ga \phi\lor \psi & \textrm{iff}& \gM_n\models^\ga\phi\textrm{ or } \gM_n\models^\ga\psi\\

564: \gM_n\models^\ga \phi\implies \psi & \textrm{iff}& \gM_n\models^\ga(\lnot\phi\lor\psi) \\

565: \gM_n\models^\ga \phi\equiv \psi & \textrm{iff}& \gM_n\models^\ga((\phi\implies\psi)\land(\psi\implies\phi)) \\

566: %

567: \gM_n\models^\ga \forall x \phi & \textrm{iff} & \gM_n\models^\gb\phi

568: \textrm{ for every assignment $\gb$ that may differ}~\textrm{from

569:   $\ga$ only in $x$ and such that $\gb(x)\in D_n$}\\ 

570: %

571: \gM_n\models^\ga \exists x \phi & \textrm{iff} & \gM_n\models^\gb\phi

572: \textrm{ for some assignment $\gb$ that may differ from $\ga$ only in

573:   $x$ and such that $\gb(x)\in D_n$}\\ 

574: %

575: \gM_n\models^\ga\next\phi & \textrm{iff}& \gM_{n+1}\models^\ga\phi;\\

576: \gM_n\models^\ga\sometime\phi & \textrm{iff}& \textrm{there exists } m\geq n \textrm{ such that } \gM_{m}\models^\ga\phi; \\

577: \gM_n\models^\ga\always\phi & \textrm{iff}& \textrm{for all $m\geq n$, } \gM_m\models^\ga\phi;\\

578: \gM_n\models^\ga(\phi\until\psi) & \textrm{iff}& \textrm{there exists $m\geq

579: n$, such that } \gM_m\models^\ga\psi\textrm{ and, for all } i\in\Nat,

580: n\leq i < m \textrm{ implies } \gM_i\models^\ga\phi;\\ 

581: \gM_n\models^\ga(\phi\unless\psi) & \textrm{iff }&

582: \gM_n\models^\ga(\phi\until\psi)\textrm{ or }

583: \gM_n\models^\ga\always\phi.\\ 

584: \mbox{\ } & & \\

585: \hline

586: \end{array}

587: $$

588: \end{small}

589: \caption{Semantics of \fotl.}\label{fig:sem}

590: \end{figure*}

591: %

592: $\gM$ is a \emph{model} for a formula $\phi$ (or $\phi$ is \emph{true} in

593: $\gM$) if, and only if, there exists an assignment $\ga$ in $D_0$ such that

594: $\gM_0\models^\ga\phi$.  A formula is \emph{satisfiable} if, and only if,

595: it has a model. A formula is \emph{valid} if, and only if, it is true in any

596: temporal structure $\gM$ under any assignment $\ga$ in $D_0$.

597: 

598: \New%

599: The models introduced above are known as \emph{models with expanding

600:   domains} since $D_n\subseteq D_{n+1}$.  Another important class of

601: models consists of \emph{models with constant domains} in which the

602: class of first-order temporal structures, where \fotl{} formulae are

603: interpreted, is restricted to structures $\gM = \langle D_n,

604: I_n\rangle$, $n\in\Nat$, such that $D_i = D_j$ for all

605: $i,j\in\Nat$. The notions of truth and validity are defined similarly

606: to the expanding domain case.  It is known~\cite{WZ01DecModal} that

607: satisfiability over expanding domains can be reduced to satisfiability

608: over constant domains with only a polynomial increase in the size of

609: formulae.

610: 

611: \subsection{Monodicity and Monadicity}

612: %

613: The set of valid formulae of \fotl{} is not recursively

614: enumerable. Furthermore, it is known that even ``small'' fragments of

615: \fotl, such as the \emph{two-variable monadic} fragment (where all

616: predicates are unary), are not recursively

617: enumerable~\cite{Merz:Incomp:1992,HWZ00}.  However, the set of valid

618: \emph{monodic} formulae is known to be finitely

619: axiomatisable~\cite{WZ:APAL:AxMono}.

620: \begin{definition}

621: An \fotl-formula $\phi$ is 

622: called \emph{monodic} if, and only if, any subformula of the form $\mT\psi$,

623: where $\mT$ is one of $\next$, $\always$, $\sometimes$ (or $\psi_1\mT\psi_2$,

624: where $\mT$ is one of $\until$, $\unless$), contains at most one free variable.

625: \end{definition}

626: %

627: We note that the addition of either equality or function symbols to

628: the monodic fragment generally leads to the loss of recursive

629: enumerability~\cite{WZ:APAL:AxMono,DFL02:StudiaLogica,Hodkinson:Packed}.

630: Thus, monodic \fotl{} is expressive, yet even small extensions lead to

631: serious problems. Further, even with its recursive enumerability,

632: monodic \fotl{} is generally undecidable. To recover decidability, the

633: easiest route is to restrict the first order part to some decidable

634: fragment of first-order logic, such as the guarded, two-variable or

635: monadic fragments. We here choose the latter, since monadic predicates

636: fit well with our intended application to parameterised

637: systems. Recall that monadicity requires that all predicates have

638: arity of at most `1'. Thus, we use monadic, monodic

639: \fotl{}~\cite{DFK03:ToCL}.

640: 

641: A practical approach to proving monodic temporal formulae is to use

642: \emph{fine-grained temporal resolution}~\cite{KDDFH05:IC}, which has

643: been implemented in the theorem prover \TRPppV~\cite{HKRV04:IJCAR}.

644: In the past, \TRPppV{} has been successfully applied  to problems from

645: several domains~\cite{GHDFK05:JAR}, in particular, to examples specified in

646: the temporal 

647: logics of knowledge (the fusion of propositional linear-time temporal

648: logic with multi-modal S5)~\cite{DFW97:JLC,Dix05,DFK06:TIME}.

649:  From this work it is clear that monodic first-order temporal logic is

650: an important tool for specifying complex systems. However, it is also

651: clear that the complexity, even of \emph{monadic} monodic first-order

652: temporal logic, makes this approach difficult to use for larger

653: applications~\cite{GHDFK05:JAR,FKL06:VISSAS}.      

654: 

655: \subsection{XOR Restrictions}

656: %

657: An additional restriction  we make to the above logic involves implicit XOR

658: constraints 

659: over predicates. Such restrictions were introduced into temporal

660: logics in~\cite{DFK06:TIME}, where the correspondence with B{\"u}chi

661: automata was described, and generalised in~\cite{DFK07:IJCAI}. In both

662: cases, the decision problem is of much better (generally, polynomial)

663: complexity than that for the standard, unconstrained, logic.

664: However, in these papers only \emph{propositional} temporal logic was

665: considered. We now add such an XOR constraint to \fotlx{}.

666: 

667: The set of predicate symbols $\Pi=\{P_0, P_1,\dots\}$, is now partitioned

668: into a set of XOR-sets, $X_1$, $X_2$, $\ldots$, $X_n$, with one

669: \emph{non-XOR} set $N$ such that

670: \begin{enumerate}

671: \item all $X_i$ are disjoint with each other,

672: \item $N$ is disjoint with every $X_i$,

673: \item $\Pi$\ $=\ \displaystyle\bigcup_{j=0}^n X_j \,\cup\, N$, and

674: \item for each $X_i$, exactly \emph{one} predicate within $X_i$ is

675:   satisfied (for any element of the domain) at any moment in time.

676: \end{enumerate}

677: \begin{example}

678: Consider the formula

679: $$

680: \forall x.\ ((P_1(x)\lor P_2(x))\land (P_4(x)\lor P_7(x)\lor P_8(x)))

681: $$

682: where $\{P_1,P_2\}\subseteq X_1$ and  $\{P_4,P_7,P_8\}\subseteq

683: X_2$. The above formula states that, for any element of the domain, a,

684: then one of $P_1(a)$ or $P_2(a)$ must be satisfied and one of

685: $P_4(a)$, $P_7(a)$ or $P_8(a)$ must be satisfied.

686: \end{example}

687: 

688: \subsection{Normal Form}

689: % Assume we have $n$ sets of XOR predicates 

690: % $P_1 = \{p_{11}(x),\ldots p_{1N_1}(x)\}$,

691: % $\ldots$,

692: % $P_n = \{p_{n1}(x), \ldots p_{nN_n}(x)\}$

693: % and a set of additional predicates $A = \{a_1(x), \ldots a_{N_a}(x)\}$.

694: % We also allow $0$-ary predicates (i.e. propositions).

695: % 

696: % \nb{!!!!!!!!!!$Y\to A$}.

697: To simplify our description, we will define a \emph{normal form} into

698: which \fotlx{} formulae can be translated.  In the following:

699: \begin{itemize}

700: \item $\accentset{\land}{X}^{\minus}_{ij}(x)$ denotes a conjunction of

701:   negated XOR predicates from the set $X_i$;

702: \item $\accentset{\lor}{X}^{\plus}_{ij}(x)$ denotes a disjunction of

703:   (positive) XOR predicates from the set $X_i$;

704: \item $\accentset{\land}{N}_i(x)$ denotes a conjunction of non-XOR

705:   literals;

706: \item $\accentset{\lor}{N}_i(x)$ denotes a disjunction of non-XOR

707:   literals.

708: \end{itemize}

709: %

710: A \emph{step} clause is defined as follows:

711: $$

712: \begin{array}{l}

713: \accentset{\land}X^\minus_{1j}(x) \land \ldots \accentset{\land}X^\minus_{nj}(x)

714: \land \accentset{\land}N_j(x)

715: \imp \\

716: \hspace*{2em}\next (\accentset{\lor}X^\plus_{1j}(x)  \lor \ldots \lor

717: \accentset{\lor}X^\plus_{nj}(x) \lor \accentset{\lor}N_j(x) )

718: \end{array}

719: %\mbox{Step}

720: $$

721: %

722: A \emph{monodic temporal problem in Divided Separated Normal Form

723:   (DSNF)}~\cite{DFK03:ToCL} is a quadruple $\langle \uP, \iP, \sP,

724: \eP\rangle$, where:

725: %

726: \begin{enumerate}

727: \itemsep=0pt

728: \item the universal part, $\uP$, is a finite set of arbitrary closed

729:   first-order formulae;% (clauses);

730: \item the initial part, $\iP$, is, again, a finite set of arbitrary

731:   closed first-order formulae;

732: \item the step part, $\sP$, is a finite set of step clauses; and

733: \item the eventuality part, $\eP$, is a finite set of 

734: eventuality clauses of the form $\sometime L(x)$, where $L(x)$ is a unary

735: literal.  

736: \end{enumerate}

737: %% The sets $\uP$, $\iP$, $\sP$, and $\sP$ are finite.

738: In what follows, we will not distinguish between a finite set of

739: formulae ${\mathcal X }$ and the conjunction $\bigwedge {\mathcal X}$

740: of formulae within the set. With each  monodic temporal

741: problem, we associate the formula

742: $$

743: \iP\land\always\uP\land\always\forall x\sP\land\always\forall x\eP.

744: $$

745: Now, when we talk about particular properties of a temporal problem (e.g.,

746: satisfiability, validity, logical consequences etc) we mean properties of

747: the associated formula.

748: 

749: Every monodic \fotlx formula can be translated to the normal form in 

750: satisfiability preserving way using a renaming and unwinding

751: technique which substitutes non-atomic subformulae and replaces temporal

752: operators by their fixed point definitions as described, for example,

753: in~\cite{fdp01}. A step in this transformation  is the following: We

754: recursively rename each innermost open subformula $\xi(x)$, whose main

755: connective is a temporal operator, by $P_{\xi}(x)$, where $P_{\xi(x)}$ is a new

756: unary predicate, and rename each innermost closed subformula $\zeta$, whose

757: main connective is a temporal operator, by $p_{\zeta}$, where $p_{\zeta}$ is a

758: new propositional variable. While renaming introduces new, non-XOR predicates

759: and propositions, practical problems stemming from verification are nearly

760: in the normal form, see Section~\ref{sec:model}.

761: 

762: %\subsection{Completeness}

763: %\begin{center}

764: %  \fbox{\sf From results on TLX~\cite{DFK06:TIME} and Monodic

765: %    \fotl{}~\cite{HWZ00}}

766: %\end{center}

767: %

768: \subsection{Complexity}

769: First-order temporal logics are notorious for being of a high

770: complexity. Even decidable sub-fragments of monodic first-order

771: temporal logic can be too complex for practical use. For example,

772: satisfiability of monodic monadic \fotl{} logic is known to be

773: $\mathsf{EXPSPACE}$-complete~\cite{HKKWZ03}. However, imposing

774: XOR restrictions we obtain better complexity bounds.

775: %

776: \begin{theorem}\label{th:complexity}

777: Satisfiability of monodic monadic \fotlx{} formulae (in the normal

778: form) %\nb{sic!}

779: can be decided in $2^{O(N_1 \cdot N_2 \cdot\dots\cdot N_n\cdot 2^{N_a})}$ time,

780: where $N_1$,\dots, $N_n$ are cardinalities of the sets of XOR predicates, and

781: $N_a$ is the cardinality of the set of non-XOR predicates.

782: \end{theorem}

783: Before we sketch the proof of this result, we show how the XOR restrictions

784: influence the complexity of the satisfiability problem for monadic first-order

785: (non-temporal) logic.

786: \begin{lemma}\label{lemma:fom}

787: Satisfiability of monadic first-order formulae can be decided in

788: $\mathsf{NTime}(O(n\cdot{N_1 \cdot N_2 \cdot\dots\cdot N_n\cdot 2^{N_a}}))$,

789: where $n$ is the length of the formula, and $N_1$,\dots, $N_n$, $N_a$ are as in

790: Theorem~\ref{th:complexity}.

791: \end{lemma}

792: \begin{proof}

793: As in \cite{BGG97}, Proposition 6.2.9, the non-deterministic decision procedure

794: first guesses a structure and then verifies that the structure is a model for

795: the given formula. 

796: It was shown,

797: \cite{BGG97}, Proposition 6.2.1, Exercise 6.2.3, that if a monadic first-order

798: formula has a model, it also has a model, whose domain is the set of all

799: \emph{predicate colours}.

800: A {predicate colour}, $\gamma$, is a set of unary literals such that for

801: every predicate $P(x)$ from the set of all predicates $X_1\union\dots,

802: X_n\union N$, either $P(x)$ or $\lnot P(x)$ belongs to $\gamma$.   Notice that under the conditions of the lemma, there are at

803: most ${N_1 \cdot N_2 \cdot\dots\cdot N_n\cdot 2^{N_a}}$ different predicate

804: colours. Hence, the structure to guess is of $O({N_1 \cdot N_2 \cdot\dots\cdot

805: N_n\cdot 2^{N_a}})$ size.

806: 

807: It should be clear that one can evaluate a monadic formula of the size $n$ in a

808: structure of the size $O({N_1 \cdot N_2 \cdot\dots\cdot N_n\cdot

809: 2^{N_a}})$ in deterministic $O(n\cdot {N_1 \cdot N_2 \cdot\dots\cdot N_n\cdot

810: 2^{N_a}})$ time. Therefore, the overall complexity of the decision procedure is

811: $\mathsf{NTime}(O(n\cdot{N_1 \cdot N_2 \cdot\dots\cdot N_n\cdot 2^{N_a}}))$.

812: \end{proof}

813: %

814: %

815: \begin{proof}[of Theorem~\ref{th:complexity}, Sketch]

816:   For simplicity of presentation, we assume the formula contains no

817:   propositions.  Satisfiability of a monodic \fotl{} formula is

818:   equivalent to a property of the \emph{behaviour graph} for the

819:   formula, checkable in time polynomial in the product of the number of 

820:   different predicate colours and the size of the graph,

821:   see~\cite{DFK03:ToCL}, Theorem 5.15. For unrestricted \fotl{}

822:   formulae, the size of the behaviour graph is double exponential in

823:   the number of predicates. We estimate now the size of the behaviour

824:   graph and time needed for its construction for \fotlx{} formulae.

825: 

826:   Let $\Gamma$ be a set of predicate colours and $\rho$ be a map from the set

827:   of constants, $\const(\TProb)$, to $\Gamma$.  A couple $\langle\Gamma,

828:   \rho\rangle$ is called a \emph{colour scheme}.

829:   Nodes of the behaviour graph are {colour schemes}. Clearly, there

830:   are no more than $2^{O(N_1 \cdot N_2 \cdot\dots\cdot N_n\cdot

831:     2^{N_a})}$ different colour schemes. However, not every colour

832:   scheme is a node of the behaviour graph: a colour scheme

833:   $\mathcal{C}$ is a node if, and only if, a monadic formula of

834:   first-order (non-temporal) logic, constructed from the given

835:   \fotlx{} formula and the colour scheme itself, is satisfiable (for

836:   details see~\cite{DFK03:ToCL}). A similar first-order monadic condition

837:   determines which nodes are connected with edges. It can be seen that the size

838:   of the formula is polynomial in both cases.

839:  By Lemma~\ref{lemma:fom}, satisfiability of monadic first-order formulae can be

840:  decided in deterministic $2^{O(N_1 \cdot N_2 \cdot\dots\cdot N_n\cdot

841:  2^{N_a})}$ time.

842: 

843:   Overall, the behaviour graph, representing all possible models, for

844:   an \fotlx formula can be constructed in $2^{O(N_1 \cdot N_2

845:     \cdot\dots\cdot N_n\cdot 2^{N_a})}$ time.

846: \end{proof}

847: 

848: 

849: %%%%%%%%%%%%%%% beginning of edited part, Lisits, 11.01.2007

850: 

851: \section{Infinite-State Systems}

852: % Asynchronous Machines Communicating via  Delayed Broadcast}

853: \label{sec:model}

854: % \begin{quote}

855: % \textsf{N.B. need a model that handles asynchrony (and delayed

856: %  messages) well, e.g. comunicating finite-state machines with

857: %  queues?}

858: %\end{quote}

859: % \begin{quote}

860: % \textsf{AL: Queues appears to be problematic since we cannot specify their behaviour

861: % in temporal logic. So below we consider asynchronous finite-state 

862: % machines which communicate via delayed broadcast with acknowlegement. }

863: % 

864: % \end{quote} 

865: % \begin{center}

866: %   \fbox{\sf Text below from VISSAS~\cite{FKL06:VISSAS} and broadcast

867: %     protocols~\cite{esparza99verification}}

868: % \end{center}

869: %

870: In previous work,

871: notably~\cite{esparza99verification,delzanno00automatic} a

872: parameterised  finite state machine based model,

873: suitable for the specification and verification of protocols over

874: arbitrary numbers of processes was defined. Essentially, this uses a

875: family of identical, and synchronously executing, finite state

876: automata with a rudimentary form of communication: if one automaton

877: makes a transition (an action) $a$, then it is required that

878: \emph{all} other automata simultaneously make a complementary

879: transition (reaction) $\bar{a}$. In \cite{FKL06:VISSAS} we translated

880: this automata model into monodic \fotl{} and used automated theorem

881: proving in that logic to verify parameterised cache coherence

882: protocols~\cite{Del03}. The model assumed not only synchronous

883: behaviour of the communicating automata, but instantaneous broadcast.

884: 

885: Here we present a more general model suitable for specification of

886: both synchronous and asynchronous systems (protocols) with (possibly)

887: delayed broadcast and give its faithful translation into \fotlx. This

888: not only exhibits the power of the logic but, with the improved

889: complexity results of the previous section, provides a route towards

890: the practical verification of temporal properties of infinite state

891: systems.

892: 

893: \subsection{Process Model}

894: %

895: We begin with a description of both the asynchronous model, and the 

896: delayed broadcast approach.

897: 

898: \begin{definition}[Protocol]\label{def:protocol-simple}

899: A protocol, {\cal P} is a tuple $\langle Q, I, \Sigma,\tau \rangle$, 

900: where

901: 

902: \begin{itemize}

903: \item $Q$ is a finite set of states; 

904: \item $I \subseteq Q$ is a set of initial states;  

905: \item $\Sigma = \Sigma_{L} \cup \Sigma_{M} \cup \bar{\Sigma}_{M}$, where

906: \begin{itemize}

907: \item $\Sigma_{L}$ is a finite set of local actions; 

908: \item $\Sigma_{M}$ is a finite set of broadcast actions,\\ i.e. ``send a

909:   message''; 

910: \item $\bar{\Sigma}_{M} = \{\bar{\sigma}\mid \sigma \in \Sigma_{M}\}$ is 

911: the set of broadcast reactions, i.e. ``receive a message'';

912: \end{itemize}

913: \item $\tau \subseteq  Q \times \Sigma \times Q$ is a transition

914: relation that satisfies the following property 

915: \[\forall \sigma \in \Sigma_{M}.\ \forall q \in Q.\ \exists q' \in Q.\ 

916: \langle q,\bar{\sigma},q' \rangle \in \tau \] 

917: %

918: i.e., ``readiness to receive a message in any state''.

919: \end{itemize}

920: \end{definition}

921: %

922: Further, we define a notion of global machine, which is a set of $n$

923: finite automata, where $n$ is a parameter, each following the protocol

924: and able to communicate with others via (possibly delayed) broadcast.

925: To model asynchrony, we introduce a special automaton action,

926: $idle\,\not\in \Sigma$, meaning the automaton is not active and so its

927: state does not change. At any moment an arbitrary group of automata may

928: be idle and all non-idle automata perform their actions in accordance

929: with the transition function $\tau$; different automata may perform

930: different actions.

931: 

932: 

933: \begin{definition}[Asynchronous Global Machine]\label{def:glob_mach1} 

934: %

935:   Given a protocol, ${\cal P}= \langle Q, I, \Sigma,\tau \rangle$, the

936:   global machine ${\cal M}_{G}$ of dimension \emph{$n$} is the tuple $\langle

937:   Q_{{\cal M}_{G}}, I_{{\cal M}_{G}}

938: %\Sigma_{{\cal M}_{G}}, 

939: \tau_{{\cal M}_{G}}, {\cal E} \rangle$, where

940: 

941: \begin{itemize}

942: \item $Q_{{\cal M}_{G}} = Q^{n}$

943: %\item $\Sigma_{{\cal M}_{G}} = \Sigma$

944: \item $I_{{\cal M}_{G}} = I^{n}$

945: \item $\tau_{{\cal M}_{G}} \subseteq Q_{{\cal M}_{G}} 

946: \times (\Sigma \cup \{idle\}) ^{n} 

947: \times Q_{{\cal M}_{G}}$ is a transition

948: relation that satisfies the following property

949: %

950: $$\begin{array}{c}

951: \langle \langle s_{1}, \ldots, s_{n} \rangle, \langle \sigma_{1},

952: \ldots \sigma_{n} \rangle, \langle s'_{1}, \ldots, s'_{n} \rangle

953: \rangle \in \tau_{{\cal M}_{G}}\\

954: \hbox{\textit{iff}}\\

955: \forall 1\leq i\leq n.\ 

956: [(\sigma_{i} \not = idle \Rightarrow

957: \langle s_{i}, \sigma_{i}, s'_{i} \rangle \in \tau) \\

958: \land (\sigma_{i} = idle \Rightarrow s_{i} = s'_{i}]\,.

959: \end{array}$$

960: 

961: 

962: \item ${\cal E} = 2^{\Sigma_{M}}$ is a communication environment, that is a set of possible

963: sets of messages in transition.   

964: 

965: 

966: 

967: \end{itemize} 

968: %

969: An element $G \in Q_{{\cal M}_{G}} \times (\Sigma \cup \{idle\}) ^{n}

970: \times {\cal E}$ is said to be a global configuration of the machine.

971: 

972: A run of a global machine ${\cal M}_{G}$ is a possibly infinite

973: sequence $\langle s^{1}, \sigma^{1}, E_{1} \rangle \ldots \langle

974: s^{i}, \sigma^{i}, E_{i} \rangle \ldots $ of global configurations

975: of ${\cal M}_{G}$ satisfying the properties (1)--(6) listed

976: below. In this formulation we assume $s^{i} = \langle s_{1}^{i},

977: \ldots, s_{n}^{i}\rangle$ and $ \sigma^{i} = \langle \sigma_{1}^{i},

978: \ldots, \sigma_{n}^{i} \rangle$.

979: 

980: 

981: \begin{enumerate}

982: 

983: \item $s^{1} \in I^{n}$\\

984:   (``initially all automata are in initial states'');  

985: 

986: \item $E_{1} = \emptyset$\\

987:  (``initially there are no messages in  transition''); 

988: 

989: \item  $\forall i.\ \langle s^{i}, \sigma^{i}  , s^{i+1} \rangle \in

990:   \tau_{{\cal M}_{G}}$ \\

991: (``an arbitrary part of the automata can fire'';  

992: 

993:  

994: \item $\forall a \in \Sigma_{M}.\; \forall i. \; \forall j.\, (

995:   (\sigma^{i}_{j} = a) \Rightarrow \forall k. \; \exists l \ge i. \;

996:   (\sigma^{l}_{k} = \bar{a}))$\\

997:   (``delivery to all participants is guaranteed'');

998: 

999: \item $\forall a \in \Sigma_{M}. \; \forall i. \; \forall j. \; 

1000: [(\sigma^{i}_{j} = \bar{a}) \Rightarrow (a \in E_{i}) \lor \exists k. \; \sigma^{i}_{k} = a )]$  

1001: (``one can receive only messages  kept by the environment, or sent at the 

1002: same moment of time '')  

1003:  

1004: \end{enumerate} 

1005: %

1006: In order to formulate further requirements we introduce the following

1007: notation:

1008: 

1009: 

1010: \[ Sent_{i} = \{a \in \Sigma_{M} \mid \exists j.\ \sigma^{i}_{j} = a \}\] 

1011: 

1012: \noindent $Delivered_{k} =$

1013: $$

1014: \left\{\begin{array}{c|l}

1015:                  & \exists i \le k.\ (a \in Sent_{i}) \ \land\\

1016: a \in \Sigma_{M} & (\forall l.\  (i < l < k) \rightarrow a \not\in

1017: Sent_{l})\  \land\\

1018:                  & (\forall j. \exists l.\ (i \le l \le k) \land

1019:                  (\sigma^{l}_{j} = \bar{a}))

1020: \end{array}\right\}$$

1021: %

1022: Then, the last requirement the run should satisfy is

1023:    % \footnote{\emph{AL:

1024:    % There is a delicate point here concerning whether a message should

1025:    % be delivered to the sender himself. In the above I assume it

1026:    % should - this simplifies further temporal translation.  Otherwise,

1027:    % we would need equality + related problems again. Downside of this

1028:    % decision, however is that the older model (with synchronous

1029:    % instantaneous broadcast) is not an instance (particular case) of

1030:    % this more general model, but rather a variation.}}

1031: \begin{enumerate} 

1032: \item[6.] $\forall i.\ E_{i+1} = (E_{i} \cup Sent_{i}) - Delivered_{i}$ 

1033: \end{enumerate} 

1034: %

1035: \end{definition} 

1036: 

1037: \paragraph{Example: Asynchronous Floodset Protocol.} 

1038: We illustrate the use of the above model by presenting the

1039: specification of an asynchronous FloodSet protocol in our model. This

1040: is a variant of the \emph{FloodSet algorithm with alternative decision

1041:   rule} (in terms of \cite{Lynch96:book}, p.105) designed for solution

1042: of the Consensus problem. 

1043: %,

1044: 

1045: The setting is as follows. There are $n$ processes, each having an

1046: {\em input bit} and an \emph{output bit}. The processes work

1047: asynchronously, run the same algorithm and use {\em broadcast} for

1048: communication. The broadcasted messages are guaranteed to be

1049: delivered, though possibly with arbitrary delays. (The process is

1050: described graphically in Fig.~\ref{fig:flood}.)

1051: 

1052: \begin{figure}[ht]

1053: \begin{center}

1054: \includegraphics[width=0.4\textwidth]{cons.eps}

1055: \end{center}

1056: \caption{Asynchronous FloodSet Protocol Process.\label{fig:flood}} 

1057: \end{figure}

1058: %originally  in the presence 

1059: %of crash (or fail-stop) failures.    

1060: %\subsection{Overview of the Protocol}

1061: %

1062: 

1063: The goal of the algorithm is to eventually reach an agreement, i.e. to

1064: produce an output bit, which would be the same for all 

1065: processes. It is required also that if all

1066: processes have the same input bit, that bit should be produced as an

1067: output bit.

1068: 

1069: The asynchronous FloodSet protocol we consider here is adapted from 

1070: \cite{Lynch96:book}. Main differences with original protocol are: 

1071: 

1072: 

1073: \begin{figure*}[t]

1074: \begin{center}

1075: \fbox{\begin{minipage}{0.98\textwidth}

1076: \begin{itemize}

1077: %%\item[{\bf I}] Each automaton is in precisely one state:\\{}

1078: %%$\always[\forall x.\ P_{q_{1}}(x)\oplus P_{q_{2}(x)}\oplus\ldots\oplus

1079: %%P_{q_{k}}(x)]$, where $\{P_{q_{1}}, \ldots P_{q_{k}}\} = Q$.

1080: 

1081: \item[{\bf I.}] Each automaton either performs one of the actions available

1082:   in its state, or is idle:\\{}

1083:  $\always[\forall x.\ P_{q}(x)

1084:   \rightarrow A_{\sigma_{1}}(x)\lor \ldots\lor

1085:   A_{\sigma_{k}}(x) \lor A_{idle}(x)]$, where $\{\sigma_{1}, \ldots

1086:   \sigma_{k}\} = \{\sigma \in \Sigma \mid \exists r \langle q, \sigma,

1087:   r \rangle \in \tau \}$.

1088: 

1089: \item[{\bf II.}] Action effects (non-deterministic actions):\quad$\always[\forall x P_{q}(x) \land A_{\sigma}(x)

1090:   \rightarrow \next \bigvee_{\langle q, \sigma, r \rangle \in \tau}

1091:   P_{r}(x)]$ for all $q \in S$ and $\sigma \in \Sigma$.

1092: 

1093: \item[{\bf III.}] Effect of being idle:\quad $\always[\forall x P_q(x) \land

1094:   A_{idle}(x) \rightarrow \next P_q(x)]$, for all $q \in S$

1095: 

1096: \item[{\bf IV.}] Initially there are no messages in the transition and all

1097: automata are in initial states:\quad

1098:   $\start \rightarrow \neg m_{\sigma}$ for all $\sigma \in \Sigma_{m}$ and 

1099:   $\start \rightarrow \forall x \bigvee_{q \in I} P_{q}(x)$. 

1100: 

1101: \item[{\bf V.}] All messages are eventually received (Guarantee of

1102:   Delivery):\quad$\always [\exists y A_{\sigma}(y) \rightarrow

1103:   \forall x \sometimes A_{\bar{\sigma}}(x)]$, for all $\sigma \in

1104:   \Sigma_{m}$. 

1105: 

1106: \item[{\bf VI.}] Only messages kept in the environment (are in transition),

1107:   or sent at the same moment of time can be received:\quad

1108:   $\always[\forall x A_{\bar{\sigma}}(x) \rightarrow  m_{\sigma} \lor

1109:   \exists y A_{\sigma}(y)   ]$ for all $\sigma \in \Sigma_{m}$. 

1110: 

1111: \item[{\bf VII.}]  Finally, for all $\sigma \in \Sigma_{m}$, we have

1112:   the conjunction of the following formulae:

1113: 

1114: \begin{enumerate}

1115: %%\item $\neg delivered_{\sigma}$

1116: \item $\start \rightarrow \forall x.\ \neg Received_{\sigma}(x)$

1117: %%\item $\always [delivered_{\sigma} \leftrightarrow \forall x.\ Received_{\sigma}(x)]$ 

1118: %%\item $\always[(\neg delivered_{\sigma})\until(\forall x.\  Received_{\sigma}(x))]$ 

1119: \item $\always[\forall x.\  (A_{\bar{\sigma}}(x) \land \neg \forall

1120:   y.\ 

1121: Received_{\sigma}(y)) \rightarrow \next Received_{\sigma}(x)]$

1122: \item $\always[\forall x.\  (Received_{\sigma}(x) \land \neg \forall

1123:   y.\ Received_{\sigma}(y)\rightarrow \next Received_{\sigma}(x)]$

1124: \item $\always[\forall x.\ (\neg (A_{\bar{\sigma}}(x) \lor

1125:   Received_{\sigma}(x)) \land \neg \forall y.\ Received_{\sigma}(y))

1126:   \rightarrow \next \neg Received_{\sigma}(x)]$

1127: \item $\always[\forall x.\  Received_{\sigma} \rightarrow \next \neg m_{\sigma}]$

1128: \item $\always[\exists x.\ A_{\sigma}(x) \land \neg \forall y.\ 

1129: Received_{\sigma}(y) \rightarrow \next m_{\sigma}]$

1130: \item $\always[\neg \exists x.\ A_{\sigma}(x) \land \neg \forall y.\ 

1131: Received_{\sigma}(y) \rightarrow (m_{\sigma}\leftrightarrow 

1132: \next m_{\sigma}] $

1133: \end{enumerate}

1134: %

1135: 

1136: 

1137: \end{itemize}

1138: \end{minipage}}

1139: \end{center}

1140: \caption{Temporal Specification of Abstract Protocol

1141:   Structure.\label{fig:trans}} 

1142: \end{figure*}

1143: 

1144: 

1145: \begin{itemize}

1146: \item the original protocol was synchronous, while our variant is asynchronous;

1147: \item the original protocol assumed instantaneous message delivery,

1148:   while we

1149:   allow arbitrary delays in delivery; and 

1150: \item although the original protocol was designed to work in the

1151:   presence of crash (or fail-stop) failures, we assume, for

1152:   simplicity, that there are no failures.

1153: \end{itemize}

1154: %

1155: Because of the absence of failures the protocol is very simple and

1156: unlike the original one does not require ``retransmission'' of any

1157: value.  We will show later (in Section~\ref{sec:var}) how to include

1158: the case of crash failures in the specification (and verification).

1159: Thus, the asynchronous FloodSet protocol is defined, informally, as

1160: follows.

1161: %(adapted from \cite{Lynch96:book}\footnote{The difference

1162: %being that, in \cite{Lynch96:book}, every process {\em knows} the bound $f$ in

1163: %advance and stops the execution of the protocol after $f+2$ rounds,

1164: %producing the appropriate output bit. For generality, we consider the

1165: %version where the processes do not know $f$ in advance and produce a

1166: %\emph{tentative output bit} at every round.}) 

1167: %is as follows.

1168: \begin{itemize}

1169: \item At the first round of computations, every process broadcasts its

1170:       input bit.

1171: %\item At every later round, a process broadcasts any value {\em the first

1172: %time it sees it}.

1173: \item At every round the (tentative) output bit is set to the

1174: minimum value ever seen so far.

1175: \end{itemize}

1176: %

1177: The correctness criterion for this protocol is that, eventually, the

1178: output bits of all processes will be the same.

1179: \medskip

1180: 

1181: \noindent 

1182: Now we can specify the asynchronous FloodSet as a protocol $\langle

1183: Q,I, \Sigma, \tau \rangle$, where $Q = \{ i_{0}, i_{1}, o_{0},

1184: o_{1}\}$; $I = \{i_{0}, i_{1}\}$; $\Sigma = \Sigma_{m} \cup

1185: \bar{\Sigma}_{m} \cup \Sigma_{L}$ with $\Sigma_{m} = \{0,1\}$,

1186: $\bar{\Sigma}_{m} = \{\bar{0}, \bar{1}\}$, $\Sigma_{L} =

1187: \emptyset$. The transition relation $\tau = \{\langle

1188: i_{0},0,o_{0}\rangle,$ $\langle o_{0}, \bar{0}, o_{0}\rangle,$

1189: $\langle o_{0}, \bar{1}, o_{0}\rangle,$ $\langle

1190: i_{1},1,o_{1}\rangle,$ $\langle o_{1},\bar{0},o_{0}\rangle,$ $\langle

1191: o_{1},\bar{1},o_{1} \rangle \}$.

1192: 

1193: 

1194: \subsection{Temporal Translation} 

1195: %

1196: % {\bf Comment(AL): In the translation I have not used three-parts

1197: %   format for the specification which we have used in the past

1198: %   (VISSAS, etc). The reason is not all formulae (esp. see the

1199: %   properties of broadcast) can be fitted easily in the format

1200: %   (without renaming etc). I am not quite sure whether we want to do

1201: %   that.  Because of that ``always'' closure is presented everywhere

1202: %   explicitly.}

1203: %

1204: Given a protocol ${\cal P} = \langle Q,I,\Sigma,\tau\rangle$, we

1205: define its translation to \fotlx{} as follows.  \medskip

1206: 

1207: \noindent For each $q \in Q$, introduce a monadic predicate symbol

1208: $P_{q}$ and for each $\sigma \in \Sigma \cup \{idle\}$ introduce a

1209: monadic predicate symbol $A_{\sigma}$. For each $\sigma \in

1210: \Sigma_{M}$ we introduce also a propositional symbol $m_{\sigma}$.

1211: 

1212: 

1213: %(representing the notion of the ``active'' automaton). 

1214: Intuitively,

1215: elements of the domain in the temporal representation will represent

1216: exemplars of finite automata, and the formula $P_{q}(x)$ is intended to

1217: represent ``automaton x is in state $q$''. The formula $A_{\sigma}(x)$ is going

1218: to represent ``automaton $x$ performs action $\sigma$''.    

1219: Proposition $m_{\sigma}$ will denote the fact 

1220: ``message $\sigma$ is in transition'' (i.e. it has been sent but not all

1221: participants have received it.)  

1222: 

1223: Because of intended meaning we define two XOR-sets: 

1224: $X_{1} = \{P_{q}\mid q \in Q \}$ and $X_{2} = \{A_{\sigma} \mid \sigma \in 

1225: \Sigma \cup \{idle\}\}$. 

1226: All other predicates belong to the set of non-XOR predicates.

1227:  \medskip

1228: 

1229:  \noindent We define the temporal translation of ${\cal P}$, called

1230:  $T_{\cal P}$, as a conjunction of the formulae in

1231:  Fig.~\ref{fig:trans}. Note that, in order to define the temporal

1232:  translation of requirement (6) above, (on the dynamics of 

1233: environment updates) we introduce the

1234: unary predicate symbol $Received_{\sigma}$ for every $\sigma \in

1235: \Sigma_{m}$.

1236: \medskip

1237: 

1238: \noindent We now consider the correctness of the temporal

1239: translation. This translation of protocol $\cal P$ is faithful in the

1240: following sense.

1241: 

1242: \begin{mfproposition}

1243: \label{prop:trans}

1244: Given a protocol, ${\cal P}$, and a global machine, ${\cal M}_{G}$, of

1245: dimension $n$, then any temporal model $M_{1}, M_{2}, \ldots$ of

1246: $T_{\cal P}$ with the finite domain $c_{1}, \ldots c_{n}$ of size $n$

1247: represents some run $\langle s^{1}, \sigma^{1}, E_{1} \rangle \ldots \langle

1248: s^{i}, \sigma^{i}, E_{i} \rangle \ldots $  of ${\cal M}_{G}$ as

1249: follows:

1250: 

1251: $\langle \langle s_{1}, \ldots, s_{n} \rangle, 

1252:           \langle \sigma_{1}, \ldots, \sigma_{n} \rangle, 

1253:           E\rangle$ is $i$-th configuration of the run iff 

1254: $M_{i} \models P_{q_{1}}(c_{1}) \land \ldots

1255: P_{q_{n}}(c_{n})$,   $M_{i} \models A_{\sigma_{1}}(c_{1}) \land \ldots

1256: A_{\sigma_{n}}(c_{n})$  and $E = 

1257: \{\sigma \in \Sigma_{m} \mid M_{i} \models m_{\sigma}\}$        

1258:             

1259: 

1260: %$$

1261: %\hbox{\rm for all}\ j.\ \langle q_{1}, \ldots q_{n} \rangle \in G_{j}

1262: %\quad\leftrightarrow\quad M_{j} \models P_{q_{1}}(c_{1}) \land \ldots

1263: %P_{q_{n}}(c_{n})

1264: %$$

1265: %

1266: Dually, for any run of ${\cal M}_{G}$ there is a temporal model of

1267: $T_{\cal P}$ with a domain of size $n$ representing this run.

1268: \end{mfproposition} 

1269: 

1270: \begin{proof} 

1271: By routine inspection of the definitions of runs, temporal models and

1272: the translation.

1273: \end{proof}

1274: 

1275: \subsection{Variations of the model}\label{sec:var}

1276: 

1277: The above model allows various modifications and corresponding version

1278: of Proposition~\ref{prop:trans} still holds.

1279: 

1280: \paragraph{Determinism.} The basic model allows non-deterministic

1281: actions. To specify the case of deterministic actions only, one should

1282: replace the ``Action Effects'' axiom in Fig.~\ref{fig:trans} by the

1283: following variant:

1284: \[

1285: \always[\forall x.\ P_{q}(x) \land A_{\sigma}(x) \rightarrow \next P_{r}(x)]

1286: \]   for all $\langle q, \sigma, r  \rangle \in \tau$

1287: 

1288: \paragraph{Explicit bounds on delivery.} In the basic mode, no

1289: explicit bounds on delivery time are given. To introduce bounds one

1290: has to replace the ``Guarantee of Delivery'' axiom with the following

1291: one:

1292: 

1293: \[

1294: \always [\exists y.\, A_{\sigma}(y) \rightarrow \forall x.\, \next A_{\bar{\sigma}}(x) \lor \next A_{\bar{\sigma}}(x) \lor \ldots 

1295: \lor \next^{n} A_{\bar{\sigma}}(x)]

1296: \]  for all $\sigma \in \Sigma_{m}$ and some $n$ (representing the

1297: maximal delay).

1298: 

1299: 

1300: \paragraph{Finite bounds on delivery.} One may replace the ``Guarantee of

1301:   Delivery'' axiom with the following one  

1302: 

1303: \[

1304: \always [\exists y.\ A_{\sigma}(y) \rightarrow \sometimes \forall x.\ Received_{\bar{\sigma}}(x)]

1305: \]  for all $\sigma \in \Sigma_{m}$.

1306: 

1307: \paragraph{Crashes.} One may replace the ``Guarantee of Delivery''

1308: axiom by an axiom stating that only the messages sent by normal

1309: (non-crashed) participants will be delivered to all participants.

1310: (See~\cite{FKL06:VISSAS} for examples of such specifications in a

1311: \fotl{} context.)

1312: 

1313: %\paragraph{Initial.} Specification can also be extended with some initial conditions. 

1314:  

1315: 

1316: \paragraph{Guarded actions.} One can also extend the model with

1317: guarded actions, where action can be performed depending on global

1318: conditions in global configurations.

1319: \bigskip

1320: 

1321: \noindent Returning to the FloodSet protocol, one may consider a

1322: variation of the asynchronous protocol suitable for resolving the

1323: Consensus problem in the presence of \emph{crash failures}. We can

1324: modify the above setting as follows. Now, processes may fail and, from

1325: that point onward, such processes send no further messages. Note,

1326: however, that the messages sent by a process {\em in the moment of

1327:   failure} may be delivered to {\em an arbitrary subset} of the

1328: non-faulty processes.

1329: 

1330: The goal of the algorithm also has to be modified, so only

1331: \emph{non-faulty} processes are required to eventually reach an

1332: agreement. Thus, the FloodSet protocol considered above is modified by

1333: adding the  following rule: 

1334: %

1335: \begin{itemize}

1336: \item At every round (later than the first), a process broadcasts any

1337:   value  {\em the first time it sees it}.

1338: \end{itemize}

1339: %

1340: Now, in order to specify this protocol the variation of the model with

1341: crashes should be used. The above rule can be easily encoded in the

1342: model and we leave it as an exercise for the reader.

1343: 

1344: An interesting point here is that the protocol is actually correct

1345: under the assumption that \emph{only finitely many processes may

1346:   fail.}  This assumption is automatically satisfied in our automata

1347: model, but not in its temporal translation. Instead, one may use the

1348: above \emph{Finite bounds on delivery} axiom to prove the

1349: correctness of this variation of the algorithm.

1350: 

1351: 

1352: 

1353: \subsection{Verification}

1354: %

1355: Now we have all the ingredients to perform the verification of

1356: parameterised protocols.  Given a protocol $\cal P$, we can translate

1357: it into a temporal formula $T_{\cal P}$. For the temporal

1358: representation, $\chi$ of a required correctness condition, we then

1359: check whether $T_{P} \rightarrow \chi$ is valid temporal formula. If

1360: it is valid, then the protocol is correct for all possible values of

1361: the parameter (sizes).

1362: 

1363: Correctness conditions can, of course, be described using any legal

1364: \fotlx{} formula. For example, for the above FloodSet protocol(s) we

1365: have a liveness condition to verify:

1366: 

1367: \[

1368: \sometimes (\forall x.\ o_{0}(x) \lor \forall x.\ o_{1}(x)) 

1369: \]

1370: 

1371: or, alternatively

1372: 

1373: \[

1374: \sometimes \left[ \begin{array}{l}

1375:     (\forall x.\ \mathit{Non}\hbox{\rm -}\mathit{faulty}(x) \rightarrow o_{0}(x))\ \lor\\

1376:     (\forall x.\ \mathit{Non}\hbox{\rm -}\mathit{faulty}(x) \rightarrow o_{1}(x))

1377:     \end{array}\right]

1378: \] 

1379: %

1380: in the case of a protocol  working in presence of processor crashes.  

1381: 

1382: While space precludes describing many further conditions, we just note

1383: that, in~\cite{FKL06:VISSAS}, we have demonstrated how this approach

1384: can be used to verify safety properties, i.e with $\chi = \always

1385: \phi$. Since we have the power of \fotlx{}, but with decidability

1386: results, we can also automatically verify fairness formulae of the

1387: form $\chi = \always\sometime\phi$.

1388:  

1389:  

1390:  

1391: %%%%%%%%%%%%%%%%%%%%%%%%%  End of edited part,. Lis: 15.01.2007 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1392: 

1393: 

1394: \section{Concluding Remarks}

1395: %

1396: In the propositional case, the incorporation of XOR constraints within

1397: temporal logics has been shown to be advantageous, not only because of

1398: the reduced complexity of the decision procedure (essentially,

1399: polynomial rather than exponential;~\cite{DFK07:IJCAI}), but also

1400: because of the strong fit between the scenarios to be modelled (for

1401: example, finite-state verification) and the XOR

1402: logic~\cite{DFK06:TIME}). The XOR constraints essentially allow us to

1403: select a set of names/propositions that must occur exclusively. In the

1404: case of verification for finite state automata, we typically consider the

1405: automaton states, or the input symbols, as being represented by such

1406: sets. Modelling a scenario thus becomes a problem of engineering

1407: suitable (combinations of) XOR sets.

1408:  

1409: In this paper, we have developed an XOR version of \fotl{}, providing:

1410: its syntax and semantics; conditions for decidability; and detailed

1411: complexity of the decision procedure.  As well as being an extension

1412: and combination of the work reported in both~\cite{DFK03:ToCL}

1413: and~\cite{DFK07:IJCAI}, this work forms the basis for tractable

1414: temporal reasoning over infinite state problems. In order to motivate

1415: this further, we considered a general model concerning the

1416: verification of infinite numbers of identical processes. We provide an

1417: extension of the work in~\cite{FKL06:VISSAS}

1418: and~\cite{AbdullaJNdS04,AbdullaJRS06}, tackling liveness properties of

1419: infinite-state systems, verification of asynchronous infinite-state

1420: systems, and varieties of communication within infinite-state systems.

1421: In particular, we are able to capture some of the more complex aspects

1422: of \emph{asynchrony} and \emph{communication}, together with the

1423: verification of more sophisticated \emph{liveness} and \emph{fairness}

1424: properties.

1425: 

1426: The work in~\cite{FKL06:VISSAS} on basic temporal specification such

1427: as the above have indeed shown that deductive verification can here be

1428: attempted but is expensive --- the incorporation of XOR provides

1429: significant improvements in complexity.

1430: 

1431: \subsection{Related Work}

1432: 

1433: The properties of first-order temporal logics have been studied, for

1434: example, in~\cite{HWZ00,HKKWZ03}. Proof methods for the monodic

1435: fragment of first order-temporal logics, based on resolution or

1436: tableaux have been proposed in

1437: ~\cite{DFK03:ToCL,KDDFH05:IC,Kontchakovetal02}.

1438: 

1439: Model checking for parameterised and infinite state-systems is

1440: considered in~\cite{AbdullaJNdS04}. Formulae are translated into to a

1441: B\"uchi transducer with regular accepting states. Techniques from

1442: regular model checking are then used to search for models. This

1443: approach has been applied to several algorithms verifying safety

1444: properties and some liveness properties.

1445: 

1446: Constraint based verification using counting

1447: abstractions~\cite{delzanno00automatic,Del03,esparza99verification},

1448: provides complete procedures for checking safety properties of

1449: broadcast protocols.  However, such approaches

1450: \begin{itemize}

1451: \item have theoretically non-primitive recursive upper bounds for

1452:   decision procedures (although they work well for small, interesting,

1453:   examples) --- in  our case the upper bounds are definitely

1454:   primitive-recursive;

1455: 

1456: \item are not suitable (or, have not been used) for asynchronous systems

1457:   with delayed broadcast --- it is not clear how to adapt these

1458:   methods for such systems; and 

1459: 

1460: \item typically lead to undecidable problems if applied to liveness

1461:   properties. 

1462: \end{itemize}

1463: 

1464: \subsection{Future Work}

1465: 

1466: Future work involves exploring further the framework described in this

1467: paper in particular the development of an implementation to prove

1468: properties of protocols in practice. Further, we would like to see if we

1469: can extend the range of systems we can tackle beyond the monodic fragment.

1470: 

1471: We also note that some of the variations we might desire to include in

1472: Section~\ref{sec:var} can lead to undecidable fragments. However, for

1473: some of these variations, we have correct although (inevitably) incomplete

1474: methods, see~\cite{FKL06:VISSAS}. We wish to explore these boundaries

1475: further. 

1476: 

1477: 

1478: 

1479: % Beyond monodicity? Non-monodic \fotl{}-XOR? Can XOR constraints be used

1480: % in such a way that we are not able to specify a tiling argument

1481: % within, for example, \fotl{} formulae with 2 free variables?

1482: 

1483: %\bibliography{abbreviations,automata,theorem-proving,branching,ours,knowledge,tl,logic,actors,dai,os,modal,object,languages,architectures,ai,atal}

1484: %\bibliographystyle{latex8}

1485: 

1486: \begin{thebibliography}{10}\setlength{\itemsep}{-.8891ex}%\small

1487: 

1488: \bibitem{AbdullaJNdS04}

1489: P. A. Abdulla, B. Jonsson, M. Nilsson, J. d'Orso, and M. Saksena.

1490: \newblock {Regular Model Checking for LTL(MSO)}.

1491: \newblock In {\em Proc. 16th International Conference on Computer Aided

1492:   Verification (CAV)}, volume 3114 of {\em LNCS},

1493:   pages 348--360. Springer, 2004.

1494: 

1495: \bibitem{AbdullaJRS06}

1496: P. A. Abdulla, B. Jonsson, A. Rezine, and M. Saksena.

1497: \newblock {Proving Liveness by Backwards Reachability}.

1498: \newblock In {\em Proc. 17th International Conference on Concurrency Theory

1499:   (CONCUR)}, volume 4137 of {\em LNCS}, pages

1500:   95--109. Springer, 2006.

1501: 

1502: \bibitem{AFWZ02}

1503: A. Artale, E. Franconi, F. Wolter, and M. Zakharyaschev.

1504: \newblock A Temporal Description Logic for Reasoning over Conceptual Schemas

1505:   and Queries.

1506: \newblock In {\em Proc. European Conference on Logics in Artificial

1507:   Intelligence (JELIA)}, volume 2424 of {\em LNCS}, pages 98--110. Springer, 2002.

1508: 

1509: \bibitem{BGG97}

1510: E. B{\"o}rger, E Gr{\"a}del, and Yu. Gurevich.

1511: \newblock {\em The Classical Decision Problem}.

1512: \newblock Springer, 1997.

1513: 

1514: \bibitem{BDFL02:LPAR} J. Brotherston, A. Degtyarev, M. Fisher, and

1515:   A. Lisitsa.  \newblock {Implementing Invariant Search via Temporal

1516:     Resolution}.  \newblock In {\em Proc. International Conference on

1517:     Logic for Programming, Artificial Intelligence, and Reasoning

1518:     (LPAR)}, volume 2514 of {\em LNCS},

1519:   pages 86--101. Springer Verlag, 2002.  

1520: 

1521: \bibitem{Clarke00:MC}

1522: E. Clarke, O. Grumberg, and D. Peled.

1523: \newblock {\em Model Checking}.

1524: \newblock MIT Press, Dec. 1999.

1525: 

1526: \bibitem{DFK03:ToCL}

1527: A. Degtyarev, M. Fisher, and B. Konev.

1528: \newblock {Monodic Temporal Resolution}.

1529: \newblock {\em ACM Transactions on Computational Logic}, 7(1):108--150, January

1530:   2006. (\texttt{ arXiv:cs.LO/0306041})

1531: 

1532: \bibitem{DFL02:StudiaLogica}

1533: A. Degtyarev, M. Fisher, and A. Lisitsa.

1534: \newblock {Equality and Monodic First-Order Temporal Logic}.

1535: \newblock {\em Studia Logica}, 72(2):147--156, Nov. 2002.

1536: 

1537: \bibitem{delzanno00automatic}

1538: G. Delzanno.

1539: \newblock Automatic Verification of Parameterized Cache Coherence Protocols.

1540: \newblock In {\em Proc. 12th International Conference on Computer Aided Verification

1541:   (CAV)}, volume 1855 of {\em LNCS}, pages 53--68, 2000.

1542: 

1543: \bibitem{Del03}

1544: G. Delzanno.

1545: \newblock Constraint-based verification of parametrized cache coherence

1546:   protocols.

1547: \newblock {\em Formal Methods in System Design}, 23(3):257--301, 2003.

1548: 

1549: \bibitem{Dix05}

1550: C. Dixon.

1551: \newblock {Using Temporal Logics of Knowledge for Specification and

1552:   Verification--a Case Study}.

1553: \newblock {\em Journal of Applied Logic}, 4(1): 50-78, 2006.

1554: 

1555: 

1556: 

1557: \bibitem{DFFH04:TIME}

1558: C. Dixon, M.C. Fern\'{a}ndez-Gago, M. Fisher,  and W. van der Hoek.

1559: \newblock {Using  Temporal Logics of Knowledge in the Formal Verification of

1560: Security Protocols.}

1561: \newblock In {\em Proc. International Symposium on Temporal Representation and

1562:   Reasoning (TIME)}, pages 148--151, 2004. IEEE CS Press,

1563: 

1564: 

1565: \bibitem{DFK06:TIME}

1566: C. Dixon, M. Fisher, and B. Konev.

1567: \newblock {Is There a Future for Deductive Temporal Verification?}

1568: \newblock In {\em Proc. International Symposium on Temporal Representation and

1569:   Reasoning (TIME)}, pages 11--18, 2006. IEEE CS Press.

1570: 

1571: \bibitem{DFK07:IJCAI}

1572: C. Dixon, M. Fisher, and B. Konev.

1573: \newblock {Tractable Temporal Reasoning}.

1574: \newblock In {\em Proc. International Joint Conference on Artificial

1575:   Intelligence (IJCAI)}. AAAI Press, 2007.

1576: 

1577: \bibitem{DFW97:JLC}

1578: C. Dixon, M. Fisher, and M. Wooldridge.

1579: \newblock {R}esolution for {T}emporal {L}ogics of {K}nowledge.

1580: \newblock {\em Journal of Logic and Computation}, 8(3):345--372, 1998.

1581: 

1582: \bibitem{emerson:90a}

1583: E. A. Emerson.

1584: \newblock {T}emporal and {M}odal {L}ogic.

1585: \newblock In J. van Leeuwen, editor, {\em Handbook of Theoretical Computer

1586:   Science}, pages 996--1072. Elsevier, 1990.

1587: 

1588: \bibitem{esparza99verification} J. Esparza, A. Finkel, and R. Mayr.

1589:   \newblock {On the Verification of Broadcast Protocols}.  \newblock

1590:   In {\em Proc.\ 14th {IEEE} Symposium on Logic in Computer Science

1591:     (LICS)}, pages 352--359. IEEE CS Press, 1999.

1592: 

1593: \bibitem{fdp01}

1594: M. Fisher, C. Dixon, and M. Peim.

1595: \newblock {Clausal Temporal Resolution}.

1596: \newblock {\em ACM Transactions on Computational Logic}, 2(1):12--56, Jan.

1597:   2001. (\texttt{  arXiv:cs.LO/9907032})

1598: 

1599: \bibitem{FKL06:VISSAS}

1600: M. Fisher, B. Konev, and A. Lisitsa.

1601: \newblock Practical Infinite-state Verification with Temporal Reasoning.

1602: \newblock In {\em Verification of Infinite State Systems and Security}. IOS Press, January 2006.

1603: 

1604: \bibitem{GKKWZ03}

1605: D. Gabelaia, R. Kontchakov, A. Kurucz, F. Wolter, and M. Zakharyaschev.

1606: \newblock On the Computational Complexity of Spatio-Temporal Logics.

1607: \newblock In {\em Proc. 16th International Florida Artificial

1608:   Intelligence Research Society Conference (FLAIRS)}, pages 460--464. AAAI

1609:   Press, 2003.

1610: 

1611: \bibitem{GHDFK05:JAR}

1612: M.-C. F. Gago, U. Hustadt, C. Dixon, M. Fisher, and B. Konev.

1613: \newblock {First-Order Temporal Verification in Practice}.

1614: \newblock {\em {Journal of Automated Reasoning}}, 34(3):295--321, 2005.

1615: 

1616: \bibitem{Hodkinson:Packed}

1617: I. Hodkinson.

1618: \newblock {Monodic Packed Fragment with Equality is Decidable}.

1619: \newblock {\em Studia Logica}, 72(2):185--197, 2002.

1620: 

1621: \bibitem{HKKWZ03}

1622: I. Hodkinson, R. Kontchakov, A. Kurucz, F. Wolter, and M. Zakharyaschev.

1623: \newblock On the Computational Complexity of Decidable Fragments of First-Order

1624:   Linear Temporal Logics.

1625: \newblock In {\em Proc. International Symposium on Temporal

1626:   Representation and Reasoning (TIME)}, pages 91--98. IEEE CS Press, 2003.

1627: 

1628: \bibitem{HWZ00}

1629: I. Hodkinson, F. Wolter, and M. Zakharyashev.

1630: \newblock {Decidable Fragments of First-Order Temporal Logics}.

1631: \newblock {\em Annals of Pure and Applied Logic}, 2000.

1632: 

1633: %% \bibitem{HDSFMH2001c}

1634: %% U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.-J. Meyer, and W. van der

1635: %%   Hoek.

1636: %% \newblock {Verification Within the KARO Agent Theory}.

1637: %% \newblock In Rouff et al. \cite{FAABSbook:06}.

1638: 

1639: \bibitem{HKRV04:IJCAR}

1640: U. Hustadt, B. Konev, A. Riazanov, and A. Voronkov.

1641: \newblock {TeMP: A Temporal Monodic Prover}.

1642: \newblock In {\em Proc. 2nd International Joint Conference on Automated Reasoning (IJCAR)},

1643:   volume 3097 of {\em LNAI}, pages 326--330. Springer, 2004.

1644: 

1645: \bibitem{KDDFH05:IC}

1646: B. Konev, A. Degtyarev, C. Dixon, M. Fisher, and U. Hustadt.

1647: \newblock Mechanising First-Order Temporal Resolution.

1648: \newblock {\em Information and Computation}, 199(1-2):55--86, 2005.

1649: 

1650: \bibitem{Kontchakovetal02}

1651: R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev.

1652: \newblock {Temoralising Tableaux}.

1653: \newblock {\em Studia Logica}, 76(1):91--134, 2004.

1654: 

1655: \bibitem{Lynch96:book}

1656: N. Lynch. 

1657: \newblock {\em Distributed Algorithms}.

1658: \newblock Morgan Kaufmann Publishers, San Mateo, CA, 1996.

1659: 

1660: \bibitem{maidl01unifying}

1661: M. Maidl.

1662: \newblock A Unifying Model Checking Approach for Safety Properties of

1663:   Parameterized Systems.

1664: \newblock {\em LNCS}, 2102:311--323, 2001.

1665: 

1666: \bibitem{Merz:Incomp:1992}

1667: S. Merz.

1668: \newblock Decidability and Incompleteness Results for First-Order Temporal

1669:   Logic of Linear Time.

1670: \newblock {\em Journal of Applied Non-Classical Logics}, 2:139--156, 1992.

1671: 

1672: % \bibitem{FAABSbook:06}

1673: % C. Rouff, M. Hinchey, J. Rash, W. Truszkowski, and D. Gordon-Spears, editors.

1674: %\newblock {\em Agent Technology from a Formal Perspective}.

1675: %\newblock NASA Monographs in Systems and Software Engineering. Springer-Verlag,

1676: %  New York, USA, 2006.

1677: 

1678: \bibitem{SturmW02}

1679: H. Sturm and F. Wolter.

1680: \newblock {A Tableau Calculus for Temporal Description Logic: the Expanding

1681:   Domain Case}.

1682: \newblock {\em Journal of Logic and Computation}, 12(5):809--838, 2002.

1683: 

1684: \bibitem{WZ01DecModal}

1685: F. Wolter and M. Zakharyaschev.

1686: \newblock {Decidable Fragments of First-Order Modal Logics}.

1687: \newblock {\em Journal of Symbolic Logic}, 66:1415--1438, 2001.

1688: 

1689: \bibitem{WZ:APAL:AxMono}

1690: F. Wolter and M. Zakharyaschev.

1691: \newblock Axiomatizing the Monodic Fragment of First-Order Temporal Logic.

1692: \newblock {\em Annals of Pure and Applied Logic}, 118(1-2):133--145, 2002.

1693: 

1694: \end{thebibliography}

1695: \end{document}

1696: