1: %%% $Id: main-regular.tex,v 1.16 2006/06/21 12:10:57 bertrand Exp $

2: 

3: \documentclass[runningheads,envcountsect,envcountsame]{llncs}

4: %\usepackage{subfigure}

5: \usepackage{floatflt}

6: 

7: \usepackage{pslatex}

8: \usepackage[T1]{fontenc}

9: \usepackage{color}

10: 

11: 

12: \usepackage{floatflt}

13: \usepackage{amsmath}

14: %\usepackage{amsthm}

15: \usepackage{amsfonts}

16: \usepackage{amssymb}

17: \usepackage{pslatex}

18: %\usepackage{gastex}

19: %\usepackage{theorem}

20: \usepackage{stmaryrd}

21: 

22: %%% TEXEXPAND: INCLUDED FILE MARKER ./macros.tex

23: %%% $Id: macros.tex,v 1.15 2006/06/14 08:24:47 bertrand Exp $

24: 

25: \newtheorem{fact}[theorem]{Fact}{\bfseries}{\itshape}

26: 

27: \def\ldouble{\langle\!\!\langle}

28: \def\rdouble{\rangle\!\!\rangle}

29: 

30: \newcommand{\Ende}{\qed} 

31: 

32: \newcommand{\lfp}{\mathrm{lfp}}

33: \newcommand{\gfp}{\mathrm{gfp}}

34: \newcommand{\Cu}{C_{\uparrow}}

35: \newcommand{\Cd}{C_{\downarrow}}

36: \newcommand{\Ku}{K_{\uparrow}}

37: \newcommand{\Kd}{K_{\downarrow}}

38: \newcommand\Pre{{\mathit{Pre}}}

39: \newcommand\Post{{\mathit{Post}}}

40: \newcommand\wPre{{\widetilde{\Pre}}}

41: 

42: % Some names for math symbols

43: %============================

44: \newcommand{\Real}{{\mathbb{R}}} % use the right fonts

45: \newcommand{\Realplus}{{\Real_{\geq 0}}}

46: \newcommand{\Realpos}{{\Real_{> 0}}}

47: \newcommand{\Nat}{{\mathbb{N}}} % use the right fonts

48: \renewcommand{\epsilon}{\varepsilon} % we want all epsilons the same

49: \renewcommand{\setminus}{\smallsetminus} % we want all setminus the same

50: \renewcommand{\phi}{\varphi} % we want all phis the same

51: \newcommand{\sat}{\models}      % symbols for |=

52: \newcommand{\impl}{\Rightarrow} % => implication

53: 

54: \newcommand{\CTL}{{\mathit{CTL}}}

55: \newcommand{\CTLstar}{{\CTL}^*}

56: 

57: % Gadgets for our example LCS's

58: %==============================

59: \newcommand{\F}{{{\mathcal{F}}}}

60: \newcommand{\Fair}{{{\mathcal{F}}}}

61: \newcommand{\fair}{{{\mathit{fair}}}}

62: \newcommand{\FairSafe}{\Safe_{\Fair}}

63: \newcommand{\TBoxAFr}{T_{\Box \Diamond A}^\Fair}

64: 

65: \newcommand{\Cond}{{{\mathit{Cond}}}}

66: \newcommand{\Goal}{{{\mathit{Goal}}}}

67: \newcommand{\Final}{{{\mathit{Final}}}}

68: \newcommand{\Init}{\mathit{Init}}

69: 

70: 

71: 

72: \def\U{{\mathcal{U}}} % a scheduler, or strategy

73: 

74: \newcommand{\A}{{\mathcal{A}}}  % A = a Buchi or Streett automaton

75: \renewcommand{\c}{{c}} % c = a channel

76: \newcommand{\C}{{\mathsf{C}}} % C = a set of channels

77: \renewcommand{\L}{{\mathcal{L}}} % L = a LCS

78: \newcommand{\N}{{\mathcal{N}}}  % N == a NPLCS

79: \newcommand{\Pcal}{{{\mathcal{P}}}} % P in mathcal, as in powerset

80: \newcommand{\PR}{{{\mathbb{P}}}} % P in bb for the measure on the sigma-field

81: \newcommand{\bfP}{{\textbf{P}}} % P in bold for the Prob Matrix in the chain

82: \newcommand{\R}{{\mathcal{R}}}   % the set of regions\newcommand{\W}{{\mathcal{W}}}  

83: \renewcommand{\S}{{\mathcal{S}}}  

84: \newcommand{\W}{{\mathcal{W}}}

85: \newcommand{\Until}{{\mathsf{U}}}

86: \newcommand{\Next}{{\mathsf{X}}}

87: \newcommand{\Release}{{\mathsf{R}}}

88: %\newcommand{\Eventually}{{\mathsf{F}}}

89: \newcommand{\Lang}{{\mathsf{TL}}}

90: 

91: \newcommand{\Acc}{{\mathit{Acc}}}

92: \newcommand{\Conf}{{\mathit{Conf}}}

93: \newcommand{\env}{{\textit{env}}}

94: \newcommand{\false}{{\mathsf{false}}}

95: \newcommand{\Free}{{\textit{Free}}}

96: \newcommand{\MC}{{\mathit{MC}}} % Markov Chain

97: \newcommand{\LTS}{{\mathit{LTS}}} % Labeled Transition System

98: \newcommand{\MDP}{{\mathit{MDP}}} % Markovian Decision Process

99: \newcommand{\Mess}{{\mathsf{M}}} % M = set of messages

100: %\newcommand{\M}{{\mathsf{M}}} %idem

101: \newcommand{\op}{{\mathit{op}}}

102: \newcommand{\Prom}{{\mathit{Prom}}}

103: \newcommand{\Safe}{{\mathit{Safe}}}

104: \newcommand{\true}{{\mathsf{true}}}

105: 

106: %% Arrow for transitions with label (variable length)

107: %====================================================

108: \newcommand{\overto}[1]{\xrightarrow{\!\!#1\!\!}}

109: \newcommand{\step}[1]{\overto{#1}} % handy synonym

110: \def\leadsto{\rightsquigarrow}

111: \newcommand{\perf}{\mathrm{perf}}

112: 

113: % definitions

114: %============

115: \newcommand{\egdef}{\stackrel{\mbox{\begin{scriptsize}def\end{scriptsize}}}{=}}

116: \newcommand{\equivdef}{\stackrel{\mbox{\begin{scriptsize}def\end{scriptsize}}}{\Leftrightarrow}}

117: \newcommand{\eqdef}{\stackrel{\mbox{\begin{scriptsize}def\end{scriptsize}}}{\equiv}}

118: 

119: 

120: \newcommand{\tuple}[1]{\langle #1 \rangle}

121: \newcommand{\up}{\mathord{\uparrow}}

122: \newcommand{\sem}[1]{\llbracket #1 \rrbracket}

123: \newcommand{\rep}[1]{\sem{#1}}

124: \newcommand{\ex}[1]{\ldouble #1 \rdouble}

125: 

126: \def\BPre{{\it BPre}}

127: \def\APre{{\it APre}}

128: \def\Ant{\widehat{\it Pre}}

129: 

130: %\newcommand{\Aforall}{{\text A}}

131: %\newcommand{\Eexists}{{\text E}}

132: 

133: %%% Local Variables: 

134: %%% mode: latex

135: %%% TeX-master: "main-regular"

136: %%% End: 

137: %%% TEXEXPAND: END FILE ./macros.tex

138: 

139: 

140: 

141: 

142: \begin{document}

143: 

144: %%% TEXEXPAND: INCLUDED FILE MARKER ./header.tex

145: %%% $Id: header.tex,v 1.5 2006/05/12 20:44:30 phs Exp $ -*-LaTeX-*-

146: 

147: \title{On computing fixpoints in well-structured regular model checking,

148:   with applications to lossy channel systems}

149: \titlerunning{On computing fixpoints, with applications to lossy channel systems}

150: 

151: \author{  C. Baier\inst{1}

152: \and

153: 	  N. Bertrand\inst{2}

154: \and

155: 	  Ph. Schnoebelen\inst{2}

156: }

157: \institute{

158: 	  Universit{\"a}t Bonn, Institut f{\"u}r Informatik I, Germany

159: \and

160: 	  LSV, ENS de Cachan \& CNRS, France

161: }

162: 

163: 

164: \maketitle

165: 

166: 

167: %% \begin{center}

168: %% \fbox{\textbf{Draft version of \today.}}

169: %% \end{center}

170: 

171: 

172: %% Local Variables:

173: %% TeX-master: "main-regular"

174: %% End:

175: %%% TEXEXPAND: END FILE ./header.tex

176: 

177: %%% TEXEXPAND: INCLUDED FILE MARKER ./abstract.tex

178: %%% $Id: abstract.tex,v 1.4 2006/05/02 09:21:40 phs Exp $

179: 

180: 

181: \begin{abstract}

182: We prove a general finite convergence theorem for ``upward-guarded''

183: fixpoint expressions over a well-quasi-ordered set. This has immediate

184: applications in regular model checking of well-structured systems, where a

185: main issue is the eventual convergence of fixpoint computations. In

186: particular, we are able to directly obtain several new decidability results

187: on lossy channel systems.

188: \end{abstract}

189: 

190: 

191: %%% Local Variables:

192: %%% mode: latex

193: %%% TeX-master: "main-regular"

194: %%% End:

195: 

196: % LocalWords:  fixpoint

197: %%% TEXEXPAND: END FILE ./abstract.tex

198: %%% TEXEXPAND: INCLUDED FILE MARKER ./sec-intro.tex

199: %%% $Id: sec-intro.tex,v 1.14 2006/05/12 20:44:30 phs Exp $

200: 

201: 

202: 

203: \section{Introduction}

204: %=====================

205: 

206: 

207: \emph{Regular model

208:   checking}~\cite{kesten2001,bouajjani2000b,voronkov-csl03} is a

209: popular paradigm for the symbolic verification of models with infinite

210: state space.  It has been applied to varied families of systems

211: ranging from distributed algorithms and channel systems to hybrid

212: systems and programs handling dynamic data structures.

213: 

214: In regular model checking, one works with regular sets of

215: states and handles them via

216: finite descriptions, e.g., finite-state automata or regular expressions. Models

217: amenable to regular model checking are such that, when $S\subseteq \Conf$

218: is regular, then $\Post(S)$ (or $\Pre(S)$), the set of 1-step successors

219: (resp., predecessors), is again a regular set that

220: can be computed effectively from $S$. Since regular sets are

221: closed under Boolean operations, one can\footnote{

222: %

223:    Actually, such symbolic computations are possible with any class of

224:    representation closed under, and providing algorithms for, $\Pre$ or

225:    $\Post$, Boolean operations, vacuity~\cite{kesten2001,henzinger2005}.

226: %

227: } try to compute the reachability set

228: $\Post^*(\Init)$, as the

229: limit of the sequence

230: \begin{gather}

231: \tag{*}

232: \label{eq-post*}

233: S_0 := \Init;

234: \quad

235: S_1 := S_0\cup\Post(S_0);

236: \quad

237: \ldots

238: \quad

239: S_{n+1} := S_n\cup\Post(S_n);

240: \quad

241: \ldots

242: \end{gather}

243: Since equality of regular sets is decidable, the computation of

244: \eqref{eq-post*} can contain a test that detects if the limit is reached in

245: finite time, i.e., if $S_{n+1}=S_n$ for some $n\in\Nat$,

246: 

247: 

248: With infinite-state models, the main difficulty is \emph{convergence}. It

249: is very rare that a fixpoint computation like \eqref{eq-post*} converges in

250: finite time, and innovative techniques that try to compute directly, or guess and

251: check, or approximate the limit set $\Post^*(\Init)$, are currently under

252: active

253: scrutiny~\cite{BLW03,boigelot2003,bouajjani2004,habermehl04,BFLS-atva2005}.

254: 

255: \emph{Well-structured transition systems} (WSTS) are a generic family of

256: models for which the co-reachability set $\Pre^*(\Final)$ can be computed

257: symbolically with a backward-chaining version of

258: \eqref{eq-post*}~\cite{abdulla2000c,finkel98b}. For WSTS's, convergence of

259: the fixpoint computation is ensured by WQO theory: one handles

260: upward-closed sets, and increasing sequences of upward-closed sets always

261: converge in finite time when the underlying ordering is a

262: well-quasi-ordering (a WQO), as is the case with WSTS's.

263: 

264: Computing $\Pre^*(\Final)$ for reachability analysis is just a special

265: case of fixpoint computation. When dealing with richer temporal

266: properties, one is interested in more complex fixpoints. E.g., the set

267: of states satisfying the CTL formula $\exists[\Cond\Until\Goal]$ is

268: definable via a least-fixpoint expression: $\mu

269: X.\Goal\cup(\Cond\cap\Pre(X))$. For game-theoretic properties, similar

270: fixpoints are involved. E.g., the states from which the first player

271: in a turn-based game can enforce reaching a goal is given by $\mu

272: X.\Goal\cup\Pre(\overline{\Pre(\overline{X})})$.

273: 

274: 

275: \paragraph*{\bf Our contribution.}

276: %=================================

277: In this paper, we define a notion of $\mu$-expressions where recursion is

278: guarded by upward-closure operators, and give a general finite convergence

279: theorem for all such expressions. The consequence is that these fixpoint

280: expressions can be evaluated symbolically by an iterative procedure. The

281: guarded fragment we isolate is very relevant for the verification of

282: well-structured transition systems as we demonstrate by providing several

283: new decidability results on channel systems.

284: 

285: \paragraph*{\bf Related work.}

286: %=============================

287: Henzinger \textit{et al.} give general conditions for the convergence of

288: fixpoints computations for temporal~\cite{henzinger2005} or

289: game-theoretic~\cite{alfaro2001b} properties, but the underlying framework

290: (finite quotients) is different and has different applications (timed and

291: hybrid systems). Our applications to well-structured transition systems

292: generalize results from ~\cite{abdulla2003b,raskin03,raskin05,KucSch-TCS}

293: that rely on more ad-hoc finite convergence lemmas.

294: 

295: 

296: 

297: 

298: %%% Local Variables:

299: %%% mode: latex

300: %%% TeX-master: "main-regular"

301: %%% End:

302: 

303: % LocalWords:  fixpoint WQO WSTS's fixpoints Henzinger al tex phs eq WSTS CTL

304: % LocalWords:  bertrand

305: %%% TEXEXPAND: END FILE ./sec-intro.tex

306: 

307: %%% TEXEXPAND: INCLUDED FILE MARKER ./sec-guarded-mucalculus.tex

308: %%% $Id: sec-guarded-mucalculus.tex,v 1.15 2006/05/11 08:12:01 phs Exp $

309: 

310: \section{A guarded mu-calculus}

311: %==============================

312: \label{sec-guarded-mucalculus}

313: 

314: 

315: We assume basic understanding of $\mu$-calculi techniques (otherwise

316: see~\cite{arnold2001}) and of well-quasi-ordering (WQO) theory (otherwise

317: see~\cite{milner85,kruskal72}, or simply~\cite[sect.~2.1]{finkel98b}).

318: 

319: 

320: Let $(W,\sqsubseteq)$ be a well-quasi-ordered set. A subset $V$ of $W$ is

321: \emph{upward-closed} if $w\in V$ whenever $v\sqsubseteq w$ for some $v\in

322: V$. From WQO theory, we mostly need the following result:

323: \begin{fact}[Finite convergence]

324: \label{fact-fc}

325: If $V_0\subseteq V_1\subseteq V_2\subseteq \cdots$ is an infinite

326: increasing sequence of upward-closed subsets of $W$, then

327: for some index $k\in\Nat$, $\bigcup_{i\in\Nat}V_i =V_k$.

328: \end{fact}

329: 

330: The \emph{upward-closure} of $V\subseteq W$, denoted $\Cu(V)$, is the

331: smallest upward-closed set that contains $V$. The \emph{upward-kernel} of

332: $V$, denoted $\Ku(V)$, is the largest upward-closed set included in $V$.

333: There are symmetric notions of \emph{downward-closed} subset of $W$, of

334: \emph{downward-closure}, $\Cd(V)$, and of \emph{downward-kernel}, $\Kd(V)$,

335: of $V$. The complement of an upward-closed subset is downward-closed.

336: Observe that $\Cu(V)=V=\Ku(V)$ iff $V$ is upward-closed, and that $\Cu$ and

337: $\Kd$ (resp., $\Cd$ and $\Ku$) are dual:

338: \begin{xalignat}{2}

339: \label{eq-Cu-duality}

340:         W\setminus \Ku(V) &= \Cd(W\setminus V),

341:         &

342:         W\setminus \Kd(V) &= \Cu(W\setminus V).

343: \end{xalignat}

344: 

345: 

346: 

347: \paragraph*{\bf Monotonic region algebra.}

348: %----------------------------------------

349: In symbolic model-checking, a \emph{region algebra} is a family of

350: sets of states (subsets of $W$) that is closed under Boolean and other

351: operators like images or inverse images~\cite{henzinger2005}.

352: 

353: Here we consider regions generated by a family $O=\{o_1,o_2,\ldots\}$ of

354: (monotonic) operators. By a $k$-ary \emph{operator}, we mean a monotonic

355: mapping $o:(2^W)^k\to 2^W$ that associates a subset

356: $o(V_1,\ldots,V_k)\subseteq W$ with any $k$ subsets $V_1,\ldots,V_k$.

357: Monotonicity means that $o(V_1,\ldots,V_k)\subseteq o(V'_1,\ldots,V'_k)$

358: when $V_i\subseteq V'_i$ for $i=1,\ldots,k$. We allow nullary operators,

359: i.e., fixed subsets of $W$. Finally, we require that $O$ contains at least

360: four special unary operators: $\Cu$, $\Cd$, $\Ku$, $\Kd$, and two special

361: nullary operators: $\emptyset$ and $W$.

362: 

363: The \emph{region algebra generated by $O$}, denoted with $\R_O$, or simply

364: $\R$, is the set of all the subsets of $W$, called \emph{regions}, that can

365: be obtained by applying operators from $O$ on already constructed regions,

366: starting with nullary operators. Equivalently, $\R$ is the least subset of

367: $2^W$ that is closed under $O$.

368: 

369: We say the region algebra generated by $O$ is \emph{effective} if there are

370: algorithms implementing the operators in $O$ and an effective membership

371: algorithm saying whether $w\in R$ for some $w\in W$ and some region $R\in\R_O$.

372: Such effectiveness assumptions presuppose a finitary encoding of regions

373: and elements of $W$: if there are several possible encodings for a same

374: region, we assume an effective equality test.

375: 

376: 

377: \paragraph*{\bf Extending the region algebra with fixpoints.}

378: %-----------------------------------------------------------

379: Let $\chi = \{X_1,X_2,\cdots\}$ be a countable set of variables.

380: $L_\mu(W,\sqsubseteq,O)$, or shortly $L_\mu$ when $(W,\sqsubseteq)$ and $O$

381: are clear from the context, is the set of \emph{$O$-terms with least and

382: greatest fixpoints} given by the following abstract syntax:

383: \begin{gather*}

384: L_\mu \ni \phi,\psi  \ ::=

385:                o(\phi_1,\ldots,\phi_k)          \ \big| \

386:                X                                \ \big| \

387:                \mu X.\phi                       \ \big| \

388:                \nu X. \phi                      \ \big| \

389:                \Cu(\phi)                        \ \big| \

390:                \Cd(\phi)                        \ \big| \

391:                \Ku(\phi)                        \ \big| \

392:                \Kd(\phi)

393: \end{gather*}

394: where $X$ runs over variables from $\chi$, and $o$ over operators from $O$.

395: $\mu X.\phi$ and $\nu X.\phi$ are fixpoint expressions. Free and bound

396: occurrences of variables are defined as usual. We assume that no variable

397: has both bound and free occurrences in some $\phi$, and that no two

398: fixpoint subterms bind the same variable: this can always be ensured by

399: renaming bound variables. (The abstract syntax for $L_\mu$ could be shorter

400: but we wanted to stress that $\Cu$, $\Cd$, $\Ku$, and $\Kd$ are required to

401: be present in $O$.)

402: 

403: The meaning of $L_\mu$ terms is as expected: an \emph{environment} is a

404: mapping $\env : \chi \to 2^W$ that interprets each variable $X \in \chi$ as

405: a subset of $W$. Given $\env$, a term $\phi\in L_\mu$ denotes a subset of

406: $W$, written $\rep{\phi}_\env$ and defined by induction on the structure of

407: $\phi$:

408: \begin{xalignat*}{2}

409: \rep{X}_\env & \egdef  \env(X)

410: &

411: \rep{o(\phi_1,\ldots,\phi_k)}_{\env} & \egdef

412:    o(\rep{\phi_1}_\env,\ldots,\rep{\phi_k}_\env)

413: \\

414: \rep{\Cu( \phi)}_\env & \egdef

415:    \Cu\bigl( \rep{\phi}_{\env} \bigr)

416: &

417: \rep{\Cd( \phi)}_\env & \egdef

418:    \Cd (\rep{\phi}_{\env})

419: \\

420: \rep{\Ku (\phi)}_\env & \egdef

421:    \Ku( \rep{\phi}_{\env})

422: &

423: \rep{\Kd (\phi)}_\env & \egdef

424:    \Kd\bigl( \rep{\phi}_{\env}\bigr)

425: \\

426: \rep{\mu X. \phi}_\env & \egdef  \lfp \bigl(\Omega[\phi,X,\env]

427: \bigr)

428: \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!

429: \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!

430: \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!

431: &

432: \rep{\nu X. \phi}_\env & \egdef  \gfp \bigl(\Omega[\phi,X,\env]

433: \bigr)

434: \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!

435: \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!

436: \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!

437: \end{xalignat*}

438: where $\Omega[\phi,X,\env] : 2^W \to 2^W$ is a unary operator defined by

439: $\Omega[\phi,X,\env](V) \egdef \rep{\phi}_{\env[X:= V]}$, using the

440: standard variant notation ``$\env[X:=V]$'' for the environment that agrees

441: with $\env$ everywhere except on $X$ where it returns $V$. As usual,

442: $\rep{\phi}_\env$ does not depend on $\env(X)$ if $X$ is not free in

443: $\phi$, so that we may shortly write $\rep{\phi}$ when $\phi$ is a closed

444: term, i.e., a term with no free variables.

445: 

446: We recall that the semantics of the fixpoint terms is well-defined since,

447: for every $\phi$, $X$ and $\env$, $\Omega[\phi,X,\env]$ is monotonic (and

448: since $(2^W,\subseteq)$ is a complete lattice). Moreover, if $\env$ and

449: $\env'$ are such that $\env(X)\subseteq\env'(X)$ for all $X\in\chi$,

450: shortly written $\env\subseteq\env'$, then $\lfp(\Omega[\phi,X,\env])

451: \subseteq \lfp(\Omega[\phi,X,\env'])$ and $\gfp(\Omega[\phi,X,\env])

452: \subseteq \gfp(\Omega[\phi,X,\env'])$.

453: 

454: 

455: \begin{definition}[Upward- and downward-guardedness]

456: \begin{enumerate}

457: \item A variable $X$ is \emph{upward-guarded} in $\phi$ if all free

458:   occurrences of $X$ in $\phi$ are in the scope of either a $\Cu$ or a

459:   $\Ku$ operator, i.e., appear in a subterm of the form $\Cu(\psi)$ or $\Ku

460:   (\psi)$.

461: \item Dually, $X$ is \emph{downward-guarded} in $\phi$ if all its

462:   free occurrences are in the scope of a

463:   $\Cd$ or a $\Kd$ operator.

464: \item A term $\phi$ is \emph{guarded} if all its least-fixpoint subterms

465: $\mu X.\psi$ have $X$ upward-guarded in $\psi$, and all its

466:   greatest-fixpoint subterms $\nu X.\psi$ have $X$ downward-guarded in $\psi$.

467: \end{enumerate}

468: \end{definition}

469: 

470: 

471: Given some $\phi$, $X$ and $\env$, the approximants of

472: $\lfp(\Omega[\phi,X,\env])$ are given by the sequence $(M_i)_{i\in\Nat}$ of

473: subsets of $W$ defined inductively with $M_0= \emptyset$ and $M_{i+1} =

474: \rep{\phi}_{\env[X:=M_i]}$. Monotonicity yields

475: \begin{gather}

476: \label{eq-mon}

477: M_0 \subseteq M_1 \subseteq M_2 \subseteq \cdots \subseteq \lfp(\Omega[\phi,X,\env]).

478: \end{gather}

479: Similarly we define $(N_i)_{i\in\Nat}$ by $N_0 = W$ and $N_{i+1} =

480: \rep{\phi}_{\env[X:=N_i]}$, so that

481: \begin{gather}

482: N_0 \supseteq N_1 \supseteq N_2 \supseteq \cdots \supseteq \gfp(\Omega[\phi,X,\env]).

483: \end{gather}

484: 

485: 

486: \begin{lemma}[Finite convergence of approximants]

487: \label{lem-finite-approx}

488: If $X$ is upward-guarded in $\phi$, then there exists an index $k\in\Nat$ such that

489: \begin{gather}

490: \label{eq-pfa}

491: \rep{\mu X.\phi}_\env =  M_k = M_{k+1} = M_{k+2} = \ldots

492: \end{gather}

493: Dually, if $X$ is downward-guarded in $\phi$, then there exists a $k'\in\Nat$

494: such that

495: \begin{gather}

496: \rep{\nu X.\phi}_\env = N_{k'} = N_{k'+1} = N_{k'+2} = \ldots

497: \end{gather}

498: \end{lemma}

499: \begin{proof}

500: We only prove the first half since the other half is dual. Let

501: $\psi_1,\ldots,\psi_m$ be the maximal subterms of $\phi$ that are

502: immediately under the scope of a $\Cu$ or a $\Ku$ operator. Then $\phi$ can

503: be decomposed under the form

504: \begin{gather*}

505: \phi \:\equiv\: \Phi(\Uparrow \psi_1,\ldots,\Uparrow \psi_m)

506: \end{gather*}

507: where the context $\Phi(Y_1,\ldots,Y_m)$ uses fresh variables

508: $Y_1,\ldots,Y_m$ to be substituted in, and where $\Uparrow\psi_i$ is either

509: $\Cu(\psi_i)$ or $\Ku(\psi_i)$, depending on how $\psi_i$ appears in

510: $\phi$. In either case, and for any environment $\env'$, the set

511: $\rep{\Uparrow \psi_i}_{\env'}$ is upward-closed.

512: 

513: For $V_1,\ldots,V_m \subseteq W$ we shortly write

514: $\rep{\Phi}(V_1,\ldots,V_m)$ for $\rep{\Phi}_{\env[Y_1 :=

515: V_1,\ldots,Y_m:=V_m]}$. Since $X$ is upward-guarded in $\phi$, it has no

516: occurrence in $\Phi$, only in the $\psi_i$'s, so that

517: \begin{align*}

518:         M_{i+1} = \rep{\phi}_{\env[X:=M_i]} & =

519:          \rep{\Phi}(\rep{\Uparrow \psi_1}_{\env[X:=M_i]},\ldots,

520:             \rep{\Uparrow \psi_m}_{\env[X:=M_i]}) \\

521:         & =

522:          \rep{\Phi}(L_{i,1},\ldots, L_{i,m})

523: \end{align*}

524: writing $L_{i,j}$ for $\rep{\Uparrow\psi_j}_{\env[X:=M_i]}$. From

525: $M_0\subseteq M_1\subseteq M_2 \subseteq \cdots$, we deduce $L_{0,j}

526: \subseteq L_{1,j} \subseteq L_{2,j} \subseteq \cdots$ Since $\Ku$ and $\Cu$

527: return upward-closed sets, the $L_{i,j}$'s are upward-closed subsets of

528: $W$. For all $j=1,\ldots,m$, Fact~\ref{fact-fc} implies that there is an

529: index $k_j$ such that $L_{i,j} = L_{k_j,j}$ for all $i \geq k_j$. Picking

530: $K=\max(k_1,\ldots,k_j)$ gives for any $i\geq K$

531: \[

532: M_{i+1} = \rep{\Phi}(L_{i,1},\ldots, L_{i,m})

533:         = \rep{\Phi}(L_{k_1,1},\ldots,L_{k_m,m})

534:         = \rep{\Phi}(L_{K,1},\ldots,L_{K,m})

535:         = M_{K+1}.

536: \]

537: Thus, $\bigcup_{i\in\Nat}M_i=M_{K+1}=M_{K+2}$ and $M_{K+1}$ is a fixpoint

538: of $\Omega[\phi,X,\env]$, hence the least one thanks to \eqref{eq-mon}.

539: Picking $k=K+1$ satisfies \eqref{eq-pfa}.

540: %

541: \qed

542: \end{proof}

543: 

544: \paragraph*{\bf Regions with guarded fixpoints.}

545: %-----------------------------------------------

546: We can now prove our main result: subsets defined by $L_\mu$ terms are

547: regions (and can be computed effectively if the underlying region

548: algebra is effective).

549: 

550: By a \emph{region-environment} we mean an environment $\env : \chi \to \R$

551: that associates regions with variables. If $\env$ is a region-environment,

552: and $\phi$ has only free variables, i.e., has no fixpoints subterms, then

553: $\rep{\phi}_\env$ is a region.

554: 

555: \begin{theorem}

556: \label{th-guarded-effective}

557: If $\phi\in L_\mu$ is guarded and $\env$ is a region-environment then

558: $\rep{\phi}_\env$ is a region. Furthermore, if the region algebra is

559: effective, then $\rep{\phi}_\env$ can be computed effectively from $\phi$

560: and $\env$.

561: \end{theorem}

562: \begin{proof}

563: By structural induction on the structure of $\phi$. If $\phi=o()$ is a

564: nullary operator, the result holds by definition of the region algebra. If

565: $\phi = o(\phi_1,\cdots,\phi_k)$, the $\rep{\phi_i}_\env$'s are

566: (effectively) regions by induction hypothesis, so that $\rep{\phi}_\env$ is

567: an (effective) region too by definition. In particular, this argument

568: applies when $o$ is a nullary operator, or is one of the unary operators we

569: singled out: $\Cu$, $\Cd$, $\Ku$, and $\Kd$.

570: 

571: If $\phi = \mu X. \psi$, we can apply Lemma~\ref{lem-finite-approx} after

572: we have proved that each one of the approximants $M_0, M_1, M_2, \ldots$,

573: of $\rep{\phi}_\env$ are regions. In particular, $M_0=\emptyset$ is a

574: region, and if $M_i$ is a region, then $M_{i+1}=\rep{\psi}_{\env[X:=M_i]}$

575: is one too, since $\env'=\env[X:=M_i]$ is a region-environment, and since

576: by induction hypothesis $\rep{\psi}_{\env'}$ is a region when $\env'$ is a

577: region-environment. When $\R_O$ is effective, the $M_i$ can be computed

578: effectively, and one can detect when $M_k=M_{k+1}$ since region equality is

579: decidable by definition. Then $\rep{\phi}_\env = M_k$ can be computed

580: effectively. Finally, the case where $\phi=\nu X.\psi$ is dual.

581: %

582: \qed

583: \end{proof}

584: \begin{corollary}[Decidability for guarded $\L_\mu$ properties]

585: The following problems are decidable for effective

586:   monotonic region algebras:

587: \begin{description}

588: \item[Model-checking:]

589: ``Does  $w \in \rep{\phi}$?'' for a $w\in

590:  W$ and a closed and guarded $\phi\in L_\mu$.

591: \item[Satisfiability:]

592: ``Is  $\rep{\phi}$ non-empty?'' for a closed and guarded $\phi\in L_\mu$.

593: \item[Universality:]

594: ``Does  $\rep{\phi}=W$?'' for a closed and guarded $\phi\in L_\mu$.

595: \end{description}

596: \end{corollary}

597: 

598: 

599: \paragraph*{\bf A region algebra of regular languages.}

600: %======================================================

601: Consider $W=\Sigma^*$, the set of finite words over some finite alphabet

602: $\Sigma$. The \emph{subword ordering}, defined by ``$u\sqsubseteq v$ iff $u$

603: can be obtained by erasing some letters from $v$'', is a WQO (Higman's

604: Lemma). Regular languages over $\Sigma$ are a natural choice for regions:

605: observe that the closure operators $\Cu$ and $\Cd$ preserve regularity and

606: have effective implementations.\footnote{

607: %

608:   From a FSA for $R$, one obtains a FSA for $\Cu(R)$ simply by adding loops

609:   $q\step{a}q$ on all states $q$ of the FSA and for all letters

610:   $a\in\Sigma$. A FSA for $\Cd(R)$ is obtained by adding

611:   $\epsilon$-transitions $q\step{\epsilon}q'$ whenever there is a

612:   $q\step{a}q'$. From this, $\Ku$ and $\Kd$ can be implemented using

613:   \eqref{eq-Cu-duality}.

614: %

615: } Natural operators to be considered in $O$ are $\cup$ (union) and $\cap$

616: (intersection). However, any operation on languages that is monotonic,

617: preserve regularity, and has an effective implementation on regular

618: languages can be added. This includes concatenation (denoted $R.R'$),

619: star-closure (denote $R^*$), left- and right-residuals

620: ($R^{-1}R'\egdef\{v~|~\exists u\in R,uv\in R'\}$), shuffle product (denoted

621: $R \parallel R'$), reverse (denoted $\overleftarrow{R}$), conjugacy

622: ($\widetilde{R}\egdef\{vu~|~uv\in R\}$), homomorphic and

623: inverse-homomorphic images, and many more~\cite{perrin90}. Complementation

624: is not allowed in $O$ (it is not monotonic) but the duals of all

625: above-mentioned operators can be included in $O$ (without compromising

626: effectiveness) so that, for all practical purposes, complement can be used

627: with the restriction that bound variables in $L_\mu$ terms are under an

628: even number of complementations.

629: 

630: An application of Theorem~\ref{th-guarded-effective} is that, if $R_1$ and

631: $R_2$ are regular languages, then the language defined as $\mu X.\nu

632: Y.\bigl(\Ku\bigl[R_1 \parallel (X^*\cap \Cd(Y^{-1}\overleftarrow{X}\cap

633: X^{-1}R_2))\bigr]\bigr)$ is regular and a finite representation for it

634: (e.g., a regular expression or a minimal DFA) can be constructed from $R_1$

635: and $R_2$.

636: 

637: 

638: 

639: 

640: 

641: %%% Local Variables:

642: %%% mode: latex

643: %%% TeX-master: "main-regular"

644: %%% End:

645: 

646: % LocalWords:  WQO iff ary Kleene Fixpoint fixpoints fixpoint subformulae lfp

647: % LocalWords:  gfp Higman's mucalculus tex phs subterms subformula subterm eq

648: % LocalWords:  approximants mon pfa subword uv vu DFA

649: %%% TEXEXPAND: END FILE ./sec-guarded-mucalculus.tex

650: %%% TEXEXPAND: INCLUDED FILE MARKER ./sec-verif-LCS.tex

651: %%% $Id: sec-verif-LCS.tex,v 1.27 2006/05/13 10:46:50 phs Exp $

652: 

653: 

654: \section{Verification of lossy channel systems}

655: %===============================================

656: \label{sec-verif-LCS}

657: 

658: 

659: Theorem~\ref{th-guarded-effective} has several applications for regular

660: model checking of lossy channel systems~\cite{abdulla96b} (LCS) and other

661: families of well-structured systems~\cite{abdulla2000c,finkel98b}. In the

662: rest of this paper we concentrate on LCS's.

663: 

664: 

665: 

666: \subsection{Channel systems, perfect and lossy}

667: %----------------------------------------------

668: A channel system is a tuple $\L= (Q,\C,\Mess,\Delta)$ consisting of a

669: finite set $Q=\{p,q,\ldots\}$ of \emph{locations}, a finite set

670: $\C=\{c,\ldots\}$ of \emph{channels}, a finite \emph{message alphabet}

671: $\Mess=\{m,\ldots\}$ and a finite set $\Delta=\{\delta,\ldots\}$ of

672: \emph{transition rules}. Each transition rule has the form $q \step{\op} p$

673: where $\op$ is an \emph{operation}: $\c!m$ (sending message $m \in \Mess$

674: along channel $\c \in \C$), $\c?m$ (receiving message $m$ from channel

675: $\c$), or $\surd$ (an internal action to some process, no I/O-operation).

676: 

677: 

678: \paragraph*{\bf Operational semantics.}

679: %-------------------------------------

680: Let $\L= (Q,\C,\Mess,\Delta)$ be a channel system. A \emph{configuration}

681: (also, a \emph{state}) is a pair $\sigma = (q,w)$ where $q \in Q$ is a

682: location and $w : \C \to \Mess^*$ is a channel valuation that associates

683: with any channel its content (a sequence of messages). The set $Q\times

684: {\Mess^*}^\C$ of all configurations is denoted by

685: $\Conf=\{\sigma,\rho,\ldots\}$. For a subset $V$ of $\Conf$, we let

686: $\overline{V} \egdef \Conf \setminus V$.

687: 

688: Steps between configurations are as expected. Formally, $\sigma = (q,w)$

689: leads to $\sigma' = (q',w')$ by firing $\delta = p \step{\op} r$, denoted

690: $\sigma \step{\delta}_{\perf} \sigma'$, if and only if $q=p$, $q'=r$ and

691: $w'$ is obtained from $w$ by the effect of $\op$ (the ``$\perf$'' subscripts

692: emphasizes that the step is perfect: without losses). Precisely,

693: $w'(c)=w(c)$ for all channels $c$ that are not touched upon by $\op$, and

694: \[

695: 	w'(c) = \begin{cases}

696: 		  w(c) m & \textrm{ if } \op = c!m,\\

697: 		  m^{-1}w(c) & \textrm{ if } \op = c?m.

698: 		\end{cases}

699: \]

700: Thus, when $\op=c?m$, $w'$ is only defined if $w(c)$ starts with $m$ and

701: indeed this is the intended condition for firing $\delta$. Whenever $\sigma

702: \step{\delta} \rho$ for some $\rho$, we say that $\delta$ is \emph{enabled}

703: in $\sigma$, written $\delta \in \Delta(\sigma)$.

704: 

705: Below we restrict our attention to LCS's where from each $q\in Q$ there is

706: at least one rule $q\step{\op}p$ in $\Delta$ where $\op$ is not a receiving

707: action: this ensures that the LCS has no deadlock states and simplifies

708: many technical details without losing any generality.

709: 

710: 

711: \paragraph*{\bf Lossy systems.}

712: %-----------------------------

713: In \emph{lossy} channel systems, losing messages is formalized via the

714: subword ordering, extended from $\Mess^*$ to $\Conf$: $(q,w) \sqsubseteq

715: (q',w')$ if $q=q'$ and $w(c) \sqsubseteq w'(c)$ for all channels $c \in

716: \C$.

717: 

718: A (possibly lossy) step in the LCS is made of a perfect step followed by

719: arbitrary losses:\footnote{

720: %

721: \label{STEP-fn}

722:    Note that, with this definition, message losses only occur \emph{after}

723:    steps (thus, not in the initial configuration). The usual definition

724:    allows arbitrary losses before and after a step. There is no essential

725:    semantical difference between these two ways of grouping atomic events

726:    into single ``steps''. The usual definition is technically smoother when

727:    LCS's are viewed as nondeterministic systems, but becomes unnatural in

728:    situations where several adversarial processes compete, e.g., in

729:    probabilistic LCS's~\cite{BBS-acmtocl06} or other game-theoretical

730:    settings we explore in sections~\ref{sec-turn-based}

731:    and~\ref{sec-prob-lcs}.

732: %

733: } formally, we write $\sigma \step{\delta}\rho$ whenever there is a perfect

734: step $\sigma \step{\delta}_{\perf} \sigma'$ such that $\rho \sqsubseteq

735: \sigma'$. This gives rise to a labeled transition system $\LTS_\L \egdef

736: (\Conf,\Delta,\to)$, that can be given a WSTS structure by the following

737: relation: $\sigma\preceq \rho\;\equivdef\;

738: \sigma\sqsubseteq\rho\:\cap\:\Delta(\sigma)=\Delta(\rho)$. Both

739: $\sqsubseteq$ and $\preceq$ turns $\Conf$ into a WQO.

740: \begin{remark}

741: From now on we assume for the sake of simplicity that

742: $(\Conf,\sqsubseteq)$ is the WQO on which $L_\mu$ is defined. All results

743: could be strengthened using $(\Conf,\preceq)$.

744: %

745: \qed

746: \end{remark}

747: Following standard notations for transition systems $(\Conf,\Delta,\to)$

748: labeled over some $\Delta$, we write

749: $\Pre[\delta](\sigma)\egdef\{\rho\in\Conf~|~\rho\step{\delta}\sigma\}$ for

750: the set of predecessors via $\delta$ of $\sigma$ in $\L$. Then

751: $\Pre(\sigma) \egdef \bigcup_{\delta \in \Delta} \Pre[\delta](\sigma)$ has

752: all 1-step predecessors of $\sigma$, and $\Pre(V) = \bigcup_{\sigma \in V}

753: \Pre(\sigma)$ has all 1-step predecessors of states in $V$. The dual

754: $\wPre$ of $\Pre$ is defined by $\wPre(V)

755: =\overline{\Pre(\overline{V})}$. Thus $\sigma \in \wPre(V)$ iff

756: all 1-step successors of $\sigma$ are in $V$ (this includes the case where

757: $\sigma$ is a deadlock state).

758: 

759: Seen as unary operators on $2^\Conf$, both $\Pre$ and $\wPre$ are

760: monotonic and even continuous for all transition systems~\cite{sifakis82}.

761: For LCS's, the following lemma states that $\Pre$ is compatible with the

762: WQO on states, which will play a crucial role later when we want to show

763: that some $L_\mu$ term is guarded.

764: \begin{lemma}

765: \label{lem-pre-guarded}

766: Let $V\subseteq\Conf$ in the transition system $\LTS_\L$ associated with a

767: LCS $\L$. Then $\Pre(V) = \Pre(\Cu(V))$ and $\wPre(V) =

768: \wPre(\Kd(V))$.

769: \end{lemma}

770: \begin{proof}

771: $V\subseteq\Cu(V)$ implies $\Pre(V) \subseteq \Pre(\Cu(V))$. Now

772: $\sigma\in\Pre(\Cu(V))$ implies that $\sigma\step{}\rho\sqsupseteq\rho'$

773: for some $\rho'\in V$. But then $\sigma\step{}\rho'$ by definition of lossy

774: steps and $\sigma\in\Pre(V)$. The second equality is dual.

775: %

776: \qed

777: \end{proof}

778: 

779: 

780: 

781: \paragraph*{\bf An effective region algebra for LCS's.}

782: %------------------------------------------------------

783: We are now ready to apply the framework of

784: section~\ref{sec-guarded-mucalculus} to regular model checking of lossy

785: channel systems. Assume $\L= (Q,\C,\Mess,\Delta)$ is a given LCS. A region

786: $R\in\R$ is any ``regular'' subset of $\Conf$. More formally, it is any set

787: $R\subseteq\Conf$ that can be written under the form

788: \[

789: 	R = \sum_{i \in I} (q_i,R_{i}^1,\ldots,R_{i}^{|\C|})

790: \]

791: where $I$ is a \emph{finite} index set, the $q_i$'s are locations from $Q$,

792: and each $R_{i}^j$ is a regular language on alphabet $\Mess$. The notation

793: has obvious interpretation, with summation denoting set union (the empty

794: sum is denoted $\emptyset$). We are not more precise on how such regions

795: could be effectively represented (see~\cite{abdulla2001b}), but they could be handled as, e.g.,

796: regular expressions or FSAs over the extended alphabet $\Mess\cup

797: Q\cup\{\mathtt{'('},\mathtt{')'},\mathtt{','}\}$.

798: 

799: The set $O$ of operators includes union, intersection, $\Cu$, $\Cd$, $\Ku$,

800: $\Kd$: these are monotonic, regularity-preserving, and effective operators

801: as explained in our example at the end of

802: section~\ref{sec-guarded-mucalculus}. Operators specific to regular

803: model-checking are $\Pre$ and $\wPre$. That they are

804: regularity-preserving and effective is better seen by first looking at the

805: special case of perfect steps:

806: \begin{align*}

807: \Pre_{\perf}[p \step{c_i?m} r](q,R_p^1, \cdots, R_p^{|\C|}) &=

808: \begin{cases}

809:   (p,R_p^1, \ldots, R_p^{i-1}, m R_p^i, R_p^{i+1}, \ldots, R_p^{|\C|}) & \textrm{ if } q=r,\\

810:   \emptyset & \textrm{ otherwise.}

811: \end{cases}

812: \\

813: \Pre_{\perf}[q \step{c_i!m} q'](q,R_p^1, \cdots, R_p^{|\C|}) &=

814: \begin{cases}

815:   (p,R_p^1, \ldots, R_p^{i-1}, R_p^i m^{-1}, R_p^{i+1}, \ldots, R_p^{|\C|}) & \textrm{ if } q=r,\\

816:   \emptyset & \textrm{ otherwise.}

817: \end{cases}

818: \\

819: \Pre_{\perf}\Bigl(\sum_{i\in I} (q_i, R_i^1,\ldots,R_i^{|\C|})\Bigr)

820: 	& = \sum_{i\in I}\sum_{\delta\in\Delta} \Pre_{\perf}[\delta] (q_i,R_i^1,\ldots,R_i^{|\C|}).

821: \end{align*}

822: where the notation ``$m R$'' (for concatenation) and ``$R m^{-1}$'' (for

823: right-residuals) are as in section~\ref{sec-guarded-mucalculus}. For lossy

824: steps we use

825: \[

826: 		       \Pre(R) = \Pre_\perf(\Cu(R)).

827: \]

828: Clearly, both $\Pre_\perf$ and $\Pre$ are effective operators on regions.

829: 

830: 

831: 

832: \subsection{Regular model-checking for lossy channel systems}

833: %============================================================

834: 

835: Surprising decidability results for lossy channel systems is what launched

836: the study of this model~\cite{finkel94,abdulla96b,cece95}. We reformulate

837: several of these results as a direct consequence of

838: Theorem~\ref{th-guarded-effective}, before moving to new problems and new

839: decidability results in the next sections. Note that our technique is

840: applied here to a slightly different operational semantics (cf.\

841: footnote~\ref{STEP-fn}) but it would clearly apply as directly to the

842: simpler semantics.

843: 

844: \paragraph*{\bf Reachability analysis.}

845: %------------------------------------

846: Thanks to Lemma~\ref{lem-pre-guarded}, the co-reachability set can be

847: expressed as a guarded $L_\mu$ term:

848: \begin{equation}

849: \label{eq-pre-star}

850:       \Pre^*(V) = \mu X. V \cup \Pre(X) = \mu X. V \cup \Pre(\Cu(X)).

851: \end{equation}

852: \begin{corollary}

853: For regular $V\subseteq\Conf$, $\Pre^*(V)$ is regular and effectively computable.

854: \end{corollary}

855: 

856: \paragraph*{\bf Safety properties.}

857: %---------------------------------

858: More generally, safety properties can be handled. In CTL, they can be

859: written $\forall (V_1 \Release V_2)$. Recall that $\Release$, the Release

860: modality, is dual to Until: a state $\sigma$ satisfies $\forall (V_1 \Release

861: V_2)$ if and only if along all paths issuing from $\sigma$, $V_2$ always holds

862: until maybe $V_1$ is visited. Using Lemma~\ref{lem-pre-guarded},

863: $\rep{\forall (V_1 \Release V_2)}$, the set of states where the safety property

864: holds, can be defined as a guarded $L_\mu$ term:

865: \begin{equation}%you can check it at \cite[p.~10]{BradfieldStirling01}

866: \label{eq-forall-release}

867: \rep{\forall (V_1 \Release V_2)}

868: = \nu X. \bigl(V_2 \cap (\wPre(X) \cup V_1)\bigr)

869: = \nu X. \bigl(V_2 \cap (\wPre(\Kd(X)) \cup V_1)\bigr).

870: \end{equation}

871: \begin{corollary}

872: \label{coro-AR}

873: For regular $V_1,V_2\subseteq\Conf$, $\rep{\forall (V_1 \Release V_2)}$ is regular

874: and effectively computable.

875: \end{corollary}

876: Another formulation is based on the duality

877: between the ``$\forall\Release$'' and the ``$\exists\Until$'' modalities.

878: \begin{theorem}\cite[sect.~5]{KucSch-TCS}

879: \label{KS-theorem}

880: If $f$ is a temporal formula in the

881: $\Lang(\exists\Until,\exists\Next,\wedge,\neg)$ fragment of CTL (using

882: regions for atomic propositions), then $\rep{f}$ is regular and effectively

883: computable.

884: \end{theorem}

885: \begin{proof}

886: By induction on the structure of $f$, using

887: $\rep{\exists\Next f}\egdef \Pre(\rep{f})$, and the fact that

888: regions are (effectively) closed under complementation.

889: %

890: \qed

891: \end{proof}

892: 

893: 

894: \paragraph*{\bf Beyond safety.}

895: %-----------------------------

896: Inevitability properties, and recurrent reachability can be stated in $L_\mu$.

897: With temporal logic notation, this yields

898: \begin{align*}

899: %\label{eq-forall-eventually}%you can check it at \cite[p.~99]{Stirling01}

900: \rep{\forall \Diamond V} &= \mu X. \bigl(V \cup (\Pre(\Conf) \cap \wPre(X))\bigr),

901: \\

902: %\label{eq-f-infini}%you can check it at \cite[p.~22]{BradfieldStirling01}

903: \rep{\exists \Box\Diamond V} &= \nu X. \bigl(\mu Y. ((V \cup \Pre(Y)) \cap \Pre(X))\bigr).

904: \end{align*}

905: These two terms are not guarded and Lemma~\ref{lem-pre-guarded} is of no

906: help here. However this is not surprising: firstly, whether

907: $\sigma\sat\exists\Box\Diamond V$ is undecidable~\cite{abdulla96c}; secondly,

908: and while $\sigma\sat\rep{\forall \Diamond V}$ is decidable, the set

909: $\rep{\forall \Diamond V}$ cannot be computed

910: effectively~\cite{mayr-unreliable}.

911: 

912: 

913: 

914: \subsection{Generalized lossy channel systems}

915: %---------------------------------------------

916: \label{ssec-extended-lcs}

917: 

918: Transition rules in LCS's do not carry guards, aka preconditions, beyond

919: the implicit condition that a reading action $c?m$ is only enabled when

920: $w(c)$ starts with $m$. This barebone definition is for simplification

921: purpose, but actual protocols sometimes use guards that probe the contents

922: of the channel before taking this or that transition. The simplest such

923: guards are emptiness tests, like ``$p\step{c=\epsilon?}q$'' that only

924: allows a transition from $p$ to $q$ if $w(c)$ is empty.

925: 

926: We now introduce \emph{LCS's with regular guards} (GLCS's), an extension of

927: the barebone model where any regular set of channel contents can be used to

928: guard a transition rule. This generalizes emptiness tests, occurrence tests

929: (as in~\cite{OuaknineWorrell06}), etc., and allows expressing priority

930: between rules since whether given rules are enabled is a regular condition.

931: 

932: Formally, we assume rules in $\Delta$ now have the form $p

933: \step{G:\op} q$ with $p,q,\op$ as before, and where $G$, the guard,

934: can be any regular region. The operational semantics is a expected:

935: when $\delta=p\step{G:\op}q$, there is a perfect step

936: $\sigma\step{\delta}_\perf\theta$ iff $\sigma \in G$ and $\theta$ is

937: obtained from $\sigma$ by the rule $p \step{G:\op} q$ (without any

938: guard). Then, general steps $\sigma\step{\delta}\rho$ are obtained

939: from perfect steps $\sigma\step{\delta}_\perf\sigma'$ by message

940: losses $\rho\sqsubseteq \sigma'$.

941: 

942: 

943: \paragraph*{\bf Verification of GLCS's.}

944: %---------------------------------------

945: For GLCS's, $\Pre$ and $\Post$ are effective monotonic

946: regularity-preserving operators as in the  LCS case since

947: \begin{align*}

948: 	   \Pre[p\step{G:\op}q](R)&=G\:\cap\:\Pre[p\step{\op}q](R),	\\

949: 	  \Post[p\step{G:\op}q](R)&=\Post[p\step{\op}q](G\cap R).

950: \end{align*}

951: Observe that Lemma~\ref{lem-pre-guarded} holds for GLCS's as well, so that

952: Equations \eqref{eq-pre-star} and \eqref{eq-forall-release} entail a

953: generalized version of Theorem~\ref{KS-theorem}:

954: \begin{theorem}

955: For all GLCS's $\L$ and formulae $f$ in the

956: $\Lang(\exists\Until,\exists\Next,\wedge,\neg)$ fragment, $\rep{f}$ is

957: regular and effectively computable.

958: \end{theorem}

959: 

960: 

961: 

962: 

963: %%% Local Variables:

964: %%% Local IspellDict: "english"

965: %%% mode: latex

966: %%% TeX-master: "main-regular"

967: %%% End:

968: 

969: % LocalWords:  verif LCS.tex phs Exp LCS tex LCS's subword WSTS WQO iff NFA CTL

970: % LocalWords:  perf tt barebone GLCS's eq forall

971: %%% TEXEXPAND: END FILE ./sec-verif-LCS.tex

972: %%% TEXEXPAND: INCLUDED FILE MARKER ./sec-turn-based.tex

973: %%% $Id: sec-turn-based.tex,v 1.21 2006/05/13 10:00:56 phs Exp $

974: 

975: 

976: \section{Solving games on lossy channel systems}

977: %===============================================

978: \label{sec-turn-based}

979: 

980: 

981: In this section, we consider turn-based games on GLCS's where two players,

982: $A$ and $B$, alternate their moves. Games play a growing role in

983: verification where they address situations in which different agents have

984: different, competing goals. We assume a basic understanding of the

985: associated concepts: arena, play, strategy, etc. (otherwise

986: see~\cite{Graedel-Thomas-Wilke-LNCS}).

987: 

988: Games on well-structured systems have already been investigated

989: in~\cite{abdulla2003b,raskin03,raskin05}. The positive results in these

990: three papers rely on ad-hoc finite convergence lemmas that are special

991: cases of our Theorem~\ref{th-guarded-effective}.

992: 

993: 

994: 

995: 

996: \subsection{Symmetric LCS-games with controllable message losses}

997: %----------------------------------------------------------------

998: \label{ssec-symmetric-games}

999: 

1000: We start with the simplest kind of games on a GLCS: $A$ and $B$ play in

1001: turn, choosing the next configuration, i.e., picking what rule

1002: $\delta\in\Delta$ is fired, and what messages are lost.

1003: 

1004: Formally, a \emph{symmetric LCS-game} is a GLCS $\L=

1005: (Q_A,Q_B,\C,\Mess,\Delta)$ where the set of locations $Q=Q_A \cup Q_B$ is

1006: partitioned into two sets, one for each player, and where the rules ensure

1007: strict alternation: for all $p \step{G:\op} q \in \Delta$, $p\in Q_A$ iff

1008: $q\in Q_B$. Below, we shortly write $\Conf_A$ for

1009: $Q_A\times{\Mess^*}^{|\C|}$, the regular region where it is $A$'s turn to

1010: play. $\Conf_B$ is defined similarly. Strict alternation means that the

1011: arena, $\LTS_\L$, is a bipartite graph partitioned in $\Conf_A$ and

1012: $\Conf_B$.

1013: 

1014: 

1015: \paragraph*{\bf \em Reachability games.}

1016: %--------------------------------------

1017: Reachability and invariant are among the simplest objectives for

1018: games. In a reachability game, $A$ tries to reach a state in some set

1019: $V$, no matter how $B$ behaves. This goal is denoted $\Diamond V$. It

1020: is known that such games are determined and that memoryless strategies

1021: are sufficient~\cite{Graedel-Thomas-Wilke-LNCS}. The set of winning

1022: configurations for $A$ is denoted with $\ex{A} \Diamond V$, and can be

1023: defined in $L_\mu$:

1024: \begin{equation}

1025: \label{eq-reachgame}

1026: \ex{A} \Diamond V = 

1027: 	\mu X.\Bigl[ V \cup \bigl[\Conf_A \cap \Pre(X)\bigr] 

1028: 	               \cup \bigl[\Conf_B \cap \wPre(X)\bigr]\Bigr].

1029: \end{equation}

1030: The first occurrence of $X$ can be made upward-guarded by replacing

1031: $\Pre(X)$ with $\Pre(\Cu(X))$ (Lemma~\ref{lem-pre-guarded}). For the second

1032: occurrence, we can unfold the term, relying on the fixpoint equation

1033: $\rep{\mu X.\phi(X)}=\rep{\mu X.\phi(\phi(X))}$. This will replace

1034: $\Conf_B\cap\wPre(X)$ in \eqref{eq-reachgame} with

1035: \begin{equation}

1036: \tag{+}

1037: \label{eq+}

1038: \Conf_B\cap \wPre\Bigl(V \cup \bigl[\Conf_A \cap

1039:   \Pre(X)\bigr] \cup \bigl[\Conf_B \cap \wPre(X)\bigr]\Bigr).

1040: \end{equation}

1041: Now, the strict alternation between $\Conf_A$ and $\Conf_B$ lets us simplify

1042: \eqref{eq+} into

1043: \begin{equation}

1044: %\tag{++}

1045: \Conf_B \cap \wPre\Bigl(V \cup	\Pre(X) \Bigr).

1046: \end{equation}

1047: Hence \eqref{eq-reachgame} can be rewritten into

1048: \begin{gather}

1049: \label{eq-reachgame-var}

1050: \tag{\ref{eq-reachgame}'}

1051: \ex{A} \Diamond V = \mu X.\Bigl[ V \cup \bigl[\Conf_A \cap

1052: 			\Pre(\Cu(X))\bigr] \cup \bigl[\Conf_B \cap

1053: 			\wPre(V\cup \Pre(\Cu(X)))\bigr]\Bigr].

1054: \end{gather}

1055: %% \begin{remark}

1056: %% Rewriting \eqref{eq-reachgame} into \eqref{eq-reachgame-var} relies heavily

1057: %% on the strict alternation between $A$- and $B$-states. However, winning

1058: %% positions in reachability games on GLCS's without strong alternation can

1059: %% also be expressed by a guarded $L_\mu$ term.

1060: %% %

1061: %% \qed

1062: %% \end{remark}

1063: 

1064: \paragraph*{\bf \em Invariant games.}

1065: %------------------------------------

1066: In invariant games, $A$'s goal is to never leave  some set

1067: $V\subseteq\Conf$, no matter how $B$ behaves. Invariant games are

1068: dual to reachability games, and the set of winning configurations

1069: $\ex{A}\Box V$ is exactly $\overline{\ex{B}\Diamond \overline{V}}$.

1070: 

1071: 

1072: \paragraph*{\bf \em Repeated reachability games.}

1073: %------------------------------------------------

1074: Here $A$'s goal is to visit $V$ infinitely many times, no matter how $B$

1075: behaves. The set of winning configurations is given by the following

1076: $L_\mu$ term:

1077: \begin{equation}

1078: \ex{A} \Box \Diamond V = \nu Y. \ex{A}\Diamond \Bigl[ V \cap

1079: (\varphi_A(Y) \cup \varphi_B(Y))\Bigr],

1080: \end{equation}

1081: where

1082: \begin{align*}

1083: 	\varphi_A(Y) & \egdef \Conf_A \cap \Pre\bigl( \Cu(\wPre(\Kd(Y)))\bigr),

1084: \\

1085: 	\varphi_B(Y) & \egdef \Conf_B \cap \wPre(\Kd(Y)).

1086: \end{align*}

1087: and where we reuse \eqref{eq-reachgame-var} for $\ex{A} \Diamond [\ldots]$.

1088: 

1089: 

1090: 

1091: \paragraph*{\bf \em Persistence games.}

1092: %--------------------------------------

1093: In a persistence game, $A$ aims at remaining inside $V$ from some moment

1094: on, no matter how $B$ behaves. Dually, this can be seen as a repeated

1095: reachability game for $B$. Note that $\ex{A} \Diamond \Box V \neq \ex{A}

1096: \Diamond (\ex{A} \Box V)$.

1097: 

1098: \begin{theorem}[Decidability of symmetric LCS-games]

1099: For symmetric LCS-games $\L$ and regular regions $V$, the four sets

1100: $\ex{A}\Diamond V$, $\ex{A}\Box V$, $\ex{A}\Diamond\Box V$, and

1101: $\ex{A}\Box\Diamond V$, are (effective) regions. Hence reachability,

1102: invariant, repeated reachability, and persistence symmetric games are

1103: decidable on GLCS's.

1104: \end{theorem}

1105: \begin{proof}[Sketch] The winning sets can be defined by guarded $L_\mu$

1106:   terms.

1107: \end{proof}

1108: \begin{remark}

1109: There is no contradiction between the undecidability of

1110: $\exists\Box\Diamond V$ and the decidability of $\ex{A}\Box\Diamond V$. In

1111: the latter case, $B$ does not cooperate with $A$, making the goal harder to

1112: reach for $A$ (and the property easier to decide for us).

1113: %

1114: \qed

1115: \end{remark}

1116: 

1117: %%

1118: %% \paragraph*{\bf \em Parity games.}

1119: %%

1120: %%   .....

1121: %%

1122: %% \marginpar{\tt ???? I did not think about this}

1123: 

1124: 

1125: \subsection{Asymmetric LCS-games with 1-sided controlled loss of messages}

1126: %-------------------------------------------------------------------------

1127: \label{ssec-1sided-games}

1128: 

1129: Here we adopt the setting considered in~\cite{abdulla2003b}. It varies from

1130: the symmetric setting of section~\ref{ssec-symmetric-games} in that only

1131: player $B$ can lose messages (and can control what is lost), while player

1132: $A$ can only make perfect steps. Note that this generalizes games where $A$

1133: plays moves in the channel system, and $B$ is an adversarial environment

1134: responsible for message losses. We use the same syntax as for symmetric

1135: LCS-games.

1136: 

1137: 

1138: 

1139: \paragraph*{\bf \em Reachability and invariant games.}

1140: %----------------------------------------------------

1141: Let us first consider games where one player tries to reach a regular

1142: region $V$ (goal $\Diamond V$), no matter how the other player behaves.

1143: 

1144: The configurations where $B$ can win a reachability game are given by:

1145: \begin{align*}

1146: \begin{split}

1147:   \ex{B} \Diamond V

1148:   & = \mu X. V \cup \Bigl(\Conf_B \cap \Pre(X)\Bigr) \cup \Bigl(\Conf_A \cap \wPre_\perf(X) \Bigr)\\

1149:   & = \mu X. V \cup \Bigl( \Conf_B \cap \Pre(\Cu (X))\Bigr) \cup

1150:   \Bigl(\Conf_A \cap \wPre_\perf(V \cup \Pre(\Cu(X))) \Bigr)

1151: \end{split}

1152: \end{align*}

1153: where guardedness is obtained via Lemma~\ref{lem-pre-guarded} and

1154: unfolding.

1155: 

1156: When we consider a reachability game for $A$, the situation is not so clear:

1157: \begin{equation*}

1158:   \ex{A} \Diamond V = \mu X. V \cup \Bigl(\Conf_A \cap

1159:   \Pre_\perf(X)\Bigr) \cup \Bigl(\Conf_B \cap \wPre(X) \Bigr).

1160: \end{equation*}

1161: Neither Lemma~\ref{lem-pre-guarded} nor unfolding techniques can turn

1162: this into a guarded term. This should be expected since the set

1163: $\ex{A} \Diamond V$ cannot be computed

1164: effectively~\cite{abdulla2003b}.

1165: 

1166: 

1167: \begin{theorem}[Decidability of asymmetric LCS-games~\cite{abdulla2003b}]

1168: For asymmetric LCS-games $\L$ and regular regions $V$,	the sets

1169: $\ex{B}\Diamond V$  and $\ex{A}\Box V$ are (effective) regions. Hence

1170: reachability games for $B$, and invariant games for $A$ are decidable on

1171: GLCS's.

1172: \end{theorem}

1173: \begin{proof}[Sketch] Invariant games are dual to reachability games, and

1174:   the winning set $\ex{B}\Diamond V$ is defined by a guarded $L_\mu$

1175:   term.

1176: \end{proof}

1177: 

1178: 

1179: %% \begin{align}

1180: %% \begin{split}

1181: %%   \ex{A} \Box V

1182: %%	   & \egdef \nu X. V \cap \Bigl(\Conf_B \cap \Pre\bigl(

1183: %%	      V \cup \wPre_\perf(X) \bigr)  \Bigr)

1184: %% \\

1185: %%	   & = \mu X. V \cup \Bigl(\Conf_B \cap \Pre\bigl(\Cu(

1186: %%	      V \cup \wPre_\perf(X)) \bigr)  \Bigr)

1187: %% \end{split}

1188: %% \end{align}

1189: %% where guardedness is obtained via Lemma~\ref{lem-pre-guarded}.

1190: 

1191: %% When we consider a reachability game for $A$, the situation is not so clear:

1192: %% \begin{align}

1193: %%   \ex{A} \Diamond V

1194: %%	   & \egdef \mu X. V \cup \Bigl(\Conf_A \cap \Pre_\perf\bigl(

1195: %%	      V \cup \wPre(X) \bigr)  \Bigr)

1196: %% \end{align}

1197: 

1198: %% WHAT ABOUT THIS ``PROBABILISTIC'' PART??

1199: %%

1200: %% For the probabilistic variant

1201: %% ''$B$ tries to stay forever in $V$, no mater how $A$ behaves

1202: %% and no matter which loss of messages will appear''

1203: %% the set of configurations $(q,w)$

1204: %% where $q\in Q_B$ and $B$ has a winning strategy

1205: %% is expressible in $L_\mu$:

1206: %% $$

1207: %% \nu X. Q_B \cap V \cap \Pre_\perf\bigl(

1208: %% \Kd( V \cap \wPre_\perf(X) ) \bigr)

1209: %% $$

1210: 

1211: 

1212: %% Let us now look for the set of

1213: %% configurations where

1214: %% $A$ has a winning strategy for $\Box V$.

1215: %% This set is given by for the $L_\mu$ term:

1216: %% $$\ex{A} \Box V \stackrel{\text{def}}{=} \nu X. Q_A \cap V \cap

1217: %% \Pre_\perf\bigl( V \cap

1218: %% \wPre_\perf(\Kd(X) ) \bigr)

1219: %% $$

1220: %% \marginpar{\tt not considered by Parosh et al, I think}

1221: 

1222: %% \ \\

1223: 

1224: 

1225: 

1226: %%% Local Variables:

1227: %%% mode: latex

1228: %%% TeX-master: "main-regular"

1229: %%% End:

1230: 

1231: % LocalWords:  GLCS's LCS GLCS iff fixpoint eq reachgame

1232: %%% TEXEXPAND: END FILE ./sec-turn-based.tex

1233: %%% TEXEXPAND: INCLUDED FILE MARKER ./sec-prob-lcs.tex

1234: %%% $Id: sec-prob-lcs.tex,v 1.12 2006/05/13 10:04:31 phs Exp $

1235: 

1236: 

1237: \section{Channel systems with probabilistic losses}

1238: %==================================================

1239: \label{sec-prob-lcs}

1240: 

1241: 

1242: LCS's where messages losses follow probabilistic rules have been

1243: investigated as a less pessimistic model of protocols with unreliable

1244: channels (see~\cite{Sch-voss,ABRS-icomp,BBS-acmtocl06} and the references

1245: therein).

1246: 

1247: In~\cite{BBS-acmtocl06}, we present decidability results for LCS's seen as

1248: combining \emph{nondeterministic} choice of transition rules with

1249: \emph{probabilistic} message losses. The semantics is in term of Markovian

1250: decision processes, or $1\frac{1}{2}$-player games, whose solutions can be

1251: defined in $L_\mu$. Indeed, we found the inspiration for $L_\mu$ and our

1252: Theorem~\ref{th-guarded-effective} while extending our results in the MDP

1253: approach to richer sets of regions.

1254: 

1255: In this section, rather than rephrasing our results on

1256: $1\frac{1}{2}$-player games on LCS's, we show how to deal with

1257: $2\frac{1}{2}$-player games~\cite{chatterje05} on LCS's, i.e., games

1258: opposing players $A$ and $B$ (as in section~\ref{sec-turn-based}) but where

1259: message losses are probabilistic.

1260: \\

1261: 

1262: 

1263: Formally, a \emph{symmetric probabilistic LCS-game}

1264: $\L=(Q_A,Q_B,\C,\Mess,\Delta)$ is exactly like a symmetric LCS-game but

1265: with an altered semantics: in state $\sigma\in\Conf_A$, player $A$ selects

1266: a fireable rule $\delta\in\Delta$ ($B$ picks the rule if

1267: $\sigma\in\Conf_B$) and the system moves to a successor state $\rho$ where

1268: $\sigma\step{\delta}_\perf\sigma'\sqsupseteq\rho$ and $\rho$ is chosen

1269: probabilistically in $\Cd(\{\sigma'\})$. The definition of the probability

1270: distribution $\bfP(\sigma,\delta,\rho)$ can be found

1271: in~\cite{Sch-voss,BBS-acmtocl06} where it is called \emph{the local-fault

1272: model}. It satisfies $\bfP(\sigma,\delta,\rho)>0$ iff

1273: $\rho\sqsubseteq\sigma'$ (assuming $\sigma\step{\delta}_\perf\sigma'$).

1274: Additionally it guarantees a \emph{finite-attractor property}: the set of

1275: states where all channels are empty will be visited infinitely many times

1276: almost surely~\cite{ABRS-icomp,BBS-ipl}.

1277: 

1278: 

1279: 

1280: \paragraph*{\bf \em Reachability games.}

1281: %---------------------------------------

1282: Assume $A$ tries to reach region $V$ (goal $\Diamond V$) \emph{with

1283: probability 1} no matter how $B$ behaves. The set $\ex{A} [\Diamond

1284: V]_{=1}$ of states in which $A$ has an almost-sure winning strategy is

1285: given by

1286: \begin{equation}

1287: \label{eq-reach-P1}

1288: \ex{A} [\Diamond V]_{=1} =

1289:  \nu Y. \mu X.	 \left(

1290: 	\begin{array}{rl}

1291: 	 V \cup & \Bigl[\Conf_A \cap \Pre_\perf (\Cu(X) \cap \Kd(Y))\Bigr]

1292:     \\[.5em]

1293: 	   \cup & \Bigl[\Conf_B \cap \wPre_\perf (\Cu(X) \cap \Kd(Y))\Bigr]

1294: 	\end{array}

1295: 	\right).

1296: \end{equation}

1297: \begin{remark}

1298: Justifying \eqref{eq-reach-P1} is outside the scope of this paper, but we

1299: can try to give an intuition of why it works: the inner fixpoint ``$\mu X.

1300: V\cup \cdots$'' define the largest set from which $A$ has a strategy to

1301: reach $V$ no matter what $B$ does \emph{if the message losses are

1302: favorable}. However, whatever messages are lost, $A$'s strategy also

1303: guarantees that the system will remain in $Y$, from which it will be

1304: possible to retry the strategy for $\Diamond V$ as many times as necessary.

1305: This will eventually succeed almost surely thanks to the finite-attractor

1306: property.

1307: %

1308: \qed

1309: \end{remark}

1310: 

1311: 

1312: 

1313: %%%% \iffalse

1314: %%%% \marginpar{\tt here is something wrong!}

1315: %%%% {\tt Sorry. I did here several copy \& paste's

1316: %%%% and finally I lost the overview. I think what is written

1317: %%%% here is simply wrong.}

1318: %%%%

1319: %%%%

1320: %%%% To show the correctness of the above formula we shall use the

1321: %%%% following observation concerning the inner least fixed point formula.

1322: %%%% Let $N \subseteq \Conf$ and let

1323: %%%% $$ M(N) =

1324: %%%% \rep{\mu X.  V  \cup

1325: %%%%   (Q_A \cap \Pre_{\text{perfect}}

1326: %%%%	  (\Cu(X) \cap \Kd(N))\bigr)

1327: %%%%	  \cup	\bigl(Q_B \cap \wPre_{\text{perfect}}

1328: %%%%	     (\Cu(X) \cap \Kd(N))\bigr)}

1329: %%%% $$

1330: %%%%

1331: %%%% \begin{lemma}

1332: %%%%   $M(N)$ is the set of winning configuration for $A$ and the goal $[V

1333: %%%%   \cup (N \Until (V \cap N)]_{=1}$.

1334: %%%% \end{lemma}

1335: %%%%

1336: %%%%

1337: %%%% \begin{proof}

1338: %%%%   In the sequel, we briefly write $M$ rather than $M(N)$ and $M_A$ for

1339: %%%%   $\{\tuple{q,w}\in M : q \in Q_A\}$.

1340: %%%% \begin{itemize}

1341: %%%% \item We first show that there exists a memoryless $A$-strategy

1342: %%%%   $\alpha$ such that for all $B$-strategies $\beta$ and all

1343: %%%%   configurations $s \in M \setminus V$ we have

1344: %%%% \begin{center}

1345: %%%% $\Pr_{(\alpha,\beta)}(s \models N \Until (V \cap N))=1$.

1346: %%%% \end{center}

1347: %%%% For each configuration $s=\tuple{q,w} \in N_A\setminus V$ there exists

1348: %%%% a transition rule $\delta_s \in \Delta_A(s)$ such that

1349: %%%% $$\Post[\delta_s](s) \cap (\Cu(M) \cap \Kd(N))

1350: %%%%   \not= \emptyset.

1351: %%%%   $$

1352: %%%%   Consider a memoryless $A$-strategy $\alpha$ given by $\alpha(s) =

1353: %%%%   \delta_s$ for $s \in N_A \setminus V$.  For all other

1354: %%%%   $A$-configurations, the definition of $\alpha(s)$ is arbitrary.	We

1355: %%%%   now show that for each $B$-strategy $\beta$, we have

1356: %%%% \begin{center}

1357: %%%%   $\Pr_{\alpha,\beta}(s_0 \models N \Until (V \cap N)) =1$ for all

1358: %%%%   $s_0 \in M$.

1359: %%%% \end{center}

1360: %%%% Let $\M_{\alpha,\beta}$ be the Markov chain induced by $\alpha$ and

1361: %%%% $\beta$ and let $s_0$ be a fixed configuration in $M$ that we treat as

1362: %%%% starting configuration.  Let $U$ be the set of all configurations that

1363: %%%% are reachable from $s_0$ in $\M_{\alpha,\beta}$ along a finite path

1364: %%%% $s_0\, s_1 \ldots s_n$ with $s_i \notin V$ for $0 \leq i \leq n$.	We

1365: %%%% then have $U \subseteq N$ and $V \cap N$ is reachable from all

1366: %%%% configurations $u \in U$ in $\M_{\alpha,\beta}$.  The finite attractor

1367: %%%% property then yields the claim.

1368: %%%% \item Let $\alpha$ be a memoryless winning strategy for $A$ and the

1369: %%%%   goal $[V \cup (N \Until (V \cap N)]_{=1}$ and starting state $s_0$.

1370: %%%%   Consider the set $U$ of all configurations $s$ such that there

1371: %%%%   exists a finite path

1372: %%%% $$s_0 \step{\delta_1} s_1 \step{\delta_2}\ldots \step{\delta_n} s_n

1373: %%%% $$

1374: %%%% in $\L$ with $s_n=s$ and $\delta_i = \alpha(s_{i-1})$ if $s_{i-1}$

1375: %%%% is a $Q_A$-configuration for $0 \leq i \leq n$.  Thus, $s_0 \, s_1

1376: %%%% \ldots s_n$ is a $(\alpha,\beta)$-path for some $B$-strategy $\beta$.

1377: %%%% Hence, $V$ is reachable from $s$ under the given $A$-strategy

1378: %%%% $\alpha$.

1379: %%%%

1380: %%%% ....

1381: %%%%

1382: %%%%

1383: %%%% \end{itemize}

1384: %%%% \end{proof}

1385: %%%%

1386: %%%% \begin{lemma}

1387: %%%%   If $s$ is a winning configuration for $A$ and the goal $[\Diamond

1388: %%%%   V]_{=1}$ then $s \in \rep{\ex{A} [\Diamond V]_{=1}}$.

1389: %%%% \end{lemma}

1390: %%%%

1391: %%%% \begin{proof}

1392: %%%% .....

1393: %%%% \end{proof}

1394: %%%%

1395: %%%% \begin{lemma}

1396: %%%%   If $s \in \rep{\ex{A} [\Diamond V]_{=1}}$ then $s$ is a winning

1397: %%%%   configuration for $A$ and the goal $[\Diamond V]_{=1}$.

1398: %%%% \end{lemma}

1399: %%%%

1400: %%%% \begin{proof}

1401: %%%%   Let $N =\rep{\ex{A} [\Diamond V]_{=1}}$ and

1402: %%%%   $$M = \rep{\mu X.  V \cup (Q_A \cap \Pre_{\text{perfect}}

1403: %%%%	 (\Cu(X) \cap \Kd(N))\bigr) \cup \bigl(Q_B

1404: %%%%	 \cap \wPre_{\text{perfect}} (\Cu(X) \cap

1405: %%%%	 \Kd(N))\bigr)}

1406: %%%% $$

1407: %%%%

1408: %%%% Let $N_A$ be the set of all configurations $s = \tuple{q,w} \in N$

1409: %%%% where $q \in Q_A$.	 $N_B$, $M_A$ and $M_B$ have the analogous meaning.

1410: %%%%

1411: %%%% \end{proof}

1412: %%%%

1413: %%%%

1414: %%%% \iffalse

1415: %%%% \marginpar{\tt Prom ???}

1416: %%%% for single player (?)

1417: %%%% $$\nu Y. \mu X. (V \cup \underbrace{\Pre(\Cu X \cap

1418: %%%%   \Kd(Y)))}_{ \widehat{\Pre}_Y(\Cu X)}

1419: %%%% $$

1420: %%%% \fi

1421: %%%% \fi

1422: %%%%

1423: 

1424: 

1425: \paragraph*{\bf \em Invariant games.}

1426: %------------------------------------

1427: Assume now $A$ tries to stay in $V$ almost surely (goal $[\Box V]_{=1}$), no

1428: matter how $B$ behaves. Then $A$ must ensure $\Box V$ surely and

1429: we are considering a 2-player game where message losses are adversarial

1430: and could as well be controlled by $B$. This leads to

1431: \begin{equation}

1432: \label{eq-Box=1}

1433: \begin{split}

1434: \ex{A}[\Box V]_{=1}

1435: & = \nu X. V \cap

1436: \Bigl(\bigl[\Conf_A \cap

1437: \Pre_\perf(\Kd(X))\bigr] \cup \bigl[\Conf_B \cap \wPre(X)\bigr]\Bigr)

1438: \\

1439: & = \nu X. V \cap

1440: \Bigl(\bigl[\Conf_A \cap

1441: \Pre_\perf(\Kd(X))\bigr] \cup \bigl[\Conf_B \cap \wPre(\Kd(X))\bigr]\Bigr).

1442: \end{split}

1443: \end{equation}

1444: In \eqref{eq-Box=1}, the subterm $\Pre_\perf(\Kd(X))$

1445: accounts for states in which $A$ can choose  a perfect move that will end

1446: in $\Kd(X)$, i.e., that can be followed by any adversarial message losses

1447: and still remain in $X$. The subterm  $\wPre(X)$ accounts for states

1448: in which $B$ cannot avoid going to $X$, even with message losses under his

1449: control.  $\wPre(X)$ can be rewritten into

1450: $\wPre(\Kd(X))$ thanks to Lemma~\ref{lem-pre-guarded}, so that we end up

1451: with a guarded term.

1452: 

1453: 

1454: 

1455: \paragraph*{\bf \em Goals to be satisfied with positive probability.}

1456: %====================================================================

1457: In $2\frac{1}{2}$-player games, it may happen that a given goal can only be

1458: attained with some non-zero probability~\cite{chatterje05}. Observe that,

1459: since the games we consider are determined~\cite{martin98}, the goals

1460: $[\Diamond V]_{>0}$ or $[\Box V]_{>0}$ are the opposite of goals asking for

1461: probability 1:

1462: \begin{xalignat*}{2}

1463: \ex{A}[\Diamond V]_{>0} &= \overline{\ex{B}[\Box \overline{V}]_{=1}},

1464: & \quad

1465: \ex{A}[\Box V]_{>0} &= \overline{\ex{B}[\Diamond \overline{V}]_{=1}}.

1466: \end{xalignat*}

1467: 

1468: 

1469: \begin{theorem}[Decidability of qualitative symmetric probabilistic LCS-games]

1470: For symmetric probabilistic LCS-games $\L$ and regular regions $V$, the

1471: sets $\ex{A}[\Diamond V]_{=1}$, $\ex{A}[\Diamond V]_{>0}$, $\ex{A}[\Box

1472: V]_{=1}$, and $\ex{A}[\Box V]_{>0}$ are (effective) regions. Hence

1473: qualitative reachability and invariant games are decidable on GLCS's.

1474: \end{theorem}

1475: \begin{proof}[Sketch]

1476: These sets can be defined by guarded $L_\mu$ terms.

1477: %

1478: \qed

1479: \end{proof}

1480: 

1481: \iffalse

1482: \paragraph*{\bf \em Persistence games.}

1483: $A$ attempts to ensure $\Diamond \Box V$ with probability 1,

1484: no matter how $B$ behaves.

1485: $$\ex{A} [\Diamond \Box V]_{=1}

1486:  \stackrel{\text{def}}{=}

1487:   \ex{A}\bigl[ \Diamond \ex{A} [\Box V]_{=1} \bigr]_{=1}

1488: $$

1489: $A$ attempts to ensure $\Diamond \Box V$ with probability $>0$,

1490: no matter how $B$ behaves.

1491: $$\ex{A} [\Diamond \Box V]_{>0}

1492:  \stackrel{\text{def}}{=}

1493:   \ex{A}\bigl[ \Diamond \ex{A} [\Box V]_{=1} \bigr]_{>0}

1494: $$

1495: 

1496: 

1497: \paragraph*{\bf \em Repeated reachability games.}

1498: $A$'s goal is to visit $V$ infinitely often with probability 1,

1499: no matter how $B$ behaves.

1500: $$\ex{A} [\Box \Diamond V]_{=1}

1501: \stackrel{\text{def}}{=}

1502: \nu Y. \ex{A} [\Diamond (V \cap (\varphi_A(Y) \cup \varphi_B(Y)))]_{=1}

1503: $$

1504: where

1505: $$\begin{array}{lcl}

1506:   \varphi_A(Y) & = &  Q_A \cap \Pre_{\text{perfect}}

1507:     (\Kd(Y)) \\

1508:   \varphi_B(Y) & = & Q_B \cap

1509:      \wPre_{\text{perfect}}(\Kd(Y))

1510: \end{array}

1511: $$

1512: 

1513: 

1514: 

1515: 

1516: \paragraph*{\bf \em Parity games.}

1517: 

1518: .....

1519: 

1520: 

1521: \fi

1522: 

1523: 

1524: 

1525: 

1526: 

1527: %%% Local Variables:

1528: %%% mode: latex

1529: %%% TeX-master: "main-regular"

1530: %%% End:

1531: 

1532: % LocalWords:  prob lcs.tex phs Exp MDP LCS fireable NPLCS LCS's iff eq

1533: % LocalWords:  fixpoint

1534: %%% TEXEXPAND: END FILE ./sec-prob-lcs.tex

1535: % NOT YET READY \input{sec-concurrent-lcs}

1536: 

1537: %%% TEXEXPAND: INCLUDED FILE MARKER ./sec-concl.tex

1538: %%% $Id: sec-concl.tex,v 1.2 2006/05/12 20:44:30 phs Exp $

1539: 

1540: 

1541: 

1542: \section{Conclusion}

1543: %===================

1544: \label{sec-concl}

1545: 

1546: 

1547: We defined a notion of upward/downward-guarded fixpoint expressions that

1548: define subsets of a well-quasi-ordered set. For these guarded fixpoint

1549: expressions, a finite convergence theorem is proved, that shows how the

1550: fixpoints can be evaluated with a finite number of operations. This has a

1551: number of applications, in particular in the symbolic verification of

1552: well-structured systems, our original motivation. We illustrate this in the

1553: second part of the paper, with lossy channel systems as a target. For these

1554: systems, we derive in an easy and uniform way, a number of decidability

1555: theorems that extend or generalize the main existing results in the

1556: verification of temporal properties or game-theoretical properties.

1557: 

1558: These techniques can be applied to other well-structured systems, with a

1559: region algebra built on, e.g., upward-closed sets. Admittedly, many

1560: examples of well-structured systems do not enjoy closure properties as nice

1561: as our Lemma~\ref{lem-pre-guarded} for LCS's, which will make it more

1562: difficult to express interesting properties in the guarded fragment of

1563: $L_\mu$. But this can still be done, as witnessed

1564: by~\cite{raskin03,raskin05} where the authors introduced a concept of

1565: $B$-games and $BB$-games that captures some essential closure assumptions

1566: allowing the kind of rewritings and unfoldings we have justified with

1567: Lemma~\ref{lem-pre-guarded}.

1568: 

1569: 

1570: 

1571: 

1572: %%% Local Variables:

1573: %%% mode: latex

1574: %%% TeX-master: "main-regular"

1575: %%% End:

1576: % LocalWords:

1577: 

1578: % LocalWords:  fixpoint fixpoints LCS's unfoldings

1579: %%% TEXEXPAND: END FILE ./sec-concl.tex

1580: 

1581: %\bibliographystyle{alpha}

1582: \begin{thebibliography}{10}

1583: 

1584: \bibitem{ABRS-icomp}

1585: P.~A. Abdulla, N.~Bertrand, A.~Rabinovich, and {\relax Ph}~Schnoebelen.

1586: \newblock Verification of probabilistic systems with faulty communication.

1587: \newblock {\em Information and Computation}, 202(2):141--165, 2005.

1588: 

1589: \bibitem{abdulla2003b}

1590: P.~A. Abdulla, A.~Bouajjani, and J.~d'{\aftergroup\ignorespaces} Orso.

1591: \newblock Deciding monotonic games.

1592: \newblock In {\em Proc.\ 17th Int.\ Workshop Computer Science Logic (CSL 2003)

1593:   and 8th Kurt G{\"o}del Coll.\ (KGL 2003), Vienna, Austria, Aug.\ 2003},

1594:   volume 2803 of {\em Lecture Notes in Computer Science}, pages 1--14.

1595:   Springer, 2003.

1596: 

1597: \bibitem{abdulla2000c}

1598: P.~A. Abdulla, K.~{\v{C}}er{\=a}ns, B.~Jonsson, and Yih-Kuen Tsay.

1599: \newblock Algorithmic analysis of programs with well quasi-ordered domains.

1600: \newblock {\em Information and Computation}, 160(1/2):109--127, 2000.

1601: 

1602: \bibitem{abdulla96c}

1603: P.~A. Abdulla and B.~Jonsson.

1604: \newblock Undecidable verification problems for programs with unreliable

1605:   channels.

1606: \newblock {\em Information and Computation}, 130(1):71--90, 1996.

1607: 

1608: \bibitem{abdulla96b}

1609: P.~A. Abdulla and B.~Jonsson.

1610: \newblock Verifying programs with unreliable channels.

1611: \newblock {\em Information and Computation}, 127(2):91--101, 1996.

1612: 

1613: \bibitem{abdulla2001b}

1614: P.~A. Abdulla and B.~Jonsson.

1615: \newblock Channel representation in protocol verification.

1616: \newblock In {\em Proc.\ 12th Int.\ Conf.\ Concurrency Theory (CONCUR 2001),

1617:   Aalborg, Denmark, Aug.\ 2001}, volume 2154 of {\em Lecture Notes in Computer

1618:   Science}, pages 1--15. Springer, 2001.

1619: 

1620: \bibitem{arnold2001}

1621: A.~Arnold and D.~Niwi{\'n}ski.

1622: \newblock {\em Rudiments of {$\mu$}-Calculus}, volume 146 of {\em Studies in

1623:   Logic and the Foundations of Mathematics}.

1624: \newblock Elsevier Science, 2001.

1625: 

1626: \bibitem{BBS-ipl}

1627: C.~Baier, N.~Bertrand, and {\relax Ph}.~Schnoebelen.

1628: \newblock A note on the attractor-property of infinite-state {Markov} chains.

1629: \newblock {\em Information Processing Letters}, 97(2):58--63, 2006.

1630: 

1631: \bibitem{BBS-acmtocl06}

1632: C.~Baier, N.~Bertrand, and {\relax Ph}.~Schnoebelen.

1633: \newblock Verifying nondeterministic probabilistic channel systems against

1634:   \(\omega\)-regular linear-time properties.

1635: \newblock {\em ACM Transactions on Computational Logic}, 2006.

1636: \newblock To appear, available at \url{http://arxiv.org/abs/cs.LO/0511023}.

1637: 

1638: \bibitem{BFLS-atva2005}

1639: S.~Bardin, A.~Finkel, J.~Leroux, and {\relax Ph}.~Schnoebelen.

1640: \newblock Flat acceleration in symbolic model checking.

1641: \newblock In {\em Proc.\ 3rd Int.\ Symp.\ Automated Technology for Verification

1642:   and Analysis (ATVA 2005), Taipei, Taiwan, Oct.\ 2005}, volume 3707 of {\em

1643:   Lecture Notes in Computer Science}, pages 474--488. Springer, 2005.

1644: 

1645: \bibitem{boigelot2003}

1646: B.~Boigelot.

1647: \newblock On iterating linear transformations over recognizable sets of

1648:   integers.

1649: \newblock {\em Theoretical Computer Science}, 309(1--3):413--468, 2003.

1650: 

1651: \bibitem{BLW03}

1652: B.~Boigelot, A.~Legay, and P.~Wolper.

1653: \newblock Iterating transducers in the large (extended abstract).

1654: \newblock In {\em Proc.\ 15th Int.\ Conf.\ Computer Aided Verification (CAV

1655:   2003), Boulder, CO, USA, July 2003}, volume 2725 of {\em Lecture Notes in

1656:   Computer Science}, pages 223--235. Springer, 2003.

1657: 

1658: \bibitem{bouajjani2004}

1659: A.~Bouajjani, P.~Habermehl, and T.~Vojnar.

1660: \newblock Abstract regular model checking.

1661: \newblock In {\em Proc.\ 16th Int.\ Conf.\ Computer Aided Verification (CAV

1662:   2004), Boston, MA, USA, July 2004}, volume 3114 of {\em Lecture Notes in

1663:   Computer Science}, pages 372--386. Springer, 2004.

1664: 

1665: \bibitem{bouajjani2000b}

1666: A.~Bouajjani, B.~Jonsson, M.~Nilsson, and T.~Touili.

1667: \newblock Regular model checking.

1668: \newblock In {\em Proc.\ 12th Int.\ Conf.\ Computer Aided Verification (CAV

1669:   2000), Chicago, IL, USA, July 2000}, volume 1855 of {\em Lecture Notes in

1670:   Computer Science}, pages 403--418. Springer, 2000.

1671: 

1672: \bibitem{cece95}

1673: G.~C\'ec\'e, A.~Finkel, and S.~{Purushothaman Iyer}.

1674: \newblock Unreliable channels are easier to verify than perfect channels.

1675: \newblock {\em Information and Computation}, 124(1):20--31, 1996.

1676: 

1677: \bibitem{chatterje05}

1678: K.~Chatterjee, L.~de{ }Alfaro, and T.~A. Henzinger.

1679: \newblock The complexity of stochastic {Rabin} and {Streett} games.

1680: \newblock In {\em Proc.\ 32nd Int.\ Coll.\ Automata, Languages, and Programming

1681:   (ICALP 2005), Lisbon, Portugal, July 2005}, volume 3580 of {\em Lecture Notes

1682:   in Computer Science}, pages 878--890. Springer, 2005.

1683: 

1684: \bibitem{alfaro2001b}

1685: L.~de{ }Alfaro, T.~A. Henzinger, and R.~Majumdar.

1686: \newblock Symbolic algorithms for infinite-state games.

1687: \newblock In {\em Proc.\ 12th Int.\ Conf.\ Concurrency Theory (CONCUR 2001),

1688:   Aalborg, Denmark, Aug.\ 2001}, volume 2154 of {\em Lecture Notes in Computer

1689:   Science}, pages 536--550. Springer, 2001.

1690: 

1691: \bibitem{finkel94}

1692: A.~Finkel.

1693: \newblock Decidability of the termination problem for completely specificied

1694:   protocols.

1695: \newblock {\em Distributed Computing}, 7(3):129--135, 1994.

1696: 

1697: \bibitem{finkel98b}

1698: A.~Finkel and {\relax Ph}.~Schnoebelen.

1699: \newblock Well-structured transition systems everywhere!

1700: \newblock {\em Theoretical Computer Science}, 256(1--2):63--92, 2001.

1701: 

1702: \bibitem{Graedel-Thomas-Wilke-LNCS}

1703: E.~Gr{\"{a}}del, W.~Thomas, and T.~Wilke, editors.

1704: \newblock {\em Automata, Logics, and Infinite Games: A Guide to Current

1705:   Research}, volume 2500 of {\em Lecture Notes in Computer Science}.

1706: \newblock Springer, 2002.

1707: 

1708: \bibitem{habermehl04}

1709: P.~Habermehl and T.~Vojnar.

1710: \newblock Regular model checking using inference of regular languages.

1711: \newblock In {\em Proc.\ 6th Int.\ Workshop on Verification of Infinite State

1712:   Systems (INFINITY 2004), London, UK, Sep.\ 2004}, volume 138(3) of {\em

1713:   Electronic Notes in Theor.\ Comp.\ Sci.}, pages 21--36. Elsevier Science,

1714:   2005.

1715: 

1716: \bibitem{henzinger2005}

1717: T.~A. Henzinger, R.~Majumdar, and J.-F. Raskin.

1718: \newblock A classification of symbolic transition systems.

1719: \newblock {\em ACM Trans.\ Computational Logic}, 6(1):1--32, 2005.

1720: 

1721: \bibitem{kesten2001}

1722: Y.~Kesten, O.~Maler, M.~Marcus, A.~Pnueli, and E.~Shahar.

1723: \newblock Symbolic model checking with rich assertional languages.

1724: \newblock {\em Theoretical Computer Science}, 256(1--2):93--112, 2001.

1725: 

1726: \bibitem{kruskal72}

1727: J.~B. Kruskal.

1728: \newblock The theory of well-quasi-ordering: {A} frequently discovered concept.

1729: \newblock {\em Journal of Combinatorial Theory, Series A}, 13(3):297--305,

1730:   1972.

1731: 

1732: \bibitem{KucSch-TCS}

1733: A.~Ku{\v c}era and {\relax Ph}.~Schnoebelen.

1734: \newblock A general approach to comparing infinite-state systems with their

1735:   finite-state specifications.

1736: \newblock {\em Theoretical Computer Science}, 2006.

1737: \newblock To appear.

1738: 

1739: \bibitem{martin98}

1740: D.~A. Martin.

1741: \newblock The determinacy of {Blackwell} games.

1742: \newblock {\em The Journal of Symbolic Logic}, 63(4):1565--1581, 1998.

1743: 

1744: \bibitem{mayr-unreliable}

1745: R.~Mayr.

1746: \newblock Undecidable problems in unreliable computations.

1747: \newblock {\em Theoretical Computer Science}, 297(1--3):337--354, 2003.

1748: 

1749: \bibitem{milner85}

1750: E.~C. Milner.

1751: \newblock Basic {WQO}- and {BQO}-theory.

1752: \newblock In I.~Rival, editor, {\em Graphs and Order. The Role of Graphs in the

1753:   Theory of Ordered Sets and Its Applications}, pages 487--502. D.\ Reidel

1754:   Publishing, 1985.

1755: 

1756: \bibitem{OuaknineWorrell06}

1757: J.~Ouaknine and J.~Worrell.

1758: \newblock On metric temporal logic and faulty {T}uring machines.

1759: \newblock In {\em Proc.\ 9th Int.\ Conf.\ Foundations of Software Science and

1760:   Computation Structures (FOSSACS 2006), Vienna, Austria, Mar.\ 2006}, volume

1761:   3921 of {\em Lecture Notes in Computer Science}, pages 217--230. Springer,

1762:   2006.

1763: 

1764: \bibitem{perrin90}

1765: D.~Perrin.

1766: \newblock Finite automata.

1767: \newblock In J.~van Leeuwen, editor, {\em Handbook of Theoretical Computer

1768:   Science}, volume~B, chapter~1, pages 1--57. Elsevier Science, 1990.

1769: 

1770: \bibitem{raskin03}

1771: J.-F. Raskin, M.~Samuelides, and L.~Van{ }Begin.

1772: \newblock Petri games are monotonic but difficult to decide.

1773: \newblock Tech.~Report 2003.21, Centre F\'ed\'er\'e en V\'erification, 2003.

1774: \newblock Available at \url{http://www.ulb.ac.be/di/ssd/cfv/TechReps}.

1775: 

1776: \bibitem{raskin05}

1777: J.-F. Raskin, M.~Samuelides, and L.~Van{ }Begin.

1778: \newblock Games for counting abstractions.

1779: \newblock In {\em Proc.\ 4th Int.\ Workshop on Automated Verification of

1780:   Critical Systems (AVoCS 2004), London, UK, Sep.\ 2004}, volume 128(6) of {\em

1781:   Electronic Notes in Theor.\ Comp.\ Sci.}, pages 69--85. Elsevier Science,

1782:   2005.

1783: 

1784: \bibitem{voronkov-csl03}

1785: T.~Rybina and A.~Voronkov.

1786: \newblock Fast infinite-state model checking in integer-based systems.

1787: \newblock In {\em Proc.\ 17th Int. Workshop Computer Science Logic (CSL 2003)

1788:   and 8th Kurt G{\"o}del Coll.\ (KGL 2003), Vienna, Austria, Aug.\ 2003},

1789:   volume 2803 of {\em Lecture Notes in Computer Science}, pages 546--573.

1790:   Springer, 2003.

1791: 

1792: \bibitem{Sch-voss}

1793: {\relax Ph}.~Schnoebelen.

1794: \newblock The verification of probabilistic lossy channel systems.

1795: \newblock In {\em Validation of Stochastic Systems -- A Guide to Current

1796:   Research}, volume 2925 of {\em Lecture Notes in Computer Science}, pages

1797:   445--465. Springer, 2004.

1798: 

1799: \bibitem{sifakis82}

1800: J.~Sifakis.

1801: \newblock A unified approach for studying the properties of transitions

1802:   systems.

1803: \newblock {\em Theoretical Computer Science}, 18:227--258, 1982.

1804: 

1805: \end{thebibliography}

1806: 

1807: %% \newpage

1808: 

1809: %% \appendix

1810: %% \pagestyle{myheadings}

1811: %% \pagenumbering{roman}

1812: 

1813: %% \input{proofs-mucalculus}

1814: 

1815: \end{document}

1816: