1: % jcl.tex

2: % for submission to ACM Transactions on Computational Logic

3: 

4: \documentclass{esub2acm}

5: \begin{document}

6: 

7: 

8: \setlength{\oddsidemargin}{1em}

9: \setlength{\evensidemargin}{1em}

10: \setlength{\textwidth}{160mm}

11: \setlength{\textheight}{220mm}

12:  

13: %\usepackage{aaai}

14: \include{times-roman.sty}

15: %\include{zed-cm.sty}

16: %\include{csp-cm.sty}

17: %\usepackage{csptl}

18: %\include{drafthead}

19: %\usepackage{proof}

20: %\usepackage{lncs}

21: 

22: % \setlength{\parskip}{2ex}

23: % \setlength{\parindent}{0ex}

24: 

25: %\theorembodyfont{\upshape}

26:  \newtheorem{Theorem}{Theorem}

27:  \newtheorem{Property}{Property}

28:  \newtheorem{Proof}{Proof}

29:  \newtheorem{Lemma}{Lemma}

30:  \newtheorem{Proposition}{Proposition}

31:  \newtheorem{SubProof}{Proof}[Proof]

32:  \newtheorem{Definition}{Definition}

33:  \newtheorem{Axiom}{Axiom}

34:  \newtheorem{Condition}{Condition}

35:  

36: \input{psfig.tex}

37: 

38: 

39: 

40: \newcommand{\lmset}{\{\!|}

41: \newcommand{\rmset}{|\!\}}

42: \def \mset#1{{\lmset \! #1 \! \rmset}}

43: \def\spades{\spadesuit}

44: \def \trace#1{\langle #1\rangle}  

45: \let \ge        \geqslant

46: \let \le        \leqslant

47: \newcommand{\probthen}{\mapsto}

48: \newcommand{\until}{{~~\cal U~}}

49: \newcommand{\Prob}{\mathit Pr}

50: \newcommand{\prob}{\mathit prob}

51: \def \defeq {\stackrel{\mathrm{def}}{=}}

52: \def \undef {\perp}

53: \def\always{\ensuremath{\Box}}

54: \def\blackright{\mbox{$\;\;\-\!\!\!-\!\!\!\!-\!\!\!\triangleright$}}

55: \def \nat   {\mathbf{N}}

56: \def \real   {\mathbf{R}}

57: \def \power  {\mathbf{P}}

58: \def \union  {\bigcup}

59: \def \inter  {\bigcap}

60: \def \hide   {\backslash}

61: 

62: \def\mapsleft {\leftarrow\!\!\dashv}

63: 

64: 

65: \newcommand{\bc}{\begin{com}}

66: \newcommand{\ec}{\end{com}}

67: 

68: \newenvironment{com}[1]{\textmd{**\textsf{#1}**}}

69: 

70: \newsavebox{\savepar}

71: \newenvironment{boxit}{\begin{lrbox}{\savepar}

72:   \begin{minipage}[b]{5.2in}}

73:   {\end{minipage}\end{lrbox}\fbox{\usebox{\savepar}}}

74: 

75: 

76: \def\drop{\array[t]{@{}l@{}}}

77: \let\enddrop=\endarray

78: \def\ddrop{\array[t]{@{}ll@{}}}

79: \let\endddrop=\endarray

80: %\def\real{{\bbold R}}

81: 

82: \title{Stochastic Model Checking for Multimedia}

83: 

84: %[Ed: boxes at end of defns]

85: 

86: \author{Jeremy Bryans, Howard Bowman and John Derrick\\

87: Computing Laboratory, University of Kent, Canterbury, CT2 7NF,

88:  UK.\\ (Phone: + 44 1227 764000, Email: J.Derrick@ukc.ac.uk.)}

89: 

90: \begin{abstract}

91: Modern distributed systems include a class of applications in which

92: non-functional requirements are important. In particular, these

93: applications include multimedia facilities where real time constraints

94: are crucial to their correct functioning. In order to specify such

95: systems it is necessary to describe that events occur at times given

96: by probability distributions and  stochastic automata have emerged as a

97: useful technique by which such systems can be specified and verified.

98: 

99: However, stochastic descriptions are very general, in particular they

100: allow the use of general probability distribution functions, and

101: therefore their verification can be complex.  In the last few years,

102: model checking has 

103: emerged as a useful verification tool for large systems.    In this paper we

104: describe two model checking algorithms for stochastic automata.  These

105: algorithms consider how properties written in a simple probabilistic

106: real-time logic can be checked against a given stochastic automaton.

107: \end{abstract}

108: %\category{}{}{}[]  % **May have multiple occurrences.**

109: %\terms{}

110: \keywords{Distributed systems, stochastic automata, model checking}

111: \begin{bottomstuff}

112:   \begin{authinfo}

113:     \name{J. Bryans} 	  

114:    \address{Computing Laboratory, University of Kent at Canterbury,

115:     Canterbury, Kent, CT2 7NF  PHONE: +44 1227 827697} 	  

116:     \name{H. Bowman} 	  

117:     \address{Computing Laboratory, University of Kent at Canterbury,

118:     Canterbury, Kent, CT2 7NF  PHONE: +44 1227 823815} 	  

119:     \name{J. Derrick} 	  

120:     \address{Computing Laboratory, University of Kent at Canterbury,

121:     Canterbury, Kent, CT2 7NF  PHONE: +44 1227 827570} 	  

122:     %\affiliation{} %[OPTIONAL] **May have multiple occurrences.**

123:     %\biography{}   %[OPTIONAL] **May have multiple occurrences.**

124:   \end{authinfo}

125: \permission

126: \end{bottomstuff}

127: 

128: \markboth{J. Bryans, H. Bowman and J. Derrick}{Stochastic

129: Model-Checking for Multimedia}

130: \maketitle

131: 

132: \section{Introduction}

133: 

134: In this paper we describe and compare two model checking algorithms

135: for stochastic automata.  The reason for building such model checking

136: algorithms is to support the verification of non-functional properties

137: in distributed multimedia systems.

138: 

139: The advent of distributed multimedia applications such as video

140: conferencing, collaborative virtual environments, video on demand etc,

141: place great demands on the specification and design of such systems

142: because of the need to describe and verify non-functional

143: requirements~\cite{tempo-book}. These non-functional requirements

144: typically involve real time constraints such as placing bounds on

145: end-to-end latency, and are often called {\it Quality of Service

146: (QoS)}~\cite{tempo-book} requirements because they reflect the overall

147: quality of delivery as opposed to the functional aspects.

148: 

149: In order to specify and verify such constraints it is necessary not

150: only to be able to describe deterministic timing concerns but also

151: probabilistic and stochastic systems. That is, in practice timings

152: cannot be assumed to be fixed (deterministic timings) but events can

153: occur at different times with particular probabilities. Therefore it

154: is necessary to describe timings that occur according to certain {\it

155: probability distributions}.  For example, in a network specification

156: it is not sufficient to assume that the packet deliveries arrive at

157: fixed predetermined times, instead we need to model the system where

158: they might arrive at times determined by (for example) an exponential

159: distribution. 

160: 

161: There are now a number of techniques which can be used to describe

162: such systems, e.g. Queueing Systems~\cite{Kleinrock-1-1975},

163: Generalised Stochastic Petri-nets

164: \cite{Ajmone_Marsam-Conte-Balbo-1984}, Markov

165: Chains~\cite{Stewart-1994}, generalised semi-Markov

166: processes~\cite{Glynn-1989}, Stochastic Process

167: Algebra~\cite{Hillston-1996} and Stochastic

168: Automata~\cite{D'Argenio-1999} etc. In this paper we consider

169: Stochastic Automata (which are related to timed

170: automata~\cite{Alur-Dill-1994}). We define two {\em model

171: checking}~\cite{Baier-Kwiatkowska-1998} algorithms for them.

172: 

173: Stochastic automata are a very promising specification and

174: verification paradigm.  In particular they allow the study of both

175: functional and non-functional requirements within the same

176: description, giving a more complete view of overall performance than,

177: say, a queueing theory description of the problem.  They also support

178: not just exponential distributions but general distributions. The

179: issue here is the following. In a stochastic specification we need to

180: associate a distribution function $F$ with an action $a$ so that we

181: can describe the probability of the time delay after which $a$ can

182: happen.  Stochastic automata naturally allow general distributions, in

183: contrast say to stochastic process algebras which usually restrict

184: themselves to exponential distributions~\cite{Hillston-1996}.

185: 

186:  In practice it is unrealistic to only consider exponential

187: distributions and it is necessary  for arbitrary  distributions

188: (e.g. uniform, gamma, deterministic etc) to be considered. 

189: For example, it is often assumed that packet lengths are exponentially

190: distributed. However, in reality this is not the case,

191: rather they are either of constant length (as in ATM cells~\cite{Tanenbaum96})

192: or they are uniformly distributed with minimum and maximum size (as in Ethernet

193: frames~\cite{Tanenbaum96}). Stochastic automata allow such arbitrary

194: distributions 

195: to be used.

196: 

197: There are ostensibly two ways to move from the tractable case of

198: exponential distributions to the less tractable case of generalised

199: distributions.  One approach is to make small generalisations of

200: markov chains by allowing limited forms of non-memoryless behaviour

201: (see e.g. GSPNs~\cite{Ajmone_Marsam-Conte-Balbo-1984}).  However, the

202: problem with this approach is that there will 

203: always be classes of distributions that cannot be modelled.  The

204: alternative is to allow any distribution, but then use heuristics and

205: coarse approximation techniques to contain the problem of

206: intractability.  The majority of work on this topic follows the first

207: of these approaches.  However here we investigate the feasibility of

208: the second approach and thus we impose few constraints on the

209: generality of the distributions we allow in our stochastic automata.  

210: 

211: Because stochastic automata are related to  timed automata, verification

212: strategies for stochastic automata can be derived by using the extensive work

213: on verification for timed automata, see e.g.~\cite{Uppaal}

214: \cite{Kronos} \cite{Hytech}. 

215: The particular verification technique we consider is model

216: checking~\cite{Alur-Courcoubetis-Dill-1990}.  This is perhaps the most

217: successful 

218: technique to have arisen from concurrency theory.  The basic approach

219: is to show that an automaton description of a system satisfies a

220: temporal logic property, see  Figure~\ref{fig:model-checker}.

221: 

222: 

223: % \includegraphics{model-checker.pic}

224: 

225: 

226: \begin{figure*}[t]

227: \begin{center}

228:    \ \psfig{figure=model-checker.pic,height=2in,width=5in}

229:  \end{center}

230:  \caption{Model checker}

231: \label{fig:model-checker}

232:  \end{figure*}

233: 

234: 

235: In accordance with a number of other workers,

236: e.g.~\cite{Baier-Katoen-Hermanns-1999}, we view the application of

237: model checking to analysis of stochastic systems as a very exciting

238: combination, since it provides a form of generalised transient

239: analysis --- for example the property $[ \lnot error \!

240: \until_{\!\!\!<1000} \; error] < 0.01$ states that the probability of

241: first reaching 

242: an {\em error} state within 1000 time units is less than 1 percent,

243: and whether a particular stochastic system satisfies this property can

244: be investigated.    

245: 

246: 

247: In defining our model checking algorithm we draw heavily on the

248: experience of model checking timed automata

249: e.g.~\cite{Uppaal}. However, the move from timed to stochastic leads

250: to new issues that must be tackled. In particular, many of the

251: properties that we wish to verify are inherently probabilistic.

252: Conventional model checking allows us to answer questions such as ``Is

253: a particular sequence of events possible?'', but in stochastic model

254: checking we want to ask ``What is the probability of this sequence of

255: events?''.  To do this we will check an automaton against a simple

256: probabilistic temporal 

257: logic.

258: 

259: We present two approaches to model checking stochastic automata.  Both

260: approaches are enumerative in the sense that, in showing whether a

261: property holds, they enumerate reachable configurations of the

262: system.  However, the methods by which they determine the probability

263: of being in a particular configuration are quite different.

264: Specifically, one derives probabilities by integrating the relevant

265: probability density functions, while the second responds to the

266: difficulties incurred in evaluating these integrals (which will become

267: clear during the paper) by employing a discretisation process.

268: 

269: 

270: The structure of the paper is as follows. In

271: Section~\ref{sec:stochastic-automata} we introduce stochastic automata

272: illustrated by a simple example.  In Section \ref{sec:logic} we define

273: a small probabilistic real-time logic, in which we can express simple

274: properties that we wish to check our stochastic automata against.  The

275: first algorithm is presented in Section~\ref{sec:alg-one}, and the

276: second is presented in~\ref{sec:alg-two}.  Section~\ref{sec:example}

277: looks at an example of the operation of the second algorithm and

278: Section~\ref{sec:proof} considers some issues of correctness and

279: convergence relating to the second algorithm, and

280: Section~\ref{sec:complexity} looks at the time and space complexity.

281: We conclude in 

282: Section~\ref{sec:conclusions}. 

283: 

284: 

285: 

286: 

287: 

288: % 

289: % We also give the full model checking

290: % algorithm, and we conclude in Section \ref{sec:conclusions}.

291: %    

292: % 

293: 

294: \section{Stochastic Automata} \label{sec:stochastic-automata}

295: 

296: In this section we introduce stochastic automata using a small

297:  example.  Stochastic automata are related to timed

298:  automata~\cite{Alur-Dill-1994}, however stochastic clock settings are

299:  used, instead of the strictly deterministic timings used in timed

300:  automata.  We begin with the formal definition of stochastic

301:  automata, then present a simple example.  We use the definition of

302:  stochastic automata presented

303:  in~\cite{D'Argenio-Katoen-Brinksma-1998}.

304: \begin{Definition}{\upshape

305: A {\em stochastic automaton} is a structure $({\cal S},s_0,{\cal

306:   C},{\bf A},\blackright,\kappa,F)$ where: 

307: \begin{itemize}

308: \item[$\bullet$] ${\cal S}$ is a set of {\em locations} with $s_0 \in

309: {\cal S}$ being the 

310:   {\em initial location}, ${\cal C}$ is the set of all {\em clocks},

311:   and {\bf A} is a set of {\em actions}.

312: \item[$\bullet$] $\blackright \subseteq {\cal S} \times ( {\bf A} \times

313:   {\cal P}_{\mathrm{fin}}({\cal C})) \times {\cal S}$ is the set of

314:   {\em edges}.  If $s$ and $s'$ are states, $a$ is an action and $C$

315:   is a subset of ${\cal C}$, then we 

316:   denote the edge $(s,a,C,s') \in \blackright$ by $s

317:   \stackrel{a,C}{\blackright} s'$ and we say that $C$ is the {\em

318:   trigger set} of action $a$.  We use   $s \stackrel{a}{\blackright}

319:   s'$ as a 

320:   shorthand notation  for $\exists C.s \stackrel{a, C}{\blackright} s'$.

321: 

322: \item[$\bullet$] $\kappa : {\cal S} \rightarrow {\cal P}_{\mathrm

323: {fin}}(C)$ is the {\em clock setting function}, and indicates which

324: clocks are to be set in which states, where ${\cal

325: P}_{\mathrm{fin}}({\cal C})$ is the finite powerset of clocks.

326: 

327: \item[$\bullet$] $F: {\cal C} \rightarrow ({\cal R} \rightarrow [0,1])$

328: assigns to each clock a {\em distribution function} such that, for any

329: clock $x$, $F(x)(t) = 0$ for $t < 0$; we write $F_x$ for $F(x)$ and

330: thus $F_x(t)$ states the probability that the value selected for the

331: clock $x$ is less than or equal to $t$.

332: \end{itemize}

333: Each clock $x \in {\cal C}$ has an associated random

334: variable with distribution $F_x$.  

335: To facilitate the model checking, we introduce a function $\xi$ which

336: associates locations with sets of atomic propositions.

337: \[

338: \xi:  {\cal S} \mapsto {\cal P}(AP)

339: \]

340: where AP is the set of atomic propositions.  $\hfill\Box$ }\end{Definition}

341: 

342: It is necessary to impose some limitations on the stochastic automata

343: which can be used with the model checking algorithms.  In particular,

344: we require that each clock distribution function $F_x$ must have a

345: positive finite upper bound and a non-negative lower bound, and must

346: be continuous between these bounds.  The finiteness constraints mean

347: that there are certain distribution functions which we must

348: approximate.  We further assume that clocks are only

349: used on transitions emanating from  states in which they are set.

350: 

351: % \begin{center}

352: % \includegraphics{stoch-automaton2.pic}

353: % \\

354: % \includegraphics{three-graphs.pic}

355: % %\caption{The packet producer} \label{fig:stoch-automaton}

356: % \end{center}

357: 

358:  

359:  

360:  \begin{figure*}

361:  \begin{center}

362:    \ \psfig{figure=stoch-automaton2.pic,height=2in,width=2in}

363:  \\

364:    \ \psfig{figure=three-graphs.pic,height=1in,width=4in}

365:  \end{center}

366:  

367:  \caption{The packet producer} \label{fig:stoch-automaton}

368:  \end{figure*}

369:  

370: As an example, consider the simple packet producer (which is a

371: component in  a large multimedia specification) 

372: in Figure~\ref{fig:stoch-automaton}.  This is written 

373: \[

374: \begin{array}{l}

375: (\{s_0,s_1,s_2\},s_0,\{x,y,z\}, \\ 

376: \{tryagain, conc, send, fail\}, \blackright,\kappa,\{F_x,F_y,F_z\})

377: \end{array}

378: \]

379: where 

380: 

381: \[

382: \begin{array}{rcl}

383: \blackright & = & \{(s_0,tryagain,\{x\},s_0), (s_0,conc,\{x\},s_1), \\

384: & & (s_1,send,\{z\},s_0), (s_0,fail,\{y\},s_2)\} \\

385: \end{array}

386: \]

387: \[

388: \begin{array}{ccc}

389: \kappa(s_0)  =  \{x,y\}, &

390: \kappa(s_1)  =  \{z\}, &

391: \kappa(s_2)  =  \{\} 

392: \end{array}

393: \]

394: and the 

395: distribution functions for clocks $x$, $y$ and $z$ are 

396: \[

397: \begin{array}{rcl}

398: F_x(t)  & = & 2t-t^2, \mathrm{if~~} t\in[0,1] \\

399:         & = &      0, \mathrm{if~~}  t < 0 \\

400:         & = &    1, \mathrm{otherwise} \\

401: \end{array}

402: \]

403: \[

404: \begin{array}{rcl}

405: F_y(t) & = & t^2, \mathrm{if~~}  t\in[0,1] \\

406:        & = &       0,  \mathrm{if~~}  t < 0  \\

407:        & = &      1,      \mathrm{otherwise}

408: \end{array}

409: \]

410: and

411: \[

412: \begin{array}{rcl}

413: F_z(t) & = & t, \mathrm{if~~}  t\in[0,1] \\

414:        & = &       0,  \mathrm{if~~}  t < 0  \\

415:        & = &      1,      \mathrm{otherwise}

416: \end{array}

417: \]

418:  as depicted. The horizontal axis measures time, and the vertical

419: axis measures the probability of the clock being set to a value less

420: than that time. 

421: 

422: The packet producer starts in location $s_0$, and attempts to

423: establish a connection with its medium.  Three options are possible at

424: this stage.  Either the medium allows a connection, the medium tells

425: the packet producer to try again or the medium takes too long and the

426: connection fails (is timed out).  These options are modelled in the

427: automaton by setting clocks $x$ and $y$ according to the functions

428: $F_x$ and $F_y$.  If clock $x$ expires first then there is a

429: nondeterministic choice between the transition labelled  {\em conc}

430: (which moves the automaton to state $s_1$)  and the transition labelled 

431: {\em tryagain} (which moves the automaton back to state $s_0$).  This

432: choice is nondeterministic because in reality it would depend on 

433: the medium, which we have not specified here.  If clock $y$ expires

434: first, then action {\em fail} is triggered (we say that $\{y\}$ is the

435: {\em trigger set} of {\em fail}) and the automaton moves to state

436: $s_2$.  This corresponds to the medium taking too long to respond, and

437: nothing further happens.     

438: 

439: This example has been chosen because it is small enough that we can

440: show, in their entirety, the set of configurations that our model

441: checking algorithms enumerate.  Thus it can be used to illustrate our

442: two algorithms.  But, in addition, we have chosen it because it is

443: canonical in the sense that it illustrates the key concepts of

444: stochastic automata, e.g. simultaneous enabling of multiple

445: transitions generating non-determinism.  The reader should also notice

446: that this is a good example of a situation in which steady-state analysis

447: is not interesting.  Specifically, in the steady state, all the

448: probability mass will be in state $s_2$.  Thus, the sort of questions

449: we wish to ask about such  a system are about its transient behaviour,

450: e.g. what is the probability of reaching state $s_2$ within a

451: particular period of time  and indeed this is exactly the type of

452: question we will be able to formulate with the logic we introduce in

453: the next section and answer with our model checking algorithms. 

454: 

455: \section{A Probabilistic Real-Time Temporal Logic} 

456: \label{sec:PRTL}

457: \label{sec:logic} 

458: 

459: \subsection{The Logic}

460: 

461: In this section, we introduce a simple probabilistic temporal logic.

462: The purpose of the logic is to express properties that we wish to

463: check the stochastic automaton against.  The logic we define allows us

464: to check a range of such properties.

465: 

466: Recall that the region tree contains nondeterminism, and so we resolve

467: this using the notion of {\em adversaries} (see for

468: example~\cite{Baier-Kwiatkowska-1998}).  An adversary of a stochastic

469: automaton can be thought of as a scheduler, which resolves any

470: nondeterministic choices which the stochastic automaton must make.  An

471: adversary may vary it's behaviour according to the previous behaviour

472: of the automaton, or it may prescribe that for all non-deterministic

473: choices a particular branch is always preferred.

474: See~\cite{D'Argenio-1999} for examples of adversaries.

475: 

476: We assume that when we wish to model check a property against an

477: automaton, we are also given an adversary to resolve the

478: nondeterminism within the automaton. (Without this adversary,

479: enumerative analysis would not be possible; the provision of an

480: adversary is a prerequisite of model checking.)  We can now, for

481: example, answer such questions as ``Given a stochastic automaton and

482: an adversary, is the probability of a {\em send} event occurring

483: within 5 time units greater than 0.8?''.

484: 

485: The syntax of our logic is

486: 

487: \[

488: \psi ::=   \mathsf{tt} \mid \mathsf{ap} \mid \lnot \psi \mid \psi_1 \land

489: \psi_2 \mid [\phi_1  \until_{\!\!\sim c}\, \phi_2] \simeq p

490: \]

491: \[

492: \phi ::= \mathsf{tt} \mid \mathsf{ap} \mid \lnot \phi \mid \phi_1 \land \phi_2

493: \]

494: 

495: where $[\phi_1 \until_{\!\!\sim c}\, \phi_2] \simeq p$ is a {\em path

496: formula}.  The path formulae can only be used at the top level ---

497: they cannot be nested.  This is because the model checking algorithm

498: we give can only evaluate path formulae from the initial state and is

499: a necessary restriction of the current approach.

500: Further: $c \in {\nat}$ (natural numbers), {\sf ap} is an atomic

501: proposition, {\sf p} $\in [0,1]$ is a probability value and $\simeq, \sim

502: \in\{<,>,\leq,\geq\}$. 

503: 

504: We can define a number of derived operators.  For example, other

505: propositional operators are defined in the usual way:-

506: 

507: \[

508: \begin{array}{rcl}

509: \mathsf{ff} & \equiv & \lnot \mathsf{tt} \\

510: \phi_1 \lor \phi_2 & \equiv & \lnot (\phi_1 \land \phi_2) \\

511: \phi_1 \Rightarrow \phi_2 & \equiv & \lnot \phi_1 \lor \phi_2

512: \end{array}

513: \]

514: and we can define a number of abbreviations of a number of temporal

515: operators. 

516: \[

517: \begin{array}{rcl}

518: [\Diamond_{\sim c}\phi] \simeq p & \equiv & [\mathsf{tt} \!\!\until_{\!\!\sim

519: c}\;\phi] \simeq p \\ 

520: \hspace{1pt}[\always_{\sim c} \phi] \simeq p & \equiv & [\lnot

521: \Diamond_{\sim c}\lnot \phi] \simeq p  \\

522: \hspace{1pt}[\always \phi] \simeq p & \equiv & [\always_{\geq 0} \phi]

523: \simeq p \\% 

524: \hspace{1pt} [\Diamond \phi] \simeq p & \equiv & [\Diamond_{\sim 0}

525: \phi] \simeq p \\

526: \hspace{1pt} \forall [\phi_1 \!\!\until_{\!\!\sim c} \phi_2] & \equiv &

527: [\phi_1 \!\!\until_{\!\!\sim c} \phi_2] = 1 \\

528: \hspace{1pt} \exists [\phi_1 \!\!\until_{\!\!\sim c} \phi_2] & \equiv &

529: [\phi_1 \!\!\until_{\!\!\sim c} \phi_2] > 0 \\

530: \hspace{1pt}\forall\always \phi  & \equiv & \forall[\always \phi] \\% 

531: \hspace{1pt}\exists\always \phi  & \equiv & \exists[\always \phi] \\% 

532: \hspace{1pt}\forall\Diamond \phi  & \equiv & \forall[\Diamond \phi] \\% 

533: \hspace{1pt}\exists\Diamond \phi  & \equiv & \exists[\Diamond \phi] \\% 

534: \end{array}

535: \]

536: 

537: where $\forall$ and $\exists$ are the branching time temporal logic

538: operators, {\em for all} and {\em exist}~\cite{Emerson-1990}.

539: See~\cite{Baier-Katoen-Hermanns-1999} for similar definitions. 

540: 

541: With this syntax, an example of a valid formula that we can check

542: would be $[\mathsf{tt}\!\!\until_{\!\!< 10}\, \mathsf{send}] > 0.8$ which

543: says that the probability of reaching a {\sf send} event within 10

544: time units is greater than 0.8.

545: 

546: \subsection{Model Checking}

547: 

548: It should be clear that since we do not allow temporal formulae to be

549: nested we can use the following recipe in order to model check a

550: formula $\psi$ of our logic against a stochastic automaton $A$.

551: 

552: \begin{itemize}

553: \item[1.] For each until subformula (i.e. of the form $[\phi_1 \!\!

554: \until_{\sim c} \phi_2] \simeq p$) in $\psi$ perform an individual

555: model check to ascertain whether 

556: \[

557: A \models [\phi_1 \!\!\until_{\!\!\sim c}\phi_2]\simeq p

558: \]

559: \item[2.] Replace each until formula in $\psi$ by {\sf tt} if its

560: corresponding model check was successful, or {\sf ff} otherwise.

561: \item[3.] Replace each atomic proposition in $\psi$ by {\sf tt} or {\sf

562: ff} depending upon its value in the initial location of $A$.  

563: \item[4.] $\psi$ is a now ground term, i.e. truth values combined by a

564: propositional connective ($\lnot$ and $\land$).  Thus, it can simply

565: be evaluated to yield a truth value.  The automaton is a model of

566: $\psi$ if this evaluation yields {\sf tt}, and is not otherwise.  

567: \end{itemize}

568: 

569: This recipe employs standard techniques apart from the individual

570: checking that $A \models [\phi_1 \!\!\until_{\!\!\sim c}\phi_2]\simeq

571: p$ and this is what our two algorithms address.

572: 

573: 

574: \section{The Region-tree Algorithm}

575: \label{sec:alg-one}

576: 

577: In this section we introduce the first algorithm.

578: 

579: In model checking, we take a temporal logic predicate and seek to

580: establish whether it is true for our particular specification.  For

581: example, we might try to establish whether the above stochastic

582: automaton has the following property: Is the probability that a packet

583: will be successfully sent within ten time units greater than

584: eighty percent? In order to do this, we need to  define a means by

585: which we can check the stochastic 

586: automaton against this logic.  To achieve this the temporal logic and

587: the specification must have the same semantic model.

588: In~\cite{D'Argenio-Katoen-Brinksma-1998}, stochastic automata are

589: given a semantics in terms of {\em probabilistic transition systems},

590: and so the temporal logic is given a semantics in terms of

591: probabilistic transition systems as well, see

592: Appendix~\ref{sec:stoch-semantics}.

593: 

594: \subsection{Region Trees} \label{sec:region_trees}

595: 

596: For practical purposes, however, we cannot construct the probabilistic

597: transition system, since it is an infinite structure, (both in

598: branching and depth.)  We instead

599: construct a {\em region tree} from the specification.  This is

600: finitely branching, but may be infinite in depth.  Thus, a particular

601: region tree represents an unfolding of the stochastic automaton to a

602: certain depth.  In fact, we use the

603: temporal logic formula to construct a probabilistic region tree, which

604: is  used to verify the temporal logic formula.  More precisely, the

605: region tree is expanded until sufficient probability has been

606: accumulated to ascertain the truth or falsity of the formula (this

607: will become more clear shortly.)  In this section,

608: we describe how to construct  region trees from

609: stochastic automata.

610: 

611: 

612: %  we will then be in a position to describe the

613: % logic in Section~\ref{sec:logic}.

614:  

615:  

616:  We begin with the definition of a valuation, which we use to record

617:  the values of all the clocks in a particular state at a particular

618:  moment in time.  The unique clock $a \in {\cal C}$, which we add to

619:  the set of clocks, is used  to facilitate the model checking.  It

620:  keeps track of the total time elapsed in the execution of the

621:  stochastic automaton, but plays no part in the behaviour of the automaton.

622: 

623: \begin{Definition}

624:   A {\em valuation} is a function $v:{\cal C}\bigcup\{a\} \rightarrow

625:   {\cal R} \bigcup \{\perp\}$ such that $v(x) = \bot$ or $v(x)

626:   \leq x_{max}$, where 

627:   $x_{max}$ is the maximum 

628:   value to which clock $x$ can be set.    If $d \in {\cal R}_{\geq 0}$,

629:   $v-d$ is defined by $\forall 

630:   x \in {\cal C}\bigcup\{a\}. (v-d)(x) \defeq v(x)-d$.  

631: The function $\min(v)$ returns the value of the smallest defined

632: clock.    $\hfill\Box$

633: \end{Definition}

634:  

635: Since we assume that clocks are only used in the states in which they

636: are set, there is no need to remember their value once the state has

637: been exited.  Only the clock $a$ maintains its value; the rest are set

638: to $\bot$.  At the initialisation of a stochastic automaton, clock $a$

639: is set to some natural number, (we will show later how we choose this;

640: it depends on the formula we are interested in) and all other clocks

641: are undefined.  We define this initial valuation as ${\mathbf O}_n$,

642: if ${\mathbf O}(a) = n$.

643: 

644: We also need a notion of equivalence between the valuations, which

645: will enable us to construct the  regions within the

646: probabilistic region tree.  The issue here is the following.  Although

647: the size of the tree will be potentially infinite, at each node we

648: wish to have {\em finite} branching.  We achieve this because, although

649: there are an infinite number of valuations possible for any particular

650: state, there are a finite number of valuation equivalence classes.

651: This gives us the finite branching.  

652: 

653: \begin{Definition}

654: Two clock valuations  $v$ and $v'$ are {\em equivalent}  (denoted $v

655: \cong v'$) provided the following conditions hold:

656: 

657: \begin{itemize}

658: \item For each clock  $x \in {\cal C}\bigcup\{a\}$, either both $v(x)$

659:   and $v'(x)$ 

660:   are   defined, or $v(x) = \undef$ and $v'(x) = \undef$.   

661: \item For every (defined) pair of clocks $x,y \in {\cal

662:     C}\bigcup\{a\}.v(x) < v(y) \iff 

663:   v'(x) < v'(y)$.   

664: \end{itemize}  

665: 

666: The same clocks are defined in each valuation, and the order of the

667: values of the defined clocks is all that is important.    $\hfill\Box$

668: \end{Definition}

669: 

670: 

671: The reason that the order of the values of the defined clocks is all

672: that is important in the definition of a valuation equivalence class

673: is that the actions are triggered by the first clock to expire.

674: Therefore we only need to know whether one clock is greater than or

675: less than another.   Also note that there is a probability of zero

676: that different clocks are set to the same value.  This is because all

677: distributions are assumed to be continuous.   

678: 

679: % \includegraphics{region-tree.pic}

680: 

681: \begin{figure*}[t]

682: \begin{center}

683:   \ \psfig{figure=region-tree.pic,height=5in,width=5in}

684: \end{center}

685: \caption{The region tree}

686: \label{fig:region-tree}

687: \end{figure*}

688: 

689: 

690: We are now in a position to describe how a region tree is constructed

691: from a stochastic automaton. 

692: Intuitively, we build the region tree by ``unfolding'' the stochastic

693: automaton.  At each newly reached state, we calculate all possible

694: valuations (up to $\simeq$) and the probabilities of each one, then

695: from each of these 

696: (state,valuation) pairs we calculate the possible new states and

697: repeat.

698: 

699: Suppose we wish to construct the region tree for the

700: stochastic automaton in Figure~\ref{fig:stoch-automaton}.

701: 

702: 

703: 

704: 

705: The resulting region tree (up to a particular level of unfolding) is

706: given in Figure~\ref{fig:region-tree}.  The first node is labelled

707: with the location $s_0$, where the SA starts, the valuation ${\mathsf

708: 0}_1$, (i.e.  $(1,\perp,\perp)$) since clocks $x$ and $y$ have not yet

709: been set, and clock $a$ is set to value one.  Clock $a$ is set

710: according to the time value on the formula in which we are interested;

711: we will give the example formula in Section~\ref{sec:prt}.  The clocks

712: $x$ and $y$ are then set, giving a potential $3! = 6$ different

713: equivalence classes.  However, these can be reduced to two by

714: observing that clock $a$ will be fixed on 1 and $x_{max} = y_{max} =

715: 1$ and the probability of either $x$ or $y$ being set to exactly 1 is

716: zero\footnote{This coincidence of $a$, $x_{max}$ and $y_{max}$ is

717: assumed in order to simplify our presentation; the next iteration

718: illustrates the general case.}.  Using the convention that we

719: subscript the clock variables by the iteration number, in order to

720: distinguish different settings of the same clock, the two possible

721: equivalence classes are therefore $v_0(y) < v_0(x) < v_0(a)$ and

722: $v_0(x) < v_0(y) < v_0(a)$, where $v_0(a) = 1$ in both cases.  For

723: convenience, we will write $x_0$ for $v_0(x)$, $y_0$ for $v_0(y)$

724: and $a_0$ for $v_0(a)$.

725: 

726: If clock $x$ is set to less than clock $y$, the automaton will allow

727: time to pass in location $s_0$, and each clock will count down, until

728: clock $x$ reaches zero.  Then, either action {\em tryagain} or action

729: {\em conc} will fire (the choice is nondeterministic), and the

730: automaton will enter location $s_0$ or $s_1$ respectively.  The time

731: at which this occurs will obviously vary according to the initial

732: value of the clock $x$.  The possible locations entered are depicted

733: by regions 3 and 4 in the region tree in Figure~\ref{fig:region-tree},

734: where clocks $x$ and $y$ (since they are irrelevant in these regions)

735: are not recorded.  The initial value of clock $a$ when moving from

736: region 1 to either region 3 or region 4 will be $1 - x_0$ (we will

737: denote this value as $a_1$).  Thus,

738: it will be in the range $(0,1)$.

739: 

740: If clock $y$ is set to less than clock $x$ (represented by region 2),

741:  then the action {\em fail} fires, 

742: causing the automaton to enter location $s_2$, and this is depicted

743: by region 5 in the region tree.  Again, all we can say about the value

744: of clock $a$ at this stage is that it lies in the range $(0,1)$.

745: 

746: 

747: From region 3 there are two possibilities.  Either clock $z$ is set to

748: less than $a_1$, (region 6), or it is set to greater than $a_1$

749: (region 7).  From region 6 the action {\em send} will occur before the

750: clock $a$ expires, moving the automaton to location $s_0$ and the

751: region tree to region 14. From region 7 the clock $a$ will expire

752: before the action {\em send} occurs.  The region tree moves to region

753: 15, and the automaton remains in state $s_1$.

754: 

755: From region 4 (location $s_0$) both clocks $x$ and $y$ are reset according to 

756: their probability density functions, to values $x_1$ and

757: $y_1$. Since we cannot now be 

758: sure about the value of clock $a$, we have $3!=6$

759: equivalence classes, and these are represented by regions 8 to 13 when

760: we unfold the SA another 

761: level.  

762: 

763: 

764: In regions 8 and 9 $a_1$ is less than the (new) initial values of

765: clocks $x$ and $y$: these regions represent the case where clock $a$

766: expires before either of $x_1$ and $y_1$.  When we consider a

767: particular temporal logic formula this will represent the case where

768: time has run out, and so the region tree moves to either region 16 (if

769: $y$ expired 

770: first) or  region 17 (if clock $x$ expired first).

771: 

772: 

773: Regions 10 and 11 represent the valuation equivalence classes where

774: $x_1$ is less than both $a_1$ and $y_1$, and so from these

775: clock $x$ will expire first, either action {\em tryagain} or {\em

776: conc} will be performed, and the stochastic automaton will enter

777: either location $s_0$ or $s_1$ (regions 18---21).

778: 

779: 

780:  Region 12 and represent the valuation equivalence classes where

781: $y_1$ is less than both $a_1$ and  $x_1$, so clock $y$ will expire

782: first, action {\em fail} 

783: will fire, and the automaton will enter location $s_2$ (region

784: 22---23).

785: 

786: The region tree can be expanded further if necessary.  There is no

787: need to continue to expand regions 5, 15, 16, 17, 22 and 23, because in

788: all of these either the clock $a$ has expired or the stochastic

789: automata has reached location $s_2$, which is a deadlocked state, and

790: there is no further 

791: information to be gained.  In Figure~\ref{fig:region-tree}, further 

792: regions are derived from region 14 in the same way as above; these are

793: needed when we build the probabilistic region tree in the next

794: section.  

795: 

796: \subsection{Probabilistic Region Trees} \label{sec:prt}

797: 

798: Given a stochastic automaton, adversary and formula $\psi =  [\phi_1\!\!

799: \until_{\!\!\sim c}\, \phi_2]\simeq {\tt p}$ the model

800: checking algorithm consists of a number of iterations which are

801: repeated until the formula is found to be either true or false. 

802: 

803: An iteration unfolds the region tree by expanding each leaf node.  At

804: each iteration stage there are two steps.  The first step resolves

805: the nondeterministic choices in the newly expanded region tree using

806: the given adversary.  The second step then calculates the

807: probabilities on each node in the newly expanded part of the tree.

808: 

809: % 

810: %  and  each new node is labelled as {\em

811: %   passed}, {\em failed} or {\em 

812: %   undecided} according to whether the new node is at the end of a pa 

813: % 

814: % Nodes that have failed will never be further expanded.

815: % 

816: % 

817: 

818: 

819: 

820: \begin{figure*}[t]

821: \begin{center}

822:    \ \psfig{figure=prob-region-tree2.pic,height=5in,width=5in}

823:  \end{center}

824:  \caption{The probabilistic region tree}

825: \label{fig:prob-region-tree}

826:  \end{figure*}

827: 

828: %  

829: %  The probabilistic region tree is labelled with probabilities as it is

830: %  constructed.

831: % 

832: % 

833:  

834:  The region tree (Figure~\ref{fig:region-tree}) represents an unfolding of the

835:  stochastic automaton without the nondeterministic choices being resolved.

836:  The probabilistic region tree (Figure~\ref{fig:prob-region-tree}) records the

837:  resolution of the nondeterministic choices and the probabilities at

838:  the final nodes represent the chances of taking the particular

839:  sequence of actions that end in that node.  

840:  

841: 

842: At each iteration, we update the information we have on the

843: probability of a path satisfying the formula.  To do this, we define three

844: new propositions, and each node of the probabilistic region tree is

845: labelled with {\sf p}, {\sf f} or {\sf u}: {\sf p}, 

846: if it has {\it passed} (it is the end of a path which models the

847: bounded until formula $\psi$);

848: {\sf f}, if it has {\it failed} (it is the end of a path which cannot

849: model $\psi$), or {\sf u}, if it is {\it undecided}.  We also have two

850: global variables, $\Sigma {\sf p}$ and $\Sigma {\sf f}$, which keep

851: running totals of the probabilities of the {\it pass} and {\it fail}

852: paths.

853: 

854: 

855: The basic idea of the model checking algorithm is that we check the values of

856: $\Sigma {\sf p}$ and $\Sigma {\sf f}$ at each stage, and if we cannot

857: deduce from these the truth or falsity of the formula we are checking,

858: we look more closely at the undecided nodes.  That is,  we extend the

859: undecided paths by each possible 

860: subsequent 

861: action, label these new nodes {\sf p}, {\sf f} or {\sf u}, and

862: calculate their probabilities.  We then add these probabilities to

863: $\Sigma {\sf p}$ and $\Sigma {\sf f}$ and repeat. 

864: 

865: We will begin by demonstrating the technique for an example. The full

866: algorithm appears as appendix~\ref{sec:first-algorithm}.

867: Consider the example stochastic automaton

868: (Figure~\ref{fig:stoch-automaton}).

869: 

870: 

871: Let us consider the formula 

872: \[

873: \psi = [(\phi_0\lor \phi_1) \!\!\until_{\!\!<1}\; \phi_2] \geq 0.9

874: \]

875:  where $\phi_0$ (resp. $\phi_1$, $\phi_2$) is the proposition that we

876: are in state $s_0$ (resp. $s_1$, $s_2$).  The question\footnote{In fact, the

877: algorithm can easily be adapted to handle questions such as ``what is

878: the probability (to within some $\epsilon$) of a formula such as $[\phi_0\!\!

879: \until_{\!\!<1}\; \phi_2]$ being true?''.}  we are therefore asking is: is the

880: probability of reaching location $s_2$ (failing) within one time unit

881: greater than $0.9$?

882: 

883: Note that a steady state analysis will tell us only that the automaton

884: will fail (reach state $s_2$) eventually, but here we want to obtain

885: information about the transient behaviour of the automaton.

886:  The nondeterministic choice that has to

887: be made is between location $s_1$ and $s_2$.

888: We will consider  the benevolent adversary, i.e. the one that always

889: chooses location $s_1$.  

890:  

891: Consider region 1 first (Figure~\ref{fig:region-tree}).  It has two

892: possible outgoing transitions, 

893: and the choice between them is made nondeterministically.  So we must

894: refer to the adversary, which chooses location $s_1$, that is, region

895: 3.   Region 4 is not generated.  We note that the value of clock $a$ 

896: is

897: greater than zero (so time has not run out), and 

898: that proposition $p_0 \lor p_1$ is true (so the temporal logic formula is

899: able to be satisfied), so this region is labelled with {\sf u} (undecided). 

900: 

901: In region 5 proposition $p_2$ is true, and clock $a$ is still greater

902: than zero, so this region is labelled as passed {\sf p}, and region 5

903: becomes a terminal node.

904: 

905: 

906: In region 6 $a_1$ is greater than the (new) initial value of

907: clock $z$, and therefore  the {\em send}

908: action will fire before the clock $a$ expires. The region is therefore

909: labelled {\sf u}.   

910: 

911: In region 7 $a_1$ is less than the (new) initial value of

912: clock $z$, and therefore time will run out before the {\em send}

913: action has a chance to fire. The region is therefore labelled {\sf f}.  

914: 

915: 

916: From region 6 the {\em send} action moves the automaton to location

917: $s_0$ (region 14), and from here there are 6 possibilities for the

918: setting of the clocks.  

919: 

920: Regions 24 and 25 represent the valuation equivalence classes where

921: $a_1$ is less than $x_1$ and $y_1$.  Since clock $a$ will

922: expire before either clock $x$ or clock $y$,  we know that these paths

923: will not reach location $s_2$ in less than one time unit, so regions

924: 30 and 31 will be labelled {\sf f}.  The remainder of the tree is

925: generated in a similar manner.  

926: 

927: Figure~\ref{fig:prob-region-tree} represents two unfoldings.  In

928: order to determine whether the formula is true we also have to

929: calculate the probabilities on the nodes.  If the sum of the {\em

930:   pass} and the sum of the {\em fail} nodes is sufficient to tell us

931: whether the formula is true then we can stop here, otherwise  we

932: unfold the tree another level.   

933: 

934: % \subsubsection{Adding probabilities}

935: 

936: % The final step in the calculation is to determine the probabilities on

937: % each node, and we show how to do this now.

938: 

939: % 

940: % Although it seems strange that we distinguish nondeterministic regions

941: % (such as 7 and 8 or 10 and 11) which lead to the identical

942: % regions in the probabilistic region graph, it is necessary when we

943: % come to add probabilistic information to the graph.  We wish to

944: % include as much probabilistic information as possible, and so we need

945: % to make use of all the information we have.  In particular, the order

946: % of all the clocks and the position of clock $a$ within that order is

947: % important.  

948: % 

949: 

950: To determine the probabilities on the arcs, we need to use probability

951: density functions $\sf{P}\!_x$, $\sf{P}\!_y$ and $\sf{P}\!_z$ of the

952: functions $F_x$, $F_y$ and $F_z$, which we find by differentiating

953: $F_x$, $F_y$ and $F_z$ between

954: their upper and lower bounds and setting to zero everywhere else.

955: 

956: \[

957: \mathsf{P}_x(t) = \begin{drop} 2 - 2t, \mathrm{if~~} t \in [0,1] \\

958:                         0,       \mathrm{otherwise}

959:            \end{drop} 

960: \]

961: \[

962: \mathsf{P}_y(t) = \begin{drop} 2t,\mathrm{if~~} t \in [0,1] \\

963:                         0,       \mathrm{otherwise}

964:            \end{drop} \\

965: \]

966: \[

967: \mathsf{P}_z(t) = \begin{drop} 1,\mathrm{if~~} t \in [0,1] \\

968:                         0,       \mathrm{otherwise}

969:            \end{drop} \\

970: \]

971: Evaluating the function $F_x$ at a point $a$ gives the probability

972: that clock $x$ is set to a value less than $a$, and if $a > b$, then

973: $F_x(a)-F_x(b)$ gives the probability that clock $x$ is set to a value

974: between $a$ and $b$, provided $a$ and $b$ are constants.  The same

975: calculation using the corresponding probability density function (pdf)

976: would

977: be $\int^a_b {\sf P}\!_x(x)dx$, which at first sight appears more

978: complicated.  The advantage is that these functions can be used to

979: calculate the probability that clock $x$ is set to a value less than

980: $y$, where $y$ is a random variable set according to the distribution

981: function 

982: $F_y$.  If, for example, we wished to calculate the probability of the

983: equivalence class in region 1 ($v_0(x) < v_0(y) < v_0(a)$, where

984: $v_0(a) = 1$) we would evaluate

985: $\int^y_0{\mathsf P}_x(x)dx$, to give us a function that returns the

986: probability that $v_0(x)$ is between 0 and $y$, multiply this by the

987: pdf 

988: ${\mathsf P}_y(y)$, and integrate between zero and 

989: one:

990: 

991: \[\displaystyle

992: \int^1_0\int^y_0 {\mathsf P}_x(x)dx {\mathsf P}_y(y)dy

993: \]

994: which gives us the probability that $x$ will be less than $y$, where

995: $x$ and $y$ are random variables conforming to the distribution

996: functions $F_x$ and $F_y$.

997: 

998: We will now evaluate the probabilities of some of the arcs in the

999: example.  In the following, we will continue to subscript the clock

1000: variables by the iteration number, in order to distinguish different

1001: settings of the same clock.

1002: 

1003: In our example, to determine the probability on  arc $(0,2)$, where

1004: the value to which clock $y$ is initially set (which we will refer to

1005: as $y_0$) is less than the value to which clock $x$ was initially

1006: set ($x_0$), ($y_0 < x_0$)  we perform the double integration

1007: \[

1008: \displaystyle \int_{0}^{1} \int_{0}^{x_0} 2y_0 dy_0 \,(2-2x_0) dx_0  

1009: \]

1010: which evaluates to $\frac{1}{6}$. 

1011: 

1012: 

1013:  Arc $(0,1)$  must have the value $1-\frac{1}{6} = \frac{5}{6}$, since

1014:  it is the only other possibility, and

1015: can be calculated as 

1016: \[

1017: \displaystyle \int_{0}^{1} \int_{x_0}^{1} 2y_0 dy_0 \,(2-2x_0) dx_0  

1018: \]

1019: 

1020: These two arcs represent the setting of the clocks, and are therefore

1021: instantaneous. 

1022: 

1023: From Region 2 the only  region which can be reached is the leaf node

1024: region 5, and therefore the arc $(2,5)$ has probability 1.

1025: 

1026: Calculating probabilities on the paths through region 3 is more

1027: complicated.  Consider arc $(3,6)$ first.  In fact, we must calculate

1028: the probability of the path $(0,1,3,6)$ in its entirety rather than

1029: determine separately the conditional probability of arc $(3,6)$.  We

1030: do this as follows.

1031: 

1032: The clock setting information we know is: the first time the clocks

1033: $x$ and $y$ are set, the initial value of $x$ is less than the initial

1034: value of $y$ ($x_0<y_0$); and when $z_1$ is set, the sum of $x_0$ and

1035: $z_1$ is less  than the initial value of clock $a$

1036: ($x_0 + z_1 < 1$).    These constraints are captured as the

1037: combination of the integrals

1038: $\int_{x_0}^1 {\sf P}_y(y_0) dy_0$

1039: (to ensure that $x_0<y_0<1$),

1040: $\int_{0}^{1-z_1} {\sf P}_x(x_0) dx_0$

1041: (to ensure that $x_0+z_1<1$), and

1042: $\int_{0}^1 {\sf P}_z(z_1) dz_1$

1043: (since all constraints have been captured in the first two integrals.)

1044: 

1045: The combination is given as the first integral in Table~\ref{table:integrals} 

1046: and  equals $\frac{3}{5}$.

1047: 

1048: 

1049: \begin{table*}

1050: \begin{center}

1051: $

1052: \displaystyle

1053: \int_0^1 

1054:         \int_{0}^{1-z_1}  

1055:                         \int_{x_0}^1  {\sf P}_y(y_0) dy_0     

1056:         {\sf P}_x(x_0)dx_0            

1057: {\sf P}_z(z_1)dz_1

1058: $

1059: \\

1060: \vspace{1cm}

1061: $

1062: \displaystyle

1063: \int_0^1 

1064:         \int_{1-z_1}^{1}  

1065:                         \int_{x_0}^1  {\sf P}_y(y_0) dy_0     

1066:         {\sf P}_x(x_0)dx_0            

1067: {\sf P}_z(z_1)dz_1

1068: $

1069: \end{center}

1070: \caption{The integrals} \label{table:integrals}

1071: \end{table*}

1072: 

1073: 

1074: The path $(0,1,3,7)$ differs only in the fact that $a_1$ ($=1-x_0$) is

1075: less 

1076: than $z_1$, and can be calculated as the second integral in

1077: Table~\ref{table:integrals} which equals $\frac{7}{30}$.  

1078: The only difference is that ${\sf P}_x(x_0)$ is integrated between $1-z_1$

1079: and $1$. 

1080: 

1081: 

1082: At this stage in the algorithm, $\Sigma{\sf p} = \frac{1}{6}$

1083: and $\Sigma{\sf f} = \frac{7}{30}$.  Since  $\Sigma{\sf f} > 1-0.9$ we

1084: can deduce that the formula is false, and in

1085: this case, there is no need to unfold further the node labelled

1086: ${\mathsf u}$.  

1087: 

1088: The accuracy with which we know the values of  $\Sigma{\sf p}$ and

1089: $\Sigma{\sf u}$ will increase as the

1090: probabilistic region tree is extended, and in some cases it may need

1091: to be extended to infinity for perfect accuracy.  However, we can

1092: achieve accuracy to within an arbitrary tolerance $\epsilon$ with a

1093: finite probabilistic region tree.

1094: 

1095:  The major drawback of this algorithm is its complexity: with every

1096: new unfolding of the probabilistic region tree not only does the

1097: number of nodes to be considered increase, but also the number of

1098: integrations required to determine the probability on a single node

1099: increases exponentially.  It therefore becomes intractable after a few

1100: iterations.  This is the issue we try to tackle with the second

1101: algorithm.  Rather than integrate the probability density functions,

1102: we discretise the ranges of the functions and work with the resulting

1103: approximations.

1104: 

1105: \section{The Matrix algorithm}  \label{sec:alg-two}

1106: 

1107: In this section we present an overview of the second algorithm.  The

1108: second algorithm takes a stochastic automaton {\em SA}, together

1109: with a bounded until temporal logic formula TL, a time step parameter

1110: $\delta$ and an adversary {\em pick}.  For convenience we will present

1111: only the case where TL is of the form $[\phi_0\!\! \until_{\!\!\leq

1112: c}\, \phi_1]>p$.  Minor modifications to the algorithm would allow any

1113: of $\geq p$, $\leq p$ or $< p$.  We use the atomic propositions

1114: $\phi_0$ and $\phi_1$ as part of the formula because anything more

1115: complex can be reduced to these by standard model checking techniques.

1116: Using $\leq c$ guarantees that the algorithm will terminate, although

1117: we discuss the $\geq c$ case in Section~\ref{sec:greater-than}.

1118: 

1119: A single iteration of the algorithm will return one of

1120: three results: ${\sf true}$, ${\sf false}$ or ${\sf undecided}$.  If

1121: it returns ${\sf true}$, then the automaton models the formula.  If it

1122: returns ${\sf false}$, then the automaton does not model the formula.

1123: If it returns ${\sf undecided}$, then the algorithm was unable to

1124: determine whether the automaton models the formula.  In this case, the

1125: algorithm can be re-applied with a smaller value for the timestep

1126: $\delta$.  The question of convergence to the correct answer as

1127: $\delta$ tends to zero is discussed in

1128: section~\ref{sec:proof}.  For the remainder of this section we

1129: assume $\delta$ to be fixed.   

1130: 

1131: A stochastic automaton has a finite number of clocks each with a

1132: probability distribution function (pdf).  For each state, the set of

1133: clocks has an (arbitrary) order, and the algorithm makes use of this

1134: ordering\footnote{However, the choice of ordering is arbitrary and

1135: does not carry any meaning.  Any ordering will be sufficient.}. We

1136: assume that each clock has non-zero lower and upper bounds on the

1137: values to which it can be set. The first of these is a new constraint

1138: and was not required for the first algorithm. This has been done so

1139: that $\delta$ can be initially chosen to be less than the minimum of

1140: all these lower bounds.

1141: 

1142: The algorithm works by creating a snapshot of the automaton at each

1143: time point $n\delta$ ($n \in {\nat}$)\footnote{We will speak of the

1144: time instants generated by $n\delta$ ($n \in \nat$) as time points.}

1145: and extracting some global information about the probability of the

1146: formula $[\phi_0\!\! \until_{\!\!\leq c}\, \phi_1]$ being satisfied at

1147: this point.\footnote{We also require that $\exists n . n\delta = c$,

1148: which ensures that one of the snapshots will be at exactly time $c$.}

1149: To build the next snapshot, the algorithm picks out at each time point

1150: $n\delta$ the transitions that the automaton is capable of during the

1151: next interval of length $\delta$.  Because $\delta$ is less than the

1152: minimum of all the clock lower bounds, a maximum of one transition per

1153: path can occur in each interval.  Recording all possible states of the

1154: automaton at each time point is therefore enough to record all the

1155: possible transitions.

1156: 

1157: The algorithm stops when either enough information has been gathered

1158: to determine the truth or falsity of the formula, or enough time has

1159: passed so that $n\delta > c$, and allowing time to pass further will

1160: make no difference to the information we already have.  In this case

1161: the result {\sf undecided} is returned.  

1162: 

1163: \subsection{Data structures}

1164: 

1165: The principal data structures used by the algorithm are 

1166: matrices.  For each state $s$ in the stochastic automaton we derive a

1167: matrix for a given time $t$ (which is a rational number and calculated

1168: as $n\delta$), denoted

1169: $matrix(s,t)$, which is a record of the probabilities of the various

1170: combinations of clock values in state $s$ at time $t$.

1171: 

1172: Each matrix $matrix(s,t)$ will have $\#\kappa(s)$ dimensions.  Each dimension is

1173: associated with a particular clock, and the ordering of the dimensions

1174: corresponds to the ordering of the clocks.  The dimension associated

1175: with a clock $c$ will have $\lceil\frac{c_{max}}{\delta}\rceil$ entries,

1176: where $c_{max}$ is the largest value to which the clock $c$ can be set,

1177: and $\lceil \frac{c_{max}}{\delta} \rceil$ is the smallest integer

1178: greater than or equal to $\frac{c_{max}}{\delta}$. For a clock $c_i$, we

1179: will abbreviate $\lceil \frac{c_{i_{max}}}{\delta} \rceil$ by $N_i$.

1180: 

1181: The valuation function $v$ gives the value of a particular clock:

1182: $v(c_i)$ is the value of clock $c_i$.  

1183: 

1184: Each entry in the matrix $matrix(s,t)$ is the probability that at time

1185: point 

1186: $t$, the automaton is in state $s$, and each clock is within a

1187: particular time range. 

1188: Thus, the value $matrix(s,t)[k_1 \ldots k_n]$ is the

1189: probability that at time point $t$, the automaton is in state $s$,  and

1190:  $v(c_i) \in (\delta(k_i - 1),\delta k_i]$ for each clock $c_i$. 

1191: 

1192: A further data structure we shall need is $live(t)$, which  is the set

1193: of states ``live'' at time $t$ (i.e.\ their 

1194: matrices at time $t$ contain at least one non-zero entry, and the formula

1195: is still undecided).  In order to

1196: get an accurate picture of the automaton at time $t+\delta$, we must take

1197: into account all states live at time point $t$.

1198: 

1199: A $snapshot$ of the automaton at time $t$ is the set of all

1200: matrices $matrix(s,t)$ where $s$ is in $live(t)$.  

1201: 

1202: Let $pr(c_i \in (\delta(k_i-1), \delta k_i])$ be the probability that

1203: clock $c_i$ is initially set to a value in the range $(\delta(k_i-1),

1204: \delta k_i]$.  Before the algorithm proper begins, we calculate all

1205: these values from the clock probability distribution functions, which

1206: are entered into the algorithm as part of the stochastic automaton.

1207: 

1208: \subsection{Variables}

1209: 

1210: The algorithm also uses a number of auxiliary variables.  

1211: 

1212: $prob(s,t)$ is  the probability of entering state $s$ 

1213: during the time range  $(\delta(k-1), \delta k]$ (where $t=\delta

1214: k$) and is defined

1215: for 

1216: states $s$ 

1217: live at time  $\delta(k-1)$, and $s'$ live at time $\delta k$.  

1218: 

1219: $new\_states(s,t)$ is the set of states which can be reached from a

1220: state $s$ during a time range $(\delta(k-1), \delta k]$. 

1221: 

1222: $total\_pass$ is a probability value.  It is incremented at each

1223: iteration.  The iterations of the algorithm correspond to the 

1224: time points, and $total\_pass$ records the probability of the

1225: automaton having passed the formula at that time.  $total\_fail$ is

1226: also a probability value; it records the probability of the automaton

1227: having failed the formula as the algorithm progresses.

1228: 

1229: $error$  is an  upper bound on the possible errors of

1230: $total\_pass$ and $total\_fail$.  After an iteration, we know that the

1231: actual probability of the automaton having passed the formula is in

1232: the range $[total\_pass,total\_pass+error]$, and similarly for

1233: $total\_fail$.  

1234: 

1235: \subsection{Overview}

1236: 

1237: The second  algorithm is given in detail in

1238: Appendix~\ref{sec:second-algorithm}.   We begin here with a pseudocode

1239: description.   

1240: 

1241: \begin{tabbing}

1242: ...\=...\=...\=check \= formula against $s_0$ and $t=0$.\=...\=   \kill

1243: build $matrix(s_0,0)$ \\

1244: check formula against $s_0$ and $t=0$  \>\>\>\>\> $\rightarrow$ {\sf pass} \\

1245:                       \>\>\>\>\> $\rightarrow$ {\sf fail} \\

1246: \>\>\>\> $\downarrow$ {\sf undecided} \\

1247: repeat \\

1248: \> $t := t + \delta$ \\

1249: \> forall locations $s$ in $live(t-\delta)$ \\

1250: \>\> build $matrix(s,t)$ \>\>\>{\em (record possible new locations)} \\

1251: \>\>\>\>\> {\em (increment probability of entering new locations)} \\

1252: \>\>\>\>\> {\em (increment $error$)} \\

1253: \>\> update $live(t)$ \\

1254: \> forall locations $s'$ in $live(t)$ \\

1255: \>\> check formula against location: \\

1256:  \>\>\> if {\sf pass} then add probability to $total\_pass$ \\

1257: \>\>\>  if {\sf fail} then add probability to $total\_fail$ \\

1258: \>\>\>  if {\sf undecided} then update $matrix(s',t)$ \\

1259: until \>\>\> (formula has passed, or \\

1260: \>\>\> formula has failed, or \\

1261: \>\>\> $t$ has reached the limit set by the formula) \\

1262: set all locations {\sf undecided} at last iteration to false \\

1263: if $total\_pass > formula probability$ then output {\sf pass}\\

1264: elseif $total\_fail > 1- formula probability$ then output {\sf fail}\\

1265: else  output {\sf undecided} \\

1266: \end{tabbing}

1267: 

1268: 

1269: We now present the formula for initially calculating matrices, then

1270: describe the algorithm in overview, outlining the 

1271: procedures involved. 

1272: 

1273:  If there are $n$ clocks in state $s$, then $matrix(s,t)$ is

1274: calculated using the probability distribution functions of the clocks

1275: in state $s$ as follows:

1276: 

1277: \begin{tabbing}

1278: ....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=

1279: \kill

1280: \> $\forall 1 \leq k_1 \leq N_1$ \\

1281: \>\>\> $\vdots$ \\

1282: \> $\forall 1 \leq k_n \leq N_n \bullet matrix(s,t)[k_1\ldots k_n] :=

1283: {\displaystyle \prod_{l=1}^{n}} pr(v(c_{l}) \in (\delta(k_l-1),\delta

1284: k_l])$ \\ 

1285: \end{tabbing}

1286: 

1287: 

1288: The algorithm begins  by calculating $matrix(s_0,0)$,

1289: where 

1290: $s_0$ is the initial state of the stochastic automaton.  

1291: 

1292: 

1293: 

1294: $live(0)$ will either be $\{s_0\}$ or the empty set, according

1295: to whether the formula TL is made true or false by state $s_0$, or

1296: whether we cannot yet decide.  This is determined as follows.  If

1297: state $s_0$ models proposition $\phi_1$, then the formula TL is

1298: immediately true and $live(0)$ is the empty set.  Otherwise, if $s_0$

1299: models $\phi_0$ we cannot yet decide, and so $live(0)$ contains

1300: $s_0$. If the state models neither proposition then the

1301: formula TL is immediately false, and $live(0)$ is the empty set.

1302: \vspace{12pt}

1303: 

1304: If the initial step does not determine whether the formula is

1305: true or false, we perform a number of iterations.  Each iteration

1306: builds the snapshot at time point $t+\delta$, based upon the snapshot

1307: at time point 

1308: $t$.   The sequence of snapshots build progressively more information

1309: as to whether the stochastic automaton has passed or failed the

1310: formula.  

1311: 

1312: In the case of a bounded until formula with a $\leq c$

1313: subscript\footnote{i.e. $[\phi_0\!\! \until_{\!\!\leq {c}}\, \phi_1] > p$. See

1314: Section~\ref{sec:greater-than} for a discussion of how $>\! c$ time bounds

1315: are handled.}, the number

1316: of iterations is finite (i.e.\ the algorithm always 

1317: terminates) because the iterations terminate either when sufficient

1318: information has 

1319: been extracted to determine whether the formula passes or fails, or

1320: after the $\frac{c}{\delta}$th iteration, since the formula cannot

1321: become true after time $c$.

1322: 

1323: If the information at time $t$ is not enough to determine the truth

1324: or falsity of the formula, we build the snapshot for time point $t+\delta$.

1325: We now describe an individual iteration.  

1326: 

1327: An iteration consists of two sections.  In the first, we consider  all

1328: of the states which are currently 

1329: undecided.  These are all the states in $live(t)$.  For each state we

1330: create the matrices at

1331: time $t+\delta$, update $live(t+\delta)$ and calculate

1332: $prob(s',t+\delta)$ for states $s'$ which can be reached in the

1333: interval $(t,t+\delta]$.  In the second, we look at all states which

1334: can be reached in the interval $(t,t+\delta]$, and  consider them with

1335: respect to the temporal logic formula.  We then either update the global

1336: probabilities, if the states cause the formula to pass or fail,

1337: otherwise we update the respective matrices.

1338: 

1339: Note that in this algorithm a matrix is  updated at most twice.

1340: Once within procedure $new\_time\_matrix$(refer to

1341: Appendix~\ref{sec:second-algorithm}), if the state was live at

1342: the previous time, and once within the procedure $new\_state\_matrix$,

1343: if the state is reachable via a transition in the previous interval.  

1344: 

1345: \subsubsection{Creating and updating matrices}

1346: 

1347: 

1348: We begin with some necessary notation.  Let us assume  $\delta$ is a

1349: fixed rational number greater than zero.

1350: 

1351: 

1352: \begin{Definition}

1353: If $c_1,\ldots,c_n$ are the clocks on state $s$, a {\it 

1354:   valuation}\footnote{We alter the definition of valuation slightly

1355:   here for the second algorithm.} is

1356:   the vector of results of the valuation function $v(c_i)$ from clocks 

1357:   to ${\cal R}$ which gives 

1358: the values of each of the $n$ clocks.  

1359: 

1360: Two valuations $v$ and $ v'$ are ($\delta -$) equivalent if 

1361: \[

1362: \forall c_i.\exists k_l \in \nat. v(c_i) \in (\delta(k_l -1),k_l] \land v'(c_i)

1363: \in (\delta(k_l -1),k_l]

1364: \]

1365: 

1366: A {\it valuation equivalence class} (or clock configuration) is  a

1367:  maximal set of equivalent  valuations.  $\hfill\Box$

1368: 

1369: \end{Definition}

1370: 

1371: If $\delta$ is understood, we can abbreviate this configuration as

1372: $(k_1,\ldots,k_n)$.   For a

1373: state $s$ and a time point $t$, the probability $\prod_{l=1}^{n} pr(v(c_{l})

1374: \in (\delta(k_l-1),\delta k_l])$ is an $(s,t)$-{\it clock configuration

1375:   probability} (or just a clock configuration probability when $s$

1376: and $t$ are understood).

1377: 

1378: % 

1379: %  We will call

1380: % $[k_1,\ldots,k_n]$ the $(s,t)$-clock configuration for clocks

1381: % $c_1,\ldots,c_n$ (or just the clock configuration when $s$ and $t$ are

1382: % understood), and the probability $\prod_{l=1}^{n} pr(c_{l} \in

1383: % [k_l-\delta,k_l))$ the $(s,t)$-clock configuration probability (or just

1384: % the clock configuration probability when $s$ and $t$ are understood.)  

1385: % 

1386: % 

1387: 

1388: \vspace{12pt}

1389: 

1390: 

1391: There are two different procedures for updating a matrix.  The first

1392: (encapsulated in the procedure $new\_time\_matrix$) corresponds to the

1393: situation within the stochastic automaton where time passes, but the

1394: state remains unchanged.  In this case we must shift the clock

1395: configuration probabilities in the previous matrix down by one index

1396: step (which corresponds to $\delta$ time passing) and add the result

1397: to the matrix we are updating.

1398: 

1399: We also at this stage determine the new states which can be reached

1400: from the current state during the $\delta$ time passing, and the

1401: probability of entering these states.  We do this by looking at all

1402: the clock configurations where at least one of the indices has the

1403: value one.  If the clocks are set within such a configuration then we

1404: know that at least one clock will expire during the ensuing $\delta$

1405: timestep.

1406: 

1407: If only one index in the configuration has the value one then only one

1408: clock can expire, and only one state can be entered from this clock

1409: configuration, and so that state is added to the set of states which

1410: can be entered from the current state at the current time.

1411: 

1412: If more than one index in the configuration has the value one, then

1413: we simply do not go any further into the automaton and the

1414: configuration probability is added to error. 

1415: 

1416: The second way to update a matrix corresponds to a transition from one

1417: state to another within the automaton.  It is described in the

1418: procedure $new\_state\_matrix$.  For each matrix entry we calculate

1419: the clock configuration probability, multiply it by the probability of

1420: moving into this state at this time, and add it to the matrix entry we

1421: are updating.

1422: 

1423: \subsubsection{Termination of an iteration}

1424: 

1425: When the iteration terminates, it will output one of three results:

1426: {\sf true}, {\sf false} or {\sf undecided}.  {\sf true} means that the

1427: automaton models the temporal formula, i.e.\ $SA \models

1428: [\phi_0\!\!  \until_{\!\!\leq c}\, \phi_1] > p$.  {\sf false} means that

1429: $SA \not\models [\phi_0 \!\!\until_{ \!\!\leq c}\, \phi_1] > p$, and

1430: {\sf undecided} means that the algorithm could not accumulate enough

1431: information to decide whether or not the automaton modelled the

1432: formula.

1433: 

1434: The algorithm makes the output decision based on the three global

1435: variables $total\_pass$, $total\_fail$ and $error$.

1436: 

1437: $total\_pass$ is a lower bound on the probability that the stochastic

1438: automaton models the formula, and $total\_fail$ is a lower bound

1439: on the probability that the stochastic automaton does not model the

1440: formula.  $error$ 

1441: is the largest amount by which $total\_fail$ or $total\_pass$ may be

1442: wrong.  In a sense, it records the size of the uncertainty introduced

1443: by the choice of $\delta$. 

1444: 

1445: If neither of these situations holds then the errors introduced by the

1446: algorithm are too large to determine an answer with this value of

1447: $\delta$.  In this case, we can rerun the algorithm

1448: with a smaller $\delta$, and in section~\ref{sec:proof} we show

1449: that the sum of the errors tends to zero as $\delta$ tends to zero.

1450: Note, however, that in the case where the probability that $SA$ models

1451: $[\phi_0\!\! \until_{\!\!\leq c}\, \phi_1]$ is exactly $p$, we cannot

1452: guarantee 

1453: that there will be a $\delta$ small enough to allow the algorithm to

1454: generate a {\sf true} or a {\sf false}.  This is the sort of

1455: limitation that has to be accepted when working with generalised

1456: distributions.  

1457: 

1458: 

1459: 

1460: \section{Example}  \label{sec:example}

1461: 

1462: The second algorithm requires slightly more stringent restrictions on

1463: the stochastic automaton than the first one, because the clock

1464: distribution functions must have positive lower bounds, (as opposed to

1465: the non-negative lower bounds required by the first). Therefore in

1466: order to illustrate the second algorithm, we will use the 

1467: automaton in Figure~\ref{fig:stoch-automaton}, but alter slightly each

1468: of the clock distribution functions, by shifting each of them half a

1469: time unit to become 

1470: \[

1471: \begin{array}{rcl}

1472: F_x(t)  & = & 2t-t^2, \mathrm{if~~} t\in(\frac{1}{2},\frac{3}{2}] \\

1473:         & = &      0, \mathrm{if~~}  t \leq \frac{1}{2} \\

1474:         & = &    1, \mathrm{otherwise} \\

1475: \end{array}

1476: \]

1477: \[

1478: \begin{array}{rcl}

1479: F_y(t) & = & t^2, \mathrm{if~~}  t\in(\frac{1}{2},\frac{3}{2}] \\

1480:         & = &      0, \mathrm{if~~}  t \leq \frac{1}{2} \\

1481:         & = &    1, \mathrm{otherwise} \\

1482: \end{array}

1483: \]

1484: and

1485: \[

1486: \begin{array}{rcl}

1487: F_z(t) & = & t, \mathrm{if~~}   t\in(\frac{1}{2},\frac{3}{2}] \\

1488:         & = &      0, \mathrm{if~~}  t \leq \frac{1}{2} \\

1489:         & = &    1, \mathrm{otherwise} \\

1490: \end{array}

1491: \]

1492: 

1493: In this section, we will consider the temporal formula $[(a_0 \lor

1494: a_1) \!\!\until_{\!\!\leq \frac{3}{2}} a_2] > \frac{1}{2}$, where $s_i

1495: \models a_i, i \in \{1,2,3\}$.  

1496: 

1497: 

1498: We now illustrate this algorithm by applying it to the

1499:   example\footnote{The type of situation where this algorithm would do

1500:   very badly is if one clock has a very small lower bound and all the

1501:   rest have a very high lower bound.  This is accentuated if the first

1502:   clock is hardly used.  It might even be that the state where the

1503:   first clock is used is unreachable or has a very low probability of

1504:   being reached.  Thus a criterion for the algorithm to work

1505:   efficiently is that all pdf lower bounds are ``similar''.}. We set

1506:    $\delta$ equal to $\frac{1}{2}$.

1507: 

1508: 

1509: Sections A, B and C below correspond to the sections A,B and C in the

1510: algorithm description in Appendix~\ref{sec:second-algorithm}.  Within

1511: section 

1512: C, line numbers correspond to the line numbers of the algorithm.

1513: 

1514: \subsubsection*{Section A} 

1515: 

1516: This section initialises all the variables to zero, and

1517:   calculates all 

1518: the probabilities of clocks falling in the ranges

1519:   $(0,\delta],(\delta,2\delta]$ etc.  from the probability

1520: distribution functions entered as part of the stochastic automaton. 

1521: 

1522: In our example, the probabilities that the clocks $x$, $y$ and $z$ are

1523: in the ranges $(0,\delta], (\delta,2\delta]$ or $(2\delta,3\delta]$

1524: are given by

1525: \[

1526: \begin{array}{rccc}

1527:                  &    x        &      y      &     z  \\

1528: (0,\delta]       &    0        &      0      &     0  \\

1529: (\delta,2\delta] & \frac{3}{4} & \frac{1}{4} & \frac{1}{2} \\[3pt]

1530: (2\delta,3\delta]& \frac{1}{4} & \frac{3}{4} & \frac{1}{2} \\

1531: \end{array}

1532: \]

1533: 

1534: These are easy to obtain from the clock probability distribution

1535: functions.  Indeed, the ease of determining these probabilities is the

1536: main benefit of this algorithm and contrasts with the intractable

1537: manner in which the integrals explode in  the first algorithm.  

1538: 

1539:   

1540: \subsubsection*{Section B}

1541: 

1542: The initial state $s_0$ does not model $a_1$, but it does model the

1543: proposition $a_0$, and so the procedure $init\_matrix$ is called.

1544: This returns  $matrix(s_0,0)$ which is as follows

1545: \[

1546: \begin{array}{c|cccc}

1547: y &   & & &\\

1548: 3 & 0 & \frac{3}{8} & \frac{1}{8} &  \\

1549: 2 & 0 & \frac{3}{8} & \frac{1}{8} &  \\

1550: 1 & 0 & 0 & 0 & \\

1551: \hline 

1552:   & 1 & 2 & 3 &  x

1553: \end{array}

1554: \]

1555: and is easily derivable from the probabilities above.  The procedure

1556: also sets $live(0)$ to $\{s_0\}$.   

1557: 

1558: If $N_x$ is the upper bound of $x$, and $N_y$ is the upper bound of

1559: $y$, there will be $\lceil N_x \times \frac{1}{\delta}\rceil$ entries

1560: on the $x$ axis, and $\lceil N_y \times \frac{1}{\delta}\rceil$

1561: entries on the $y$ axis, so in this case (where $N_x=\frac{3}{2}$,

1562: $N_y=\frac{3}{2}$ and $\delta = \frac{1}{2}$),  we get a $3\times 3$ matrix.

1563: 

1564: 

1565: This matrix tells us e.g.\ that when the clocks in the initial state

1566: are first set, the probability of clock $x$ being set within the range

1567: $(\delta,2\delta]$ 

1568: and clock $y$ being set within the range $(2\delta,3\delta]$ is $\frac{3}{8}$.

1569: That is, for the clock configuration

1570: $\trace{(\delta,2\delta],(2\delta,3\delta]}$, the clock

1571: configuration probability is $\frac{3}{8}$.  

1572: 

1573: \subsubsection*{Section C}

1574: 

1575: We now enter the iterative part of the algorithm, where each iteration

1576: corresponds to increasing the time by one time unit ($\delta$), and

1577: the snapshot 

1578: produced at the end of iteration $n$ corresponds to a view of the

1579: automaton at time $n\delta$.  The three global probability

1580: values\footnote{These are the probability values that are updated

1581:   throughout the algorithm: $total\_pass, total\_fail$ and

1582:   $error$.} are 

1583: all still zero (lines 1-1a), so $ct$ (current time) becomes $\delta$.

1584: Only the state $s_0$ is live at time zero, so $new\_time\_matrix$ is

1585: called (line 6) for $matrix(s_0,\delta)$.  This returns a number of

1586: parameters:  $matrix(s_0,\delta)$,

1587: $new\_states(s_1,\delta),prob$ and $error$. 

1588: 

1589: 

1590: 

1591: The procedure $new\_time\_matrix$ will return the  $matrix(s_0,\delta)$  as 

1592: 

1593: \[

1594: \begin{array}{c|cccc}

1595: y &   & & &\\

1596: 3 &  0 & 0 & 0 & \\

1597: 2 &  \frac{3}{8} & \frac{1}{8} & 0 & \\

1598: 1 &  \frac{3}{8} & \frac{1}{8} & 0 & \\

1599: \hline 

1600:   & 1 & 2 & 3 &  x

1601: \end{array}

1602: \]

1603: where each clock has advanced one time unit from $matrix(s_0,0)$.  So,

1604: at time $\delta$, the probability of clock $x$ being within the range

1605: $(0,\delta]$ and clock $y$ being within the range $(\delta,2\delta]$

1606: is $\frac{3}{8}$. 

1607: 

1608: The probability of staying in state $s_0$ for at least half a time

1609: unit 

1610: is 1; this follows from the fact that no clock can be set

1611: to less than $\delta$ ($\frac{1}{2}$  time unit).  Thus

1612: $prob(s_0,\delta) = 1$.   

1613: 

1614: None of the edge values (those with at least one clock in the range

1615: $(0,\delta]$) of the previous time matrix ($matrix(s_0,0)$) is non-zero (so

1616: there is no possibility of any clock reaching zero and causing a

1617: transition to fire). The second half of the procedure (lines 10-23,

1618: which would determine the new states reached from state $s_0$) is

1619: therefore not executed and the global probability values

1620: ($total\_pass, total\_fail$ and $error$) are all

1621: still zero. $new\_states(s_0,\delta)$ will be returned as $\{\}$,

1622: since no new states can be reached at time $\delta$.  

1623: 

1624: The next step (lines 7-11 of section C) is to calculate the live

1625: states at time $\delta$, and since $remain(s_0,\delta) = true$ (it is

1626: possible to remain in state $s_0$ at time $\delta$) we

1627: include $s_0$.  

1628: 

1629: 

1630: Since there are no states which can be reached from state $s_0$ in the

1631: time interval $(0,\delta]$, lines 12-22 of section C are not executed.

1632: 

1633: All of the global probability values are still zero, (i.e.\ we don't

1634: have enough information to decide the truth or falsity of the formula

1635: at this stage, lines 1-1a of Section C), and $2\delta \leq 2$ (we have

1636: more time in which to gain more information, lines 2-3 of Section C),

1637: so we begin a second iteration.  

1638: 

1639: On the second iteration of the while loop, $ct$ is set to

1640: $2\delta$. Only $s_0$ was live at the last iteration

1641: ($live(\delta)=\{s_0\}$), so at line 6 we call $new\_time\_matrix$ for

1642: $matrix(s_0,2\delta)$.  

1643: 

1644: This again returns a number of parameters,

1645: e.g.\ $matrix(s_0,2\delta)$ becomes

1646:  

1647: \[

1648: \begin{array}{c|cccc}

1649: y &   & & &\\

1650: 3 &  0 & 0 & 0 & \\

1651: 2 &  0 & 0 & 0 & \\

1652: 1 &  \frac{1}{8} & 0 & 0 & \\

1653: \hline 

1654:   & 1 & 2 & 3 &  x

1655: \end{array}

1656: \]

1657: where the entry $matrix(s_0,2\delta)(1,1)$ is taken from the clock

1658: configuration $(\delta,2\delta],(\delta,2\delta]$ in the previous time

1659: matrix $matrix(s_0,\delta)$ and thus the probability of staying in

1660: state $s_0$ in the interval $(\delta,2\delta]$ is $\frac{1}{8}$.

1661: However this

1662: is not the final version of $matrix(s_0,2\delta)$, because some of the

1663: clock configurations lead to transitions which lead back to state

1664: $s_0$.

1665: 

1666: All the other clock configurations ($(1,1)$, $(1,2)$ and $(2,1)$) in

1667: $matrix(s_0,\delta)$ lead to transitions.   Lines 10-22 of procedure

1668: $new\_time\_matrix$ 

1669: are executed 

1670: for each of these three configurations.  

1671: 

1672: For clock configuration $(1,1)$, clock $x$ is (arbitrarily) chosen to

1673: fire, and we assume that the adversary $pick$ chooses the action

1674: $conc$, leading to state $s_1$.  Line 13a of the procedure adds state

1675: $s_1$ to $new\_states(s_0,2\delta)$, and $prob(s_1,2\delta)$ becomes

1676: $\frac{3}{8}$ (line 14). Clock configuration $(1,1)$ is one where some

1677: error may be introduced into the algorithm result.  Choosing clock $x$

1678: and action $conc$ meant that we go to a state where the formula $TL$

1679: can still be true, but choosing the other clock may not lead to such a

1680: state.  We therefore allow for the possible error introduced here by

1681: adding the clock configuration probability to $error$, which becomes

1682: $\frac{3}{8}$.  Clock configurations $(1,2)$ and $(2,1)$ are dealt

1683: with similarly, but $error$ remains constant.  

1684: 

1685: Now, the $new\_time\_matrix$ procedure is finished, and lines 7-11 of

1686: Section C determine the value of $live(2\delta)$ which is

1687: $\{s_0,s_1,s_2\}$, because at time $2\delta$ the automaton may be in

1688: any state.

1689: 

1690: Lines 12-22 of Section C consider each new state that can be reached

1691: in time interval $(\delta,2\delta]$.  State $s_0$ still allows the

1692: temporal logic formula to be true, and so procedure

1693: $new\_state\_matrix$ is called (line 17).  However,

1694: $prob(s_0,2\delta)=0$,  and therefore

1695: $matrix(s_0,2\delta)$ is not altered. 

1696: 

1697: State $s_1$ still allows the  temporal logic formula to become true

1698: (line 13) and so procedure $new\_state\_matrix$ is called (line

1699: 17). The probability of entering state $s_1$ in this interval is

1700: $\frac{6}{8}$, so $matrix(s_1,2\delta)$ is

1701: 

1702: \[

1703: \begin{array}{c|cccc}

1704:  & 0 & \frac{3}{8}  & \frac{3}{8} & \\

1705: \hline 

1706:   & 1 & 2 & 3 &  z

1707: \end{array}

1708: \]

1709: 

1710: In state $s_2$ the formula is true, and so $prob(s_2,2\delta)$

1711: ($\frac{1}{8}$) is added to $total\_pass$ (line 14).

1712: 

1713: In the final iteration, the global probability values become:

1714: $total\_pass = \frac{1}{8}$, $total\_fail = \frac{3}{8}$ and $error =

1715: \frac{4}{8}$.  The iterations stopped because the value of time became

1716: too large --- not because the global probabilities contained enough

1717: information to make a decision.  This means that $total\_pass$

1718: ($\frac{1}{8}$) is a maximum possible probability value of the formula

1719: $[(a_0\lor a_1)\!\!  \until_{\!\!\leq \frac{3}{2}}\, a_1]$ (with any

1720: clock ordering) and $total\_pass - error$ ($-\frac{3}{8}$) is a

1721: minimum possible probability value.

1722:  

1723:  Thus, since we wish to determine whether the actual probability value

1724:  is greater than $\frac{1}{2}$, the algorithm will output {\sf fail}.

1725: 

1726:    

1727:  If we were interested in a similar formula with a probability value

1728:  in the range $[0,\frac{1}{8}]$, we could reduce the size of $\delta$,

1729:  and take snapshots (e.g.) every $\frac{1}{4}$ time unit.  This (for

1730:  the reasons outlined in Section~\ref{sec:proof}) will reduce

1731:  the size of the $error$ variable.  

1732: 

1733: \subsection{Unbounded until formulae} \label{sec:greater-than}

1734: 

1735: As just presented the second algorithm only handles until formulae of

1736: the form

1737: \[

1738: [\phi_1 \!\!\until_{\!\!\leq c}\,\phi_2]\simeq p

1739: \]

1740: however a combination of the second and first algorithms yields a

1741: method to verify unbounded until formulae, i.e. those  of the form 

1742: \[

1743: [\phi_1 \!\!\until_{\!\!> c}\,\phi_2]\simeq p

1744: \]

1745: 

1746: The basic idea is to observe that verification of a formula such as

1747: $\phi_1 \!\!\until_{\!\!> c}\,\phi_2$ can be split into a

1748: conjunction of separate verifications

1749: 

1750: \begin{itemize}

1751: 

1752: \item[(a)]  Check that $\phi_1$ holds at all times until $c$ time units

1753: have elapsed; and

1754: 

1755: \item[(b)] Check that there exists an $X>c$ such that $\phi_2$ holds at

1756: time $X$, and that for all times strictly greater than $c$ and less

1757: than $X$, $\phi_1$ holds.

1758: 

1759: \end{itemize}

1760: 

1761: Thus, we can model check formulae such as $[\phi_1 \!\!\until_{\!\!>

1762: c}\,\phi_2]\simeq p$ in the following way.

1763: 

1764: \begin{itemize}

1765: 

1766: \item[(i)] Run (the obvious slight adaption of) the second algorithm

1767: to check that (a) holds.  This will finish with a certain amount of

1768: probability mass in the variable {\em total\_fail} and no probability

1769: mass in {\em total\_pass}.  The reason for the latter is that pass

1770: states can only be revealed once time has passed beyond $c$.  In

1771: addition, $live(c)$ will indicate the locations that are still

1772: undecided, i.e. from which we must explore further.

1773: 

1774: \item[(ii)] Run the first algorithm using $live(c)$ as the starting

1775: locations and the initial timing regions determined from the remaining

1776: matrices (this can be done in a straightforward manner).  However,

1777: notice that running the first algorithm in this situation does not

1778: incur the problems of intractability that it does in the general case.

1779: Specifically, since the time bound on the until has been satisfied we

1780: ostensibly only have an untimed until verification.  Consequently

1781: probabilities can be assigned to nodes without requiring the global

1782: clock to be taken into account and thus, they can be evaluated

1783: ``locally''.  Hence, the exponential explosion in the number of

1784: integrals to be considered does not occur.

1785: 

1786: \end{itemize}

1787: 

1788: \section{Correctness and convergence}  

1789: \label{sec:proof}

1790: 

1791: For a single run with fixed $\delta$, we wish to prove two things:

1792: that the algorithm terminating with {\sf pass} implies that the

1793: automaton models the formula, and that the algorithm terminating with

1794: {\sf fail} implies that the automaton does not model the formula.

1795: 

1796: If the algorithm outputs {\sf pass} then the variable {\em

1797: total\_pass} must be greater than $p$ (where $p$ is taken from the

1798: temporal formula $[\phi_0 \!\!\until_{\!\!\leq c}\, \phi_1] > p$).

1799: The only place where {\em total\_pass} gets incremented is line 14 of

1800: section C (see full algorithm in

1801: Appendix~\ref{sec:second-algorithm}). If the current state $q$ models

1802: $\phi_1$ (and all previous states in the path model $\phi_0$) we add

1803: the probability of entering the state $q$ at the current time

1804: point. If the sum of these probabilities is greater than $p$ then the

1805: algorithm outputs {\sf pass}.

1806: 

1807: 

1808: We will consider the case when the algorithm outputs {\sf

1809: pass}. Consider the initial state.  Note that for any clock

1810: configuration, 

1811: the probability of all paths which commence with the clocks being set

1812: somewhere within this configuration is equal to the clock

1813: configuration probability.  Furthermore, for an arbitrary state $s$

1814: and time $c$ and configuration, the probability of all paths which go

1815: through this configuration at this time is the probability of the

1816: configuration multiplied by the probability of reaching that state at

1817: that time.

1818: 

1819: The probability of reaching state $s$ at time $c$ is the second

1820: parameter passed to the procedure {\it new\_state\_matrix}\footnote{In

1821: fact, it is greater than or equal to this sum, because some routes

1822: through the transition system may have passed or failed the formula

1823: already, and therefore would be considered no further by the

1824: algorithm.}.

1825: 

1826: If every valuation in a configuration corresponds to the same

1827: automaton transition, and this transition is the final one in a path

1828: which models the formula, then we add the clock configuration

1829: probability (multiplied by the probability of reaching that state at

1830: that time) to {\it total\_pass}.

1831: 

1832: 

1833: This is the only way in which the algorithm adds to the variable {\it

1834: total\_pass}.  Since the algorithm only outputs {\sf pass} if {\it

1835: total\_pass} is greater than the formula probability $p$, it is clear

1836: that the algorithm will only output {\sf pass} if the automaton models

1837: the formula.

1838: 

1839: If more than one clock in the configuration is in the range

1840: $(0,\delta]$ then more than one of the clocks will have reached time 0

1841: in the interval we are considering, and so the clock configuration

1842: probability is added to {\it error}  (line 12 of procedure {\it

1843: new\_time\_matrix}). 

1844: 

1845: A similar argument applies in the case where the algorithm outputs

1846: {\sf fail}.

1847: 

1848: Therefore the algorithm is sound in the sense that if we are given  a

1849: definitive answer, this answer is correct.  There remains, of course,

1850: the question of convergence to the correct answer, and the following

1851: theorem summarises the situation. 

1852: 

1853: \begin{Theorem} For every automaton $SA$ and propositions $\phi_0$ and

1854: $\phi_1$ it is the case that if $SA$ models $[\phi_0

1855: \!\!\until_{\!\!\leq c}\, \phi_1]$ with probability $p$, then for any

1856: error $e$ greater than zero, there is a timestep $\delta$ greater than

1857: zero such that for the formula $[\phi_0 \!\!\until_{\!\!\leq c}\,

1858: \phi_1]\!>\!  q$, the algorithm will only return {\sf undecided} if $q

1859: \in [p\!-\!e,p\!+\!e]$.

1860: 

1861: \end{Theorem}

1862: 

1863:  First note that $n$ independent single

1864: variable continuous probability distribution functions

1865: $f_1\ldots f_n$ can always be combined to give a single $n$ variable

1866: probability distribution function which is continuous in all

1867: dimensions:  $f(x_1\ldots x_n) = f_1(x_1) \times \cdots \times

1868: f_n(x_n)$.  

1869: 

1870: For convenience, consider a location with two outgoing transitions and

1871: two clocks $x$ and $y$ with distribution functions $f_x$ and $f_y$.

1872: Because $f_x$ and $f_y$ are both continuous, if we set $f(x,y) =

1873: f_x(x) \times f_y(y)$ we can (by the note above) say that

1874: \[

1875: \forall \epsilon > 0. \exists \delta > 0. f(x,x+\delta) -

1876: f(x,x-\delta) < \epsilon

1877: \]

1878: 

1879: We will show that for any desired size of error we can choose a

1880: suitably small timestep.

1881: 

1882: \begin{figure}

1883: \begin{center}

1884:   \ \psfig{figure=proof2.pic,height=1.9in,width=2in}

1885: 

1886: \caption{Upper bound on error with clocks $x$ and $y$.}

1887: \label{fig:proof.pic}

1888: \end{center}

1889: \end{figure}

1890: 

1891: Now, $\int_0^m f(x,x+\delta) - f(x,x-\delta) dx$ \footnote{ $m =

1892: {min\{x_{max},y_{max}\}}$, where $x_{max}$ is the 

1893: largest value to which  clock $x$ can be set.} (the probability of the clock

1894: valuation falling between the two 45 degree lines in

1895: Figure~\ref{fig:proof.pic}) is greater than the 

1896: sum of all contributions to the error variables (represented by the

1897: squares in the figure).  Since the number of locations in the stochastic

1898: automaton is finite (say $N_s$) and (for bounded until formulas with less

1899: than subscripts) the maximum number of visits to any location is finite

1900: (say $N_v$) for any desired error $e$ we must ensure that, for every

1901: location, for the multivariate function associated with that location, we

1902: choose $\epsilon$ such that $\epsilon < \frac{e}{N_s \times N_v}$.  If

1903: the timestep is set to the smallest $\delta$ necessary to ensure that

1904: every location provides errors less than $\frac{e}{N_s \times N_v}$, then

1905: total error provided by one location (over all time) will be less than

1906: $\frac{e}{N_s}$ and the total error provided by all locations will be

1907: less than $e$.   

1908: 

1909: 

1910: \section{Complexity measures}  \label{sec:complexity}

1911: 

1912: \subsection{Time complexity}

1913: 

1914: The time complexity of the algorithm discussed in

1915: Section~\ref{sec:alg-two} depends on a number of factors, namely

1916: $\delta$, $t$, $n_1$, $n_2$ and $\mid {\cal S} \mid$.  The explanation

1917: of these parameters is as follows:

1918: 

1919: \begin{itemize}

1920: \item $t$ is the value of time given in the time-bounded until

1921: formula: $[a \!\!\until_{\!\!\!\leq t} b] \sim p$;

1922: \item $\delta$ is the chosen timestep;

1923: \item $\mid {\cal S} \mid$ is the number of states in the automaton;

1924: \item  $n_1$ is the largest number of clocks in  a single state and

1925: \item $n_2$ is the largest (positive  finite) upper bound of all the

1926: clocks. 

1927: \end{itemize}

1928: 

1929: 

1930:  An upper bound on the number of matrices which need to be built in a

1931:  single iteration is $\mid {\cal S} \mid$, where ${\cal S}$ is the set

1932:  of all states in the automaton.  

1933: 

1934: 

1935: To calculate the time complexity we also need to calculate the size of

1936: the largest matrix.  Each matrix is multi-dimensional, and

1937: $\frac{n_2}{\delta}$ will be the maximum number of entries over all

1938: matrices and all dimensions.  For example, in the example in

1939: Section~\ref{sec:example} all the matrices had 2 dimensions and the

1940: maximum number of entries in any dimension was 3 since $\delta =

1941: \frac{1}{2}$ and $n_2 = \frac{3}{2}$.

1942: 

1943: An upper bound on the size of the largest matrix will therefore be

1944: the   number 

1945: of elements in the largest dimension, 

1946: raised to the power of the largest number of clocks on a single

1947: state.   

1948: 

1949: The time complexity is thus bounded by the time taken to update all

1950: the possible matrices in each iteration of the while loop in the

1951: algorithm, multiplied by the maximum number of iterations the

1952: algorithm will perform in the worst case.  This latter value is

1953: $\frac{t}{\delta}$, therefore the time complexity is  

1954: \[

1955: \frac{t}{\delta} \times

1956: (\frac{n_2}{\delta})^{n_1} \times \mid {\cal S} \mid

1957: \]

1958: 

1959: Although this is exponential, the exponent $n_1$ is something which

1960: should in general be fairly small ($\leq 3$) because we only allow

1961: clocks to be used from the state in which they are set.

1962: 

1963: 

1964:  In fact, the algorithm could be optimised to provide a

1965: better time complexity, by limiting the size of the matrices to

1966: $\min(\frac{t}{\delta},\frac{n_2}{\delta})$ since there is no need

1967: to consider the operation of the clock beyond the limit set by the

1968: time bound on the temporal formula.  The size of the largest matrix

1969: would 

1970: therefore be  less than

1971: $(\min(\frac{t}{\delta},\frac{n_2}{\delta}))^{n_1}$, 

1972: where $n_1$ is the largest number of clocks in  a single state.

1973: 

1974: An upper bound on the time complexity would therefore be

1975: \[

1976: \frac{t}{\delta} \times

1977: (min(\frac{t}{\delta},\frac{n_2}{\delta}))^{n_1} \times \mid {\cal S} \mid

1978: \]

1979: 

1980: 

1981: 

1982: The time complexity  also relies heavily on $\delta$, and the bigger the $\delta$ the

1983: lower the time complexity.  To see the relationship with $\delta$,

1984: note that  the upper bound can be rewritten as 

1985: 

1986: \[

1987: \left(\frac{1}{\delta}\right)^{n_1+1} \times t \times 

1988: (n_2)^{n_1} \times \mid {\cal S} \mid

1989: \]

1990: 

1991: \subsection{Space complexity}

1992: 

1993: An upper bound on the space complexity will be proportional to the

1994: product of the size of the biggest matrix and the largest number of

1995: matrices which need to be stored at one time.   The size of the

1996: largest matrix is less than

1997: $(\frac{n_2}{\delta})^{n_1}$, (from time

1998: complexity calculations) and the largest number of matrices which need

1999: to be stored at any one time is twice the number of states in the

2000: automaton, $2 \;\times \mid {\cal S} \mid$.  The upper bound on space

2001: complexity is therefore 

2002: \[

2003: 2 \times (\frac{n_2}{\delta})^{n_1} \times \mid

2004: {\cal S} \mid

2005: \]

2006: 

2007: 

2008: 

2009: \section{Conclusions and further work} \label{sec:conclusions}

2010: 

2011: In this paper we have presented two algorithms for model checking

2012: bounded  until formulae against stochastic automata.  Both of these

2013: algorithms allow systems to be described using continuous probability 

2014: distributions, and we believe that this represents an important

2015: advance.  

2016: 

2017:  The principal

2018: advantage of the first algorithm is its generality:  the clocks may be set

2019: according to any function, providing the corresponding probability

2020: density function is integrable.  The major drawback of the algorithm

2021: is its complexity:  with every new unfolding of the probabilistic

2022: region tree not only does the number of nodes to be considered

2023: increase, but also the number of integrations required to determine

2024: the probability on a single node increases exponentially.   

2025: 

2026: The principal advantage of the second algorithm is its efficiency: the

2027: discretisation of the probability functions means that the

2028: calculations required are considerably simpler.  A limitation in

2029: comparison to the first algorithm is that the probability distributions

2030: must have a finite lower bound.

2031: 

2032: In addition, an advantage of both the algorithms is that, since the

2033: ``complete'' model is at no point generated, the state space explosion

2034: (which typically hinders model checking) is contained.  In particular,

2035: all data structures apart from those which reflect undecided nodes

2036: (i.e. {\sf u} 

2037: labelled regions in the first algorithm and {\em live} locations in

2038: the second algorithm) can be deleted.   In this sense the algorithms

2039: yield a form of on-the-fly exploration -- only keeping information

2040: about the ``leaves'' of the exploration tree.  

2041: 

2042: 

2043:  

2044:   Further work on the second algorithm will include relaxing the

2045: restrictions imposed on the stochastic automata, particularly the

2046: ability to set and use clocks anywhere in the automaton.  Being able

2047: to do this would allow parallel composition.

2048: 

2049: 

2050: It would also be good to increase the expressiveness of the logic,

2051: allowing nested untils or ``greater than'' queries, and to extend the

2052: model checking algorithm itself to allow queries such as ``what is the

2053: probability of $[\phi_0 \!\!\until_{\!\!\leq c}\, \phi_1]$?'' and receive

2054: a probability value for an 

2055: answer.  

2056:   

2057:  

2058: {\bf Acknowledgements: }

2059: The research presented here is supported by the

2060: UK Engineering and Physical Sciences Research Council under grant number

2061: GR/L95878 (A Specification Architecture for the Validation of Real-time

2062: and Stochastic Quality of Service).

2063: Thanks are due to co-workers on this project for their input into this

2064: work: 

2065:  Gordon and Lynne Blair from Lancaster

2066: University. Also to Pedro D'Argenio, Joost-Pieter Katoen and Holger

2067: Hermanns.   In

2068: particular Pedro's observations on clock equivalences for stochastic

2069: automata have greatly influenced our approach.  

2070: 

2071: \bibliography{spa} 

2072: 

2073: \bibliographystyle{esub2acm.bst}

2074: %\bibliographystyle{alpha}

2075: 

2076: \setlength{\parskip}{1ex}

2077: \setlength{\parindent}{0ex}

2078: 

2079: \appendix

2080: 

2081: \section{Semantics} \label{sec:stoch-semantics}

2082: 

2083: 

2084: \subsection{Probabilistic Transition Systems}  \label{decoration} \label{pts}

2085: 

2086: 

2087: The definition of the semantics of stochastic automata is given in

2088: terms of probabilistic transition systems. The definition of

2089: probabilistic transition systems is reproduced

2090: from~\cite{D'Argenio-Katoen-Brinksma-1998}.

2091: 

2092: $\nat$ is the set of non-negative integers.  $\real$ is the set of

2093: real numbers, and $\real_{\geq0}$ the set of non-negative

2094: reals. For $n \in \nat$, let $\real^n$ denote the $n$th cartesian

2095: product of $\real$.  $\real^0 \defeq \{\emptyset\}$. 

2096: 

2097: A {\it probability space} is a structure $(\Omega,{\cal F},P)$ where

2098: $\Omega$ is a {\it sample space}, ${\cal F}$ is a $\sigma${\it

2099:   -algebra} on $\Omega$ and $P$ is a {\it probability measure} on

2100: ${\cal F}$.  In this work,  as in~\cite{D'Argenio-Katoen-Brinksma-1998}, we

2101: consider only probability spaces isomorphic to some Borel space

2102: defined in a real hyperspace, whose coordinates come from independent

2103: random variables.  We denote by ${\cal R}(F_1,\ldots F_n)$ the

2104: probability space $(\real^n,{\cal B}(\real^n),P_n)$ where ${\cal

2105:   B}(\real^n)$ is the Borel algebra on $\real^n$ and $P_n$ is the

2106: probability measure obtained from $F_1 \ldots F_n$, a given family of

2107: distribution functions. See~\cite{Shiryayev-1984} for details.  

2108: 

2109: 

2110: Let ${\cal P} = (\Omega, {\cal F}, P)$ be a probability space.  Let

2111: ${\cal D}:\Omega \rightarrow \Omega'$ be a bijection.  We lift ${\cal

2112:   D}$ to subsets of $\Omega$: ${\cal D}(A) \defeq \{{\cal D}(a)\mid a

2113: \in A\}$ and define ${\cal F}' \defeq \{{\cal D}(A) \mid A \in {\cal

2114:   F}\}$.  Now, it is clear that ${\cal D}({\cal P}) \defeq

2115: (\Omega',{\cal F}',P \circ {\cal D}^{-1})$ is also a probability

2116: space. Since ${\cal D}({\cal P})$ is basically the same probability

2117: space as ${\cal P}$, we say that ${\cal D}$ is a {\it decoration} and

2118: we refer to ${\cal D}({\cal P})$ as {\it the decoration of ${\cal P}$

2119:   according to ${\cal D}$.} This is used when we come to give a

2120: semantics to stochastic automata.

2121: 

2122: 

2123: \begin{Definition}  Let $P(H)$ denote the set of probability spaces

2124: $(\Omega, {\cal F}, P)$   such that $\Omega \subseteq H$.  A {\it

2125:   probabilistic transition system}  is a structure ${\cal T} =

2126:   (\Sigma,\Sigma', \sigma_0,{\cal L},T,\longrightarrow)$ where 

2127: \begin{enumerate}

2128: \item $\Sigma$ and $\Sigma'$ are two disjoint

2129:  sets of {\it states}, with the {\it initial state} $\sigma_0 \in

2130:  \Sigma$.  States in $\Sigma$ are called {\it probabilistic states}

2131:  and states in $\Sigma'$ are called {\it non-deterministic} states. 

2132: \item ${\cal L}$ is a set of {\it labels}.  

2133: \item $T: \Sigma \rightarrow P(\Sigma')$ is the {\it probabilistic

2134:     transition relation}. 

2135: \item $\longrightarrow \subseteq \Sigma' \times  {\cal L} \times 

2136:   \Sigma$ is the {\it labelled (or non-deterministic) transition

2137:     relation}.  We use  $\sigma' \stackrel{l}{\longrightarrow} \sigma$

2138:   to denote $\trace{\sigma',l,\sigma} \in \longrightarrow$,

2139:   $\sigma' \not\stackrel{l}{\longrightarrow}$ for

2140:   $\lnot\exists\sigma.\sigma'\stackrel{l}{\longrightarrow}\sigma$ and

2141:   $\sigma' \longrightarrow \sigma$ for $ \exists l. \sigma'

2142:   \stackrel{l}{\longrightarrow} \sigma$.  $\hfill\Box$ 

2143: \end{enumerate}                        

2144: \end{Definition}

2145: 

2146: Since we are interested in timed systems, we set ${\cal L} = \mathbf{A}

2147: \times  \real_{\geq0}$, where \textbf{A} is a set of action names.  A

2148: timed action transition will be described as $a(d)$, which indicates

2149: that the action $a$ occurs exactly $d$ time units after the system has

2150: been idling.

2151: 

2152: \begin{Definition}{\upshape

2153:   A {\em valuation} is a function $v:{\cal C} \rightarrow

2154:   \real_{\geq0} \union \{\perp\}$ such that $v(x) \leq x_{max}$, where

2155:   $x_{max}$ is the maximum 

2156:   value to which clock $x$ can be set.  The set of all valuations is

2157:   ${\cal V}$.  If $d \in \real_{\geq0}$, $v-d$ is defined by $\forall

2158:   x \in {\cal C}. (v-d)(x) \defeq v(x)-d$.  We assume the set of

2159:   clocks is ordered so, if $C \subseteq {\cal C}$, we can write

2160:   $\stackrel{\rightarrow}{C}$ for the ordered form of $C$ and

2161:   $\stackrel{\rightarrow}{C}\!\!(i)$ for the $i$-th element.  Let $C

2162:   \subseteq {\cal C}$, $n = \#C$, and $\stackrel{\rightarrow}{D} \in

2163:   \real^n$.  We define

2164:   $v[\stackrel{\rightarrow}{C}\mapsleft\stackrel{\rightarrow}{D}]$ by

2165: \begin{eqnarray*}

2166: v[\stackrel{\rightarrow}{C}\mapsleft\stackrel{\rightarrow}{D}](x) 

2167: & \defeq & \left\{

2168:    \begin{array}{ll}

2169:    \stackrel{\rightarrow}{D}(i) & {\mathrm{ if~~}} x =

2170:    \stackrel{\rightarrow}{C}(i), {\mathrm{for~~ some~~}} i \in

2171:    \{1,\ldots,n\} \\

2172:    \perp & {\mathrm{otherwise}} \\

2173:    \end{array}

2174: \right.

2175: \end{eqnarray*} $\hfill\Box$

2176: }\end{Definition}

2177: This definition will be used when we explain how clock values change

2178: as states change.  It differs from the definition given

2179: in~\cite{D'Argenio-Katoen-Brinksma-1998} because there clocks not in

2180: the set ${\cal C}$ maintain their values through this operation.  This

2181: is because in~\cite{D'Argenio-Katoen-Brinksma-1998} clocks may be used

2182: to trigger actions in any state, not just the state in which they are

2183: set.  In this work, however, in order to simplify the model checking, we

2184: insist that clocks are only used in the states in which they are set,

2185: and therefore there is no need to remember their value once the state

2186: has been exited. 

2187: 

2188: 

2189:   The main obstacle now in constructing the

2190: probabilistic transition system semantics is in showing how the

2191: clock probability functions are used to construct the probability

2192: spaces.  We do this by defining a decoration function, discussed in

2193: Section~\ref{decoration}.  

2194: 

2195: Let $SA = ({\cal S},s_0,{\cal C},{\bf A},\blackright,\kappa,F)$ be

2196: a stochastic automaton. Let $s$ be a location in ${\cal S}$ and $n =

2197: \#\kappa(s)$.  Let $v$ be a valuation in ${\cal V}$. Let ${\cal V'} =

2198: \{v[\stackrel{\rightarrow}{\kappa(s)} \mapsleft

2199: \stackrel{\rightarrow}{D}] \mid \stackrel{\rightarrow}{D} \in

2200: \real^n\} \subseteq {\cal V}$.  We define the decoration function ${\cal

2201:   D}^s_v : \real^n 

2202: \rightarrow \{s\} \times  {\cal V'} \times  \{1\}$ by ${\cal

2203:   D}^s_v(\stackrel{\rightarrow}{D}) \defeq

2204: (s,v[\stackrel{\rightarrow}{\kappa(s)} \mapsleft

2205: \stackrel{\rightarrow}{D}],1)$.  Notice that ${\cal D}^s_v$ is a

2206: bijection.  In the next definition, we use the probability space ${\cal

2207:     R}(F_{x_1},\ldots,F_{x_n})$ decorated according to some ${\cal

2208:     D}^s_v$. 

2209: 

2210: \begin{Definition}

2211:   Let $SA = ({\cal S},s_0,{\cal C},{\bf A},\blackright,\kappa,F)$

2212:   be a stochastic automaton.  The actual behaviour of $SA$  is given

2213:   by the PTS $I(SA) \defeq (({\cal S} \times  

2214:   {\cal V} \times  \{0\}), ({\cal S} \times  {\cal V} \times  \{1\}),

2215:   (s_0,{\bf 0},0), \mathbf{A} \times  \real_{\geq 0}, T,

2216:   \longrightarrow)$, where in the initial valuation {\bf 0} clock

2217:   $a$ is set to some natural number (chosen according to the PRTL

2218:   function, see Section~\ref{sec:PRTL}), and each other clock is

2219:   undefined.  $T$ and $\longrightarrow$ are defined as follows:

2220: \[

2221: \begin{array}{rl}\frac{\stackrel{\longrightarrow}{\kappa(s)} =

2222:     \{x_1,\ldots,x_n\}}{T(s,v,0) = {\cal D}^s_v({\cal

2223:     R}(F_{x_1},\ldots,F_{x_n}))} & {\bf Prob} \end{array}

2224: \]

2225: \[

2226: \begin{array}{rl}\frac{\begin{array}{c}s

2227:     \!\stackrel{a,\{x\}}{\blackright}\!s' \land d \!\in  

2228:       \!\real_{\geq 0} \land (v - d)(x) \leq 0 \\ \forall d' \in

2229:       [0.d). \forall s'.s \stackrel{b,\{y\}}{\blackright}s'.(v - d')(y) >

2230:       0\end{array}}{(s,v,1) \stackrel{a(d)}{\longrightarrow}

2231:       (s',(v-d),0)} & {\bf Act} \end{array}

2232: \]                  $\hfill\Box$

2233: \end{Definition}

2234: 

2235: Within a stochastic automaton, two forms of uncertainty may arise.

2236: One is the probabilistic uncertainty associated with the

2237: clock-setting.  Although we 

2238: know which clocks are to be set, the choice of values for these clocks

2239: is probabilistic.  This is where the stochastic element of the

2240: model arises, and is defined by rule {\bf Prob}.    The other is the

2241: nondeterministic uncertainty that arises if two actions 

2242: are simultaneously able to be performed, and is defined using the rule

2243: {\bf Act}.  This nondeterminism is resolved using an

2244: adversary (Definition~\ref{def:adversary}).

2245: 

2246: 

2247: Definition of a PTS-path:

2248: 

2249: \begin{Definition}{\upshape

2250: A {\em PTS-path}  is a {\em finite} or {\em infinite} sequence of

2251: states  

2252: \[

2253: \trace{\sigma_0,\sigma'_0,\sigma_1,\sigma'_1,\ldots}

2254: \]

2255: where, $\sigma_0$ is the initial state, for each $\sigma'_i$, there

2256: exists a probability space $(S, {\cal F},P)$ such that $T(\sigma_i)

2257: =(S,{\cal F},P)$, $\sigma'_i \in S$ and $\sigma'_i \longrightarrow

2258: \sigma_{i+1}$.  }    $\hfill\Box$

2259: \end{Definition}

2260: 

2261: \begin{Definition}{\upshape

2262: An {\em SA-path} is a finite or infinite sequence

2263: \[

2264: \trace{(s_0, v_0), (s_0, v'_0), (s_1,v_1), (s_1,v'_1), \ldots,

2265:   (s_n,v_n), (s_n,v'_n),\ldots}

2266: \]

2267: such that 

2268: \begin{itemize}

2269: \item $v_0$ means no clocks are set. 

2270: \item $v'_i \in {\cal R}(F_{x_1},\ldots,F_{x_n})$ where

2271:   $T(s_i,v_i,0) = {\cal D}^s_v({\cal R}(F_{x_1},\ldots,F_{x_n}))$.

2272:   Each valuation $v'_i$ is a possible result of

2273:   the clock setting functions. 

2274: \item $(s_i,v'_i,1) \stackrel{a(d)}{\longrightarrow}

2275:   (s_{i+1},v_{i+1},0)$ for some $d$.    Timed action

2276:   transitions must be allowed by the SA.

2277: \item Finite paths end on a probabilistic state. 

2278: \end{itemize} $\hfill\Box$

2279: }\end{Definition}

2280: 

2281: An SA-path is like a run of the SA expanded with clock values.  

2282: 

2283: 

2284: \begin{Definition}{\upshape

2285: \label{def:adversary}

2286:   An {\em adversary} of an SA is a function mapping sequences of

2287:   states to states 

2288: \[

2289: adv:  <s_0,s_1,\ldots,s_n> \longrightarrow s_{n+1}

2290: \]

2291: such that $<s_0,s_1,\ldots,s_n,s_{n+1}>$ is a run of the SA. $\hfill\Box$

2292: }\end{Definition}

2293: Note that adversaries do not make any reference to time. 

2294: 

2295: With an adversary, an SA becomes deterministic.  The corresponding PTS

2296: contains no nondeterminism either.

2297: 

2298: 

2299:  If 

2300: \[

2301: \sigma = \trace{(s_0, {\bf 0}), (s_0, v'_0), (s_1,v_1), (s_1,v'_1), \ldots,

2302:   (s_k,v_k), (s_k,v'_k)}

2303: \]

2304:  is

2305:   a finite  SA-path, then  $\sigma[i] = s_i$ and $\sigma(x)$ is the state at

2306:   time $x$.  

2307: 

2308: ${\cal R}(F_{x_1},\ldots,F_{x_n})$  is the Borel space $(\real^n,

2309: {\cal B}(\real^n),P_n)$ where $P_n$ is the unique probability measure

2310: obtained from ${\cal R}(F_{x_1},\ldots,F_{x_n})$.

2311: 

2312: Now, for all $j<k$, set $A_j$ to be the maximal set of valuations

2313: equivalent to $v_j$ which lead to state $s_{j+1}$.  

2314: 

2315: % 

2316: % 

2317: %   \in {\cal B}(\real^n)$ (i.e. make sure

2318: % $A_j$ is a legitimate set from the Borel space.)

2319: % 

2320: 

2321: Let

2322: \[

2323: C(s_0,A_0,s_1,\ldots,s_{k-1},A_{k-1},s_k)

2324: \]

2325: denote the {\em cylinder set} which contains all paths starting at

2326: $s_0$ and going through all states $s_j (j\leq k)$ and valuation sets

2327: $A_j (j\leq k)$.  

2328: 

2329: 

2330: % as a cylinder set would work, except that not all the valuations in

2331: % $A_j$ necessarily lead to $s_{j+1}$.  So we impose an extra

2332: % restriction, that for every $A_j$ the same clock is the smallest in

2333: % each valuation  (this clock firing then takes the SA to state

2334: % $s_{j+1}$.)

2335: 

2336: The probability measure $Pr$ on ${\cal

2337: F}(Path(s_0))$\footnote{$Path(s_0)$ is all paths possible from $s_0$,

2338: and ${\cal F}(Path(s_0))$ is the smallest $\sigma-$algebra on $Path(s_0)$.}

2339: is identified by induction on $k$ by $Pr(C(s_0))=1$ and for $k\geq0$:

2340: \[

2341: Pr(C(s_0,A_0,\ldots,A_{k},s_{k+1}) =

2342: Pr(C(s_0,A_0,\ldots,A_{k-1},s_{k}))\cdot P(A_k)

2343: \]

2344: 

2345: where $P(A_k)$ is the probability of the set $A_k$, and is taken from

2346: the relevant Borel space.

2347: 

2348: % \footnote{Might use $P(A_k \inter [v])$ to

2349: % formalise this, because for some finite set of equivalence classes

2350: % $[v_q]$, $A_k = (A_k \inter [v_1]) \union (A_k \inter [v_2]) \cdots$

2351: % and each will go to a different state in the SA, and therefore give

2352: % rise to separate cylinder sets.}

2353: 

2354: % \begin{Definition}{\upshape

2355: %   An {\em aggregated SA-path} (or {\em aggSA-path} for short) is

2356: %   formed by replacing all the valuations in an SA-path with their

2357: %   corresponding equivalence classes.  If 

2358: % \[

2359: % \trace{(s_0, {\bf 0}), (s_0, v'_0), (s_1,v_1), (s_1,v'_1), \ldots,

2360: %   (s_n,v_n), (s_n,v'_n)}

2361: % \]

2362: %  is

2363: %   an SA-path, then  

2364: % \[

2365: % \trace{(s_0, [{\bf 0}]), (s_0, [v'_0]), (s_1,[v_1]), (s_1,[v'_1]),

2366: %   \ldots, (s_n,[v_n]), (s_n,[v'_n])}

2367: % \]

2368: %  is the aggSA-path. $\hfill\Box$

2369: % 

2370: % }\end{Definition}

2371: % 

2372: % Each clock-setting transition (that is, those  of the form

2373: % $(s_i,[v_i]) \blackright (s_i,[v'_i])$) in an aggSA-path has a probability,

2374: % which can be derived from 

2375: % the probability functions associated with the  clocks in the

2376: % definition of the Stochastic Automaton.   The clock-setting

2377: % transitions in the Stochastic Automaton therefore correspond to the

2378: % probabilistic transitions in the Probabilistic Transition System. 

2379: % 

2380: 

2381: \subsection{PRTL Semantics} 

2382: 

2383: In this section, we introduce the semantics for the temporal logic

2384: PRTL. 

2385: 

2386: To facilitate model checking, we use Probabilistic Transition Systems

2387: as a semantic model for the definition of PRTL.  But in order to do this we

2388: must resolve two problems.  The first is that PRTL is a {\em

2389:   real-time} logic --- it enables reference to specific instants in

2390: time --- and the abstract definition of

2391: PTSs~\cite{D'Argenio-Katoen-Brinksma-1998} does not contain reference

2392: to time.  This is easily solved --- we simply use the PTS generated by

2393: a Stochastic Automaton.  This contains much more detailed state

2394: information, in particular, the values of clocks.

2395: 

2396: The second problem is that the PTS contains nondeterministic

2397: information, and this nondeterminism must be resolved before we can

2398: use the PTS to assign a semantics to our logic.  We do this using 

2399:   adversaries.

2400: 

2401: %  \begin{figure} 

2402: % \begin{center}

2403: % \begin{picture}(200,100)

2404: %  

2405: %  %Stochastic automaton

2406: %  

2407: %  \put(40,40){\circle{40}}

2408: %  \put(140,40){\circle{40}}

2409: %  \put(60,40){\vector(1,0){60}}

2410: %  \qbezier(54,54)(80,80)(60,90)

2411: %  \qbezier(40,61)(40,100)(60,90)

2412: %  \put(40.2,60){\vector(0,-1){0}}

2413: %  \put(16,64){\vector(1,-1){10}}

2414: %  \put(35,50){$s_0$}

2415: %  \put(135,50){$s_1$}

2416: %  \put(30,37){$x$}

2417: %  \put(85,42){$\scriptstyle a,\{x\}$}

2418: %  \put(60,92){$\scriptstyle b,\{x\}$}

2419: %  \end{picture}

2420: %  \end{center}

2421: %  \caption{Stochastic Automaton 2} \label{fig:sa2} 

2422: %  \end{figure}

2423: %  

2424: 

2425: %  \subsection{Syntax}

2426: % 

2427: % Following~\cite{Baier-Kwiatkowska-1998} in the untimed case, we allow

2428: % quantification over adversaries: the formula $[\phi_1 \exists \!\!

2429: % \until_{\sim c}\, \phi_2] > p$ says that there is an adversary such

2430: % that the formula $\phi_1 \until_{\sim c}\, \phi_2$ holds with

2431: % probability greater than $p$, and $[\phi_1 \forall \!\! \until_{\sim

2432: %   c}\, \phi_2] > p$ states that for every adversary, the formula

2433: % $\phi_1 \until_{\sim c}\, \phi_2$ is true with probability greater

2434: % than $p$.

2435: % 

2436: % 

2437: 

2438: Recall the syntax of PRTL:

2439: 

2440: \[

2441: \begin{array}{c}

2442: \psi ::= \mathsf{tt} \mid \mathsf{ap} \mid \lnot \psi \mid \psi_1

2443: \land \psi_2 \mid [\phi_1 \!\! \until_{\sim c}\, \phi_2] \simeq p 

2444: \\

2445: \phi ::= \mathsf{tt} \mid \mathsf{ap} \mid \lnot \phi \mid \phi_1

2446: \land \phi_2

2447: \end{array}

2448: \]

2449: 

2450: where $c \in \nat$, $a$ is an atomic proposition,  $p \in [0,1]$ is a

2451: probability value and $\sim, \simeq \in\{<,>,\leq,\geq\}$.

2452: 

2453: The {\em path formulae} $\psi$ can only be used at the outermost level

2454: --- they cannot be nested.   This is because the model checking

2455: algorithms  only evaluate path formulae from the initial

2456: state.

2457: 

2458: 

2459: \begin{Definition}{\upshape

2460:   If $SA = ({\cal S},s_0,{\cal C},{\bf A},{\blackright},\kappa,F)$ is

2461:   a Stochastic Automaton and $PTS = (\Sigma,\Sigma', \sigma_0,{\cal

2462:     L},T,\longrightarrow)$ is the resulting Probabilistic Transition

2463:   System, then $\Sigma (= \Sigma') \subseteq {\cal S} \times  {\cal V}$, ${\cal

2464:     L} \subseteq A \times  \real_{\geq 0}$ and $\sigma_0 = (s_0,{\bf

2465:     0})$.  We must

2466:   also introduce a function $\xi$ which maps SA locations to the

2467:   logical propositions true in that location. $\hfill\Box$

2468: }\end{Definition}

2469: 

2470: We only need to use the probabilistic states to define the logic,

2471: since once a probabilistic state has been entered the behaviour of the

2472: automaton is completely determined until the first clock expires.

2473: 

2474: The simple formulae $\phi$ are defined in the conventional way for

2475: each probabilistic region $\sigma'$, but the until formulae $\psi$ are

2476: defined only for the initial region $\sigma_0$.  The model checking

2477: algorithm does not yet allow path formulae to be established for an

2478: arbitrary region.  

2479: 

2480: \begin{itemize}

2481: 

2482: \item[$\bullet$] $s \models \mathsf{tt}$

2483: 

2484: \item[$\bullet$] $s \models a$, provided $a \in

2485:   \xi(s)$

2486: 

2487: \item[$\bullet$] $s \models \phi_1 \land

2488:   \phi_2$, provided $s \models \phi_1$

2489:   and $s \models \phi_2$

2490: \item[$\bullet$] $s \models \lnot  \phi$,

2491:   provided $s \not\models \phi$

2492: 

2493: 

2494: \end{itemize}

2495: 

2496: \vspace{12pt}

2497: 

2498: If $\sigma$ is an SA-path, and $\psi$ a path formula then

2499: \begin{itemize}

2500: \item[$\bullet$] $\sigma \models [\phi_1 \!\! \until \phi_2]$ iff $\exists k\geq

2501: 0 . (\sigma[k] \models \phi_2 \land \forall 0 \leq i \leq k. \sigma[i]

2502: \models \psi_1)$

2503: \item[$\bullet$] $\sigma \models [\phi_1 \!\! \until_{\!\sim t} \phi_2]$ iff

2504: $\exists x\sim t . (\sigma(x) \models \phi_2 \land \forall y \in

2505: [0,x). \sigma(y) \models \psi_1)$

2506: \end{itemize}

2507: and

2508: \begin{itemize}

2509: \item[$\bullet$] $PTS \models [\phi_1 \!\! \until_{\!\sim t}

2510: \phi_2] \simeq p$ iff $Prob(s_0,\phi_1 \!\! \until_{\!\sim t} \phi_2)

2511: \simeq p$ where $Prob(s_0,\psi) \defeq Pr\{\rho \in Path(s_0) \mid

2512: \rho \models \psi \}$

2513: \end{itemize}

2514: 

2515: 

2516: %  Will need to show that, for $s_0$, $\{\sigma \in

2517: %  Path(s_0) \mid \sigma \models \psi \}$ is measurable.

2518: 

2519: 

2520: Therefore, the Probabilistic Transition System $PTS$ models the

2521: PRTL $[\phi_1 \!\! \until_{\!\sim t}

2522: \phi_2] \simeq p$ provided $Prob(s_0,\phi_1 \!\! \until_{\!\sim

2523: t} \phi_2) \simeq p$.

2524: 

2525: \section{First Algorithm}

2526: \label{sec:first-algorithm} 

2527: 

2528: Here, we give the definition of the first model checking algorithm for

2529: bounded until formulae.  We will consider a PRTL formula of the form

2530: $[\phi_1 \until_{< c}\, \phi_2] > p$.  ``less than $p$'' queries may be

2531: handled in a similar way.  

2532: 

2533: Assume an adversary {\em Adv}, and that each SA location is mapped to

2534: either $\phi_1$ or $\lnot \phi_1$ and to either $\phi_2$ or $\lnot

2535: \phi_2$.  Note that the algorithm can easily be extended to the more

2536: general case where locations contain set of atomic propositions.

2537: 

2538: Add the (new) clock $a$ to the set of all clocks. 

2539: 

2540: Construct the PRG node  $(s_0,{\bf 0}_c)$.    

2541: 

2542: Set $s = s_0$.  

2543: 

2544: If $s \not\models \phi_1$ then stop with no, else 

2545: 

2546: REPEAT

2547: \setlength{\parskip}{0ex}

2548: \setlength{\parindent}{2ex}

2549: 

2550: For each  possible valuation equivalence class $[v_i]$ from

2551: $\kappa(s)\bigcup \{a\}$, form the node  $(s,[v_i])$.

2552: 

2553: For each new node $(s,[v_i])$ choose a  subsequent  non-deterministic 

2554: node $(s_j,\bot)$ according to the adversary {\em Adv}. 

2555: 

2556: \setlength{\parindent}{4ex}

2557:    For each new

2558:     non-deterministic node $(s_j,\bot)$ 

2559: 

2560: \setlength{\parindent}{6ex}

2561:     label `{\sf p}' if $s_j \models \phi_2$ and $v(a) > 0$.   

2562: 

2563:     label `{\sf f}' if $s_j \not\models \phi_1$ or $s_j \not\models

2564:     \phi_2$ or $v(a) \leq 0$.

2565: 

2566:     label `{\sf u}' otherwise

2567: 

2568: \setlength{\parindent}{4ex}

2569: 

2570: 

2571: \setlength{\parindent}{2ex}

2572: 

2573: For each node labelled with either `{\sf p}' or `{\sf f}', calculate 

2574:   the probability of the corresponding path.

2575: 

2576: If $\Sigma_{\sf p} pr(s,[v]) > p$ then stop with yes.

2577: 

2578: If $\Sigma_{\sf f} pr(s,[v]) > 1-p$ then stop with no.

2579: 

2580: Otherwise, repeat for each node labelled `{\sf u}'.

2581: 

2582: 

2583: \section{Second algorithm}  \label{sec:second-algorithm}

2584: 

2585: In this section we present a detailed description of the algorithm.

2586: It is divided into Section A (which initialises variables), Section B

2587: (the initial part of the algorithm) and Section C (the iterative

2588: part).  Procedures used are described at the end.  

2589: 

2590: The lines of code are prefaced with numbers, and the comments are

2591: delimited with double stars.  

2592: 

2593: \begin{tabbing}

2594: ....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\= \kill

2595: \> \bc{ Section A}\ec\\

2596:  $ Model\_check(SA,Formula,\delta,pick)$    \\

2597: \> \bc{ note that the function $pick$ is the adversary, used in procedure $new\_time\_matrix$.}\ec\\

2598: \> \bc{ We are assuming a TL formula of the form $[a_0 \until_{\leq t} a_1] \geq p$.  }\ec\\

2599: \> \bc{ The $\geq p$ could easily be changed; the $\leq t$ is hardwired into the algorithm. }\ec\\

2600: \> \bc{ }\ec\\

2601: \> \bc{ We begin by initialising variables.}\ec\\

2602: \> \begin{com}{ $ct$: (integer)  current\_time}\end{com}\\

2603: \> $ct := 0 $    \\

2604: \> \bc{ $total\_pass$ and $total\_fail$ are reals in $[0,1]$.  }\ec\\

2605: \> \bc{  At any point in the algorithm, $total\_pass$ is the accumulated }\ec\\ 

2606: \> \bc{ probability of all the passed paths and $total\_fail$ is the accumulated }\ec\\

2607: \> \bc{  probability of all the failed paths. We initialise them both to zero.}\ec\\

2608: \> $ total\_pass := 0 $\\

2609: \> $ total\_fail := 0$\\

2610: \> \bc{ $error$ is a real in $[0,1]$.  It is the accumulated probability of all paths  }\ec\\

2611: \> \bc{ which, because of the discretisation of the algorithm, we cannot determine exactly.}\ec\\

2612: \> \bc{ This is where the revised version of the algorithm differs from the initial one.}\ec\\

2613: \> \bc{ It is  initialised to zero. }\ec\\

2614: \> \bc{ }\ec\\

2615: \> $ error := 0$ \\

2616: \> \bc{ $prob(s,t)$ is the probability of moving (from  anywhere) to location $s$ }\ec\\

2617: \> \bc{  at time $t$. (i.e. in interval $(t-\delta,t]$.)}\ec\\

2618: \> \bc{ For all combinations of locations and times, we initialise $prob$ }\ec\\

2619: \> \bc{ to zero. }\ec\\

2620: \> $\forall s \in S. \forall i \leq n$.\\

2621: \>\>  $prob(s,\delta i) := 0$ \\

2622: \> \bc{ $remain(s,t)$ is a boolean which is true if the probability of remaining }\ec\\

2623: \> \bc{ in location $s$ during time interval $(t-\delta,t]$ is non-zero, false otherwise.}\ec\\

2624: \> \bc{ They are all initialised to false.}\ec\\

2625: \> $\forall s \in S. \forall i \leq n$.\\

2626: \>\>  $remain(s,\delta i) := false$ \\

2627: \> \bc{ $live(t)$ is the set of locations ``active'' at the end of }\ec\\

2628: \> \bc{ interval $(t-\delta, t]$, which }\ec\\

2629: \> \bc{ we need for calculating the information for the next time interval. }\ec\\

2630: \> \bc{ For all time values, we initialise $live$ to the emptyset. }\ec\\

2631: \>  $\forall i \leq n$.\\

2632: \>\> $live(\delta i) := \emptyset$ \\

2633: \> \bc{ We initialise all values in all matrices to zero.}\ec\\

2634: \> \bc{ The are $n_s$ clocks in location $s$.}\ec\\

2635: \> $\forall s \in S.$ \\

2636: \>\> $\forall 0 \leq j \leq n.$ \\

2637: \>\>\> $\forall 1 \leq i_1 \leq N_1$ \\

2638: \>\>\>\>\> $\vdots$ \\

2639: \>\>\> $\forall 1 \leq i_{n_s} \leq N_{n_s}. matrix(s,\delta j)[i_1\ldots i_{n_s}] := 0$\\

2640: \\

2641: \> \bc{ call procedure for calculating probabilities of clocks falling in the ranges }\ec\\

2642: \> \bc{ $(0,\delta], (\delta,2\delta]$ etc.  This comes directly from the clock PDFs, }\ec\\

2643: \> \bc{ and is only calculated once.  It is needed for determining the clock}\ec\\

2644: \> \bc{probabilities.   }\ec\\

2645: \> \bc{$C$ is the set of all clocks and  $F$ is the set of clock probability functions}\ec\\

2646: \> \bc{ This procedure returns $pr$, which is needed in $new\_state\_matrix$ }\ec\\

2647: \> \bc{ and $init\_matrix$. }\ec\\

2648: \> $clock\_config\_probs(C,F,\delta,pr)$ \\

2649: \> \bc{ }\ec\\

2650: \\

2651: \> \bc{ Section B}\ec\\

2652: \> \bc{ Consider initial location of SA:  $s\_0$ }\ec\\

2653: \> \bc{  If $s\_0 \models a\_1$ then formula is trivially true.  }\ec\\

2654: \> if $s\_0 \models a_1$ then \\

2655: \>\> $ total\_pass := 1 $\\

2656: \> \bc{ If $s\_0 \models a\_0$ then formula is undecided and we   must   }\ec\\

2657: \> \bc{  unfold SA further.  }\ec\\

2658: \> elseif s\_0 $\models a_0$ then  \\

2659: \>\> \bc{ Build the initial matrix, i.e. $matrix(s\_0,0)$.  }\ec\\

2660: \>\> \bc{This will then contain the probabilities }\ec\\

2661: \>\> \bc{of all the different clock settings for location $s\_0$ at time zero.   }\ec\\

2662: \>\> $init\_matrix(matrix(s\_0,0))$  \\

2663: \>\> \bc{ The only location ``live'' at time zero will be $s\_0$.  }\ec\\

2664: \>\> $live(0) := \{s\_0\}$ \\

2665: \> \bc{ If $s\_0$ does not model $a\_0$ or $a\_1$ then formula is trivially false.  }\ec\\

2666: \> else \\

2667: \>\> $total\_fail := 1$ \\

2668: \> end if \\

2669: \\

2670: \> \bc{ Section C}\ec\\

2671: \> \bc{ Each iteration of the following loop unfolds the automaton by }\ec\\

2672: \> \bc{ one time step of $\delta$.  States which cause  the formula to  }\ec\\

2673: \> \bc{ pass/fail are pruned from the tree, and their probabilities added to }\ec\\

2674: \> \bc{ $total\_pass/total\_fail$, while the undecided states are recorded }\ec\\

2675: \> \bc{ for the next iteration.  }\ec\\ 

2676: \> \bc{  We continue while the values of $total\_pass$, $total\_fail$ and $error$ }\ec\\

2677: \> \bc{ are not enough to  determine whether the formula is true or false }\ec\\

2678: 1: \>\> repeat \\

2679: \>\> \bc{  Increment current\_time  }\ec\\

2680: 2:\>\> $ct := ct + \delta$ \\

2681: \>\>\> \bc{  for all states $s$ that were live at the last clock tick }\ec\\

2682: 4:\>\>\> $\forall s \in live(ct - \delta)$ \\

2683: \>\>\>\> \bc{  set current\_state to $s$.  }\ec\\

2684: 5:\>\>\>\> $cs := s$ \\

2685: \>\>\>\> \bc{  The procedure $new\_time\_matrix$ returns }\ec\\

2686: \>\>\>\> \bc{ $matrix(cs, ct)$: the matrix for the current state at the current time. }\ec\\

2687: \>\>\>\> \bc{ It also   }\ec\\

2688: \>\>\>\> \bc{ updates the function $prob$ with  the probability of remaining  }\ec\\

2689: \>\>\>\> \bc{ in the current state at the current time and the  probabilities of   }\ec\\

2690: \>\>\>\> \bc{ moving to  different states at the current time. }\ec\\

2691: \>\>\>\>  \bc{ It also updates the value of $error$. }\ec\\

2692: 6:\>\>\>\> $new\_time\_matrix(matrix(cs, ct),new\_states(cs,ct), remain(cs,ct), prob, error)$ \\

2693: \>\>\>\> \bc{ If the probability of remaining in current state at current time is zero  }\ec\\

2694: 7:\>\>\>\> if $remain(cs, ct) = false$ then \\

2695: \>\>\>\>\> \bc{  current state is not  live at current time and  }\ec\\ 

2696: \>\>\>\>\> \bc{  only the states which can be reached from current state at current time }\ec\\

2697: \>\>\>\>\> \bc{  are added to those live at current time }\ec\\

2698: 8:\>\>\>\>\> $live(ct) :=  live(ct) \bigcup new\_states(cs,ct)$ \\

2699: 9:\>\>\>\> else \bc{ $remain(cs, ct) = true$ }\ec\\

2700: \>\>\>\>\> \bc{  The current state, plus all states which may be reached from it at }\ec\\

2701: \>\>\>\>\> \bc{ the current time, must be added to the live states. }\ec\\

2702: 10:\>\>\>\>\> $live(ct) := live(ct) \bigcup \{cs\} \bigcup  new\_states(cs,ct)$ \\

2703: 11:\>\>\>\>end if \\

2704: 11a:\>\>\> end forall \bc{ $\forall s \in live(ct - \delta)$ }\ec\\

2705: \> \bc{ Now, we have $live(ct)$ and $prob(cs,ct)$ for all $cs$ in $live(ct)$ }\ec\\

2706: \> \bc{ i.e. all the states we could be in at time $ct$, and the probability of  }\ec\\

2707: \> \bc{ actually entering them in the previous time interval.  }\ec\\

2708: \> \bc{ }\ec\\

2709: \>\>\>\> \bc{ For every state which can be reached  at the current }\ec\\

2710: \>\>\>\> \bc{ time, we must see if it causes the formula to pass or fail, in }\ec\\

2711: \>\>\>\> \bc{ which cases we adjust the values for $total\_pass$ or }\ec\\

2712: \>\>\>\> \bc{ $total\_fail$ and remove the state from the $live$ set.  If we cannot yet }\ec\\

2713: \>\>\>\> \bc{ tell whether the formula is true or false, we must build the state/time matrix. }\ec\\

2714: 12:\>\>\>\> $\forall q \in live(ct)$  \\

2715: \>\>\>\>\> \bc{  if  $q \models a_1$, then formula is true }\ec\\

2716: 13:\>\>\>\>\> if $q \models a_1$ then \\

2717: \>\>\>\>\>\> \bc{ $total\_pass$ is incremented by the probability of entering $q$ }\ec\\

2718: \>\>\>\>\>\> \bc{  from the current state at the current time }\ec\\

2719: 14:\>\>\>\>\>\> $total\_pass := total\_pass + prob(q,ct)$ \\

2720: \>\>\>\>\>\> \bc{  State $q$ is removed from the live set }\ec\\

2721: 15:\>\>\>\>\>\> $live(ct) := live(ct) \setminus \{q\}$ \\

2722: \>\>\>\>\> \bc{  Otherwise, if  $q \models a_0$ (and $q$ is not a terminating state)  }\ec\\

2723: \>\>\>\>\> \bc{ then the formula may still be true, }\ec\\

2724: \>\>\>\>\> \bc{ so we must build $matrix(q,ct)$ and keep state $q$ in the $live(ct)$ set. }\ec\\

2725: 16:\>\>\>\>\> elseif $q \models a_0 \land q \not\in terminating\_states$ then \\

2726: \>\>\>\>\>\> \bc{ The procedure $new\_state\_matrix$ returns }\ec\\

2727: \>\>\>\>\>\> \bc{ $matrix(q,ct)$: the matrix for state $q$ at current time, and requires }\ec\\

2728: \>\>\>\>\>\> \bc{ $prob(q,ct)$: the probability of entering state $q$ from the current }\ec\\

2729: \>\>\>\>\>\> \bc{ state at the current time. }\ec\\

2730: 17:\>\>\>\>\>\> $new\_state\_matrix(matrix(q, ct), prob(q,ct))$ \\

2731: 18:\>\>\>\>\> else  \bc{ If $q$ does not model $a\_0$ or it is a terminating state and also  }\ec\\

2732: \>\>\>\>\>\>\> \bc{ it does not model $a\_1$ then the formula is false }\ec\\

2733: \>\>\>\>\>\>\> \bc{ $total\_fail$ is incremented by the probability of entering $q$ }\ec\\

2734: \>\>\>\>\>\>\> \bc{  from the current state at the current time }\ec\\

2735: 19:\>\>\>\>\>\> $total\_fail := total\_fail + prob(q,ct)$ \\

2736: \>\>\>\>\>\> \bc{  State $q$ is removed from the live set }\ec\\

2737: 20:\>\>\>\>\>\> $live(ct) := live(ct) \setminus \{q\}$ \\

2738: 21:\>\>\>\>\> end if \\

2739: 22:\>\>\>\> end forall \bc{ for all states  in  $live(ct)$ }\ec\\

2740: 23:\>\> until $total\_pass > p$ \bc{ formula has passed }\ec\\

2741: 24:\>\>\>\> or \\

2742: 25:\>\>\>\> $total\_fail \geq 1-p$ \bc{ formula has failed }\ec\\

2743: 26:\>\>\>\> or \\

2744: 27:\>\>\>\> ($error \geq 1-p \land error \geq p$) \bc{ no possibility of a pass or a fail }\ec\\

2745: 28:\>\>\>\> or \\

2746: 29:\>\>\>\> ct = t \bc{ time's up.}\ec\\

2747: 30:\>\> if ($ct = t$) then \\

2748: \>\>\> \bc{ All states undecided at the last iteration are now false, so }\ec\\

2749: \>\>\> \bc{ $total\_fail$ is set to  $1 - total\_pass - error$ }\ec\\

2750: 31: \>\>\> $total\_fail :=  1 - total\_pass - error$\\

2751: 32:\>\> end if \\

2752: \> \bc{}\ec\\

2753: \> \bc{ Output result, based on the values of}\ec\\ 

2754: \> \bc{ $total\_pass$, $total\_fail$ and $error$ }\ec\\

2755: 33:\>\> if $total\_pass  > p$ then \\

2756: \>\> \bc{ SA models formula  }\ec\\

2757: 34:\>\> output pass  \\

2758: 35:\>\> elseif  \bc{ $total\_fail \geq 1-p$ }\ec\\

2759: \>\> \bc{ SA does not model formula }\ec\\

2760: 36:\>\> output fail \\

2761: 37:\>\> else \bc{ errors are too large; cannot decide }\ec\\

2762: 38:\>\> output undecided \\

2763: 39:\>\> end if \\

2764: \end{tabbing}

2765: 

2766: 

2767: \begin{tabbing}

2768: ....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=

2769: \kill

2770: 

2771: \bc{ This procedure builds  the initial matrix. }\ec\\

2772: \bc{ We assume there are $n$ clocks associated with this state, }\ec\\

2773: \bc{ and $c^{s_0}_l$ is the $l$th clock. }\ec\\

2774: \bc{ We abbreviate $\lceil upper\_bound(c^{s_0}_l)\rceil.\frac{1}{\delta}$ by $N_l$. }\ec\\

2775: 

2776: \\

2777: $procedure \; init\_matrix(matrix(s_0,0))$ \\

2778: begin procedure \\

2779: \> $\forall 1 \leq i_1 \leq N_1$ \\

2780: \>\>\> $\vdots$ \\

2781: \> $\forall 1 \leq i_n \leq N_n . matrix(s_0,0)[i_1\ldots i_n] := {\displaystyle \prod_{l=1}^{n}} pr(c^{s_0}_l \in [i_l-\delta,i_l))$ \\

2782: end procedure \\

2783: \end{tabbing}

2784: 

2785: \begin{tabbing}

2786: ....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=

2787: \kill

2788: $procedure \; new\_time\_matrix(matrix(cs,ct),new\_states(cs,ct),remain(cs,ct),prob,error)$ \\

2789: \> \bc{ This procedure updates  a matrix by incrementing time, not by }\ec\\

2790: \> \bc{ changing state.  We can do this by considering the values in the previous time }\ec\\

2791: \> \bc{ matrix.   It also updates the function $prob$,}\ec\\

2792: \> \bc{ and the variable $error$.}\ec\\

2793: \> \bc{ There are $n$ clocks in state $cs$.}\ec\\

2794: begin procedure \\

2795: 1:\> $\forall 1 \leq i_1 \leq N_1$ \\

2796: \>\>\> $\vdots$ \\

2797: 2:\> $\forall 1 \leq i_{n} \leq N_{n} .$ \\

2798: \>\>\>\>\>\>\> \bc{  If one of the matrix indices is at its maximum value, then the }\ec\\

2799: \>\>\>\>\>\>\> \bc{ probability  value in this position must be zero.  This is }\ec\\

2800: \>\>\>\>\>\>\> \bc{ because this procedure is always the first to update a state/time matrix. }\ec\\

2801: \>\>\>\>\>\>\> \bc{  }\ec\\

2802: \>\>\>\>\>\>\> \bc{  }\ec\\

2803: 3:\>\>\>\>\>\>\> if $\exists l \leq n \bullet i_l = N_l$ then \\

2804: 4:\>\>\>\>\>\>\>\> $matrix(cs,ct)[i_1,\ldots , i_{n}] := 0$ \\

2805: \>\>\>\>\>\>\>\>  \bc{ otherwise the values in the matrix can be updated  simply from the }\ec\\

2806: \>\>\>\>\>\>\>\>  \bc{ values in the previous time matrix.  }\ec\\

2807: 5:\>\>\>\>\>\>\> else \bc{ all clocks $c_i$ are $\geq 1$ and $<N_i$ }\ec\\

2808: 6:\>\>\>\>\>\>\>\> $matrix(cs,ct)[i_1,\ldots ,i_{n}] := $\\

2809: 7:\>\>\>\>\>\>\>\>\>\> $matrix(cs,ct)[i_1,\ldots ,i_{n}] + matrix(cs,ct-\delta)[i_1{\scriptstyle +1},\ldots ,i_{n} {\scriptstyle +1}]$ \\

2810: \>\>\>\>\>\>\>\> \bc{ we record the fact that it is possible to remain in this state  }\ec\\

2811: \>\>\>\>\>\>\>\> \bc{ at this time. }\ec\\

2812: 8:\>\>\>\>\>\>\>\> $remain(cs,ct):= true$ \\

2813: 9:\>\>\>\>\>\>\> end if \\

2814: 9a:end forall \\

2815: \> \bc{ We now pick out the positions in the previous time matrix which, }\ec\\

2816: \> \bc{ when moved forward one unit in time, result in a new state.  }\ec\\

2817: 10:\> $\;\forall 1 \leq i_1 \leq N_1$ \\

2818: \>\>\> $\vdots$ \\

2819: 11:\> $\;\forall 1 \leq i_{n} \leq N_{n}$ \\

2820: \> \bc{ If more than one of the previous time matrix indices is one,  we know that }\ec\\

2821: \> \bc{  more than one of the clocks will have reached zero by $ct$, and so we  }\ec\\

2822: \> \bc{  add the probability to error.  }\ec\\

2823: 11a:\>\>\>\>\>\>\> if $\#\{ c_l \mid c_l = 1\} > 1$ then \\

2824: 12:\>\>\>\>\>\>\>\> $error := error + matrix(cs,ct-\delta)[i_1, \ldots , i_n]$ \\

2825: 12a:\>\>\>\>\>\>\> else if  $\#\{ c_l \mid c_l = 1\} = 1$\\

2826: \>\>\>\>\>\>\>\> \bc{   Given the stochastic Automaton $SA$, the state $cs$ and the clock $cc$ }\ec\\

2827: \>\>\>\>\>\>\>\> \bc{  $s'$ is the  resulting state.  If the clock is associated with more than  }\ec\\

2828: \>\>\>\>\>\>\>\> \bc{  one transition the function $pick$ (the adversary) chooses the }\ec\\

2829: \>\>\>\>\>\>\>\> \bc{ resulting state.  Otherwise the state is the one determined by the  }\ec\\

2830: \>\>\>\>\>\>\>\> \bc{ transition relation of the SA.  }\ec\\

2831: 13:\>\>\>\>\>\>\>\> $s' := pick(SA,cs,c_l)$ \\

2832: 13a:\>\>\>\>\>\>\>\> $new\_states(cs,ct) := new\_states(cs,ct) \bigcup \{s'\}$ \\

2833: \>\>\>\>\>\>\>\> \bc{  the probability of entering $s'$  at time $ct$ }\ec\\

2834: \>\>\>\>\>\>\>\> \bc{ is incremented by the matrix probability }\ec\\ 

2835: 14:\>\>\>\>\>\>\>\> $prob(s',ct) := prob(s',ct) + matrix(cs,ct-\delta)[i_1,\ldots , i_{n}]$ \\ 

2836: 22:\>\>\>\>\>\>

2837: \> end if \bc{line 11}\ec\\

2838: 23:\>\>\>\>\>\> end forall \\

2839: 24:end procedure \\

2840: \end{tabbing}

2841: 

2842: \begin{tabbing}

2843: ....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=

2844: \kill

2845: 

2846: \bc{ This procedure builds a new matrix, where the state is new rather than the time }\ec\\

2847: \bc{ We assume there are $n$ clocks associated with this state, }\ec\\

2848: \bc{ and $c^{s}_l$ is the $l$th clock. }\ec\\

2849: \bc{ We abbreviate $\lceil upper\_bound(c^{s}_l)\rceil.\frac{1}{\delta}$ by $N_l$. }\ec\\

2850: \bc{ The values in the matrix are calculated by  multiplying the clock }\ec\\

2851: \bc{ probabilities by a factor of $p$, where $p$ is the probability of }\ec\\

2852: \bc{ entering the state, and adding this value to the value already in }\ec\\

2853: \bc{ the position.  }\ec\\

2854: 

2855: \\

2856: $procedure \; new\_state\_matrix(matrix(cs,ct),p)$ \\

2857: begin procedure \\

2858: \> $\forall 1 \leq i_1 \leq N_1$ \\

2859: \>\>\> $\vdots$ \\

2860: \> $\forall 1 \leq i_{n} \leq N_{n} . matrix(cs,ct)[i_1,\ldots ,i_{n}] := $\\

2861: \>\>\>\>\>\>\>\>\>\> $matrix(cs,ct)[i_1,\ldots ,i_{n}] + (p \times {\displaystyle \prod_{l=1}^{n}} pr(c^{s}_l \in [i_l-\delta,i_l))\;)$ \\

2862: end procedure \\

2863: \end{tabbing}

2864: 

2865: % \begin{tabbing}

2866: % ....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=....\=

2867: % \kill

2868: % 

2869: % $procedure \; add((s,p),S)$ \\

2870: % begin procedure \\

2871: % \> if $\exists p'. (s,p') \in S$ then \\

2872: % \>\> $S := S \setminus \{(s,p')\} \bigcup \{(s,p+p')\}$ \\

2873: % \> else \\

2874: % \>\> $S := S \bigcup \{(s,p)\}$ \\

2875: % \> end if \\

2876: % end procedure \\

2877: % \end{tabbing}

2878: 

2879: 

2880:  \end{document}

2881: 

2882: 

2883:  

2884: