1 Introduction
1.1 Related work
1.2 Outline
2 Partially observable Markov decision processes
2.1 Markov decision processes
-
S is a set of states;
-
\({\bar{s}}\in S\) is an initial state;
-
A is a set of actions;
-
\(P : S \times A \rightarrow { Dist }(S)\) is a (partial) probabilistic transition function;
-
\( R = ( R _S, R _A)\) is a reward structure where \( R _S : S \rightarrow \mathbb {R}\) is a state reward function and \( R _A : S \times A \rightarrow \mathbb {R}\) an action reward function.
2.2 Partially observable Markov decision processes
-
\((S,{\bar{s}},A,P, R )\) is an MDP;
-
\(\mathcal {O}\) is a finite set of observations;
-
\( obs : S \rightarrow \mathcal {O}\) is a labelling of states with observations;
-
\(\sigma \) is a strategy of the MDP \((S,{\bar{s}},A,P,R)\);
-
for any paths \(\pi =s_0 \xrightarrow {a_0}s_1 \xrightarrow {a_1}\cdots s_n\) and \(\pi '=s_0' \xrightarrow {a_0'} s_1'\xrightarrow {a_1'} \cdots s_n'\) satisfying \( obs (s_i)= obs (s_i')\) and \(a_i=a_i'\) for all i, we have \({\sigma }(\pi )={\sigma }(\pi ')\).
2.3 Parallel composition of POMDPs
-
if \(a \in A_1 \cap A_2\), then \(a \in A(s_1,s_2)\) if and only if \(a \in A(s_1) \cap A(s_2)\) withfor all \(s' = (s_1',s_2') \in S_1 \times S_2\) and \(R_{A}(s,a) = R_{A,1}(s_1,a) + R_{A,2}(s_2,a)\);$$\begin{aligned} P(s,a)(s') = P_1(s_1,a)(s_1') {\cdot } P_2(s_2,a)(s_2') \end{aligned}$$
-
if \(a \in A_1 {\setminus } A_2\), then \(a \in A(s_1,s_2)\) if and only if \(a \in A(s_1)\) withfor all \(s' = (s_1',s_2') \in S_1 \times S_2\) and \(R_{A}(s,a) = R_{A,1}(s_1,a_1)\);$$\begin{aligned} P(s,a)(s') = \left\{ \begin{array}{ll} P_1(s_1,a)(s_1') &{} \quad {if\,\,s_2=s_2'} \\ 0 &{} \quad {otherwise} \end{array} \right. \end{aligned}$$
-
if \(a \in A_2 {\setminus } A_1\), then \(a \in A(s_1,s_2)\) if and only if \(a \in A(s_2)\) withfor all \(s' = (s_1',s_2') \in S_1 \times S_2\) and \(R_{A}(s,a) = R_{A,2}(s_2,a_2)\);$$\begin{aligned} P(s,a)(s') = \left\{ \begin{array}{ll} P_2(s_2,a)(s_2') &{} \quad {if\,\,s_1=s_1'} \\ 0 &{} \quad {otherwise} \end{array} \right. \end{aligned}$$
-
\(R_{S}(s) = R_{S,1}(s_1) + R_{S,2}(s_2)\);
-
\( obs (s) = ( obs _1(s_1) , obs _2(s_2))\).
3 Verification and strategy synthesis for POMDPs
3.1 Property specification
3.2 Verification and strategy synthesis for POMDPs
3.3 Numerical computation algorithms
-
\(M=2\) yields 34 grid points and the bounds \([4.3846,\infty ]\);
-
\(M=3\) yields 74 grid points and the bounds [4.8718, 5.3077];
-
\(M=4\) yields 150 grid points and the bounds [4.8846, 5.3077];
-
\(M=5\) yields 283 grid points and the bounds [5.0708, 5.3077];
-
\(M=6\) yields 501 grid points and the bounds [5.3077, 5.3077].
4 Partially observable probabilistic timed automata
4.1 Time, clocks and clock constraints
4.2 Syntax of POPTAs
-
\( L \) is a finite set of locations and \(\overline{l}\in L \) is an initial location;
-
\(\mathcal {X}\) is a finite set of clocks;
-
\( A \) is a finite set of actions;
-
\( inv : L {\rightarrow } CC ({\mathcal {X}})\) is an invariant condition;
-
\( enab : L \times A {\rightarrow } CC ({\mathcal {X}})\) is an enabling condition;
-
\( prob : L \times A {\rightarrow }{ Dist }(2^{\mathcal {X}} \times L )\) is a probabilistic transition function;
-
\( r = ( r _{ L }, r _{ A })\) is a reward structure where \( r _{ L }: L \rightarrow \mathbb {R}\) is a location reward function and \( r _{ A }: L \times A {\rightarrow }\mathbb {R}\) is an action reward function.
-
location rewards, which are accumulated at rate \( r _{ L }(l)\) while in location l;
-
action rewards \( r _{ A }(l,a)\), which are accumulated when taking action a in location l.
-
\(( L , \overline{l}, \mathcal {X}, A , inv , enab , prob , r )\) is a PTA;
-
\(\mathcal {O}_ L \) is a finite set of observations;
-
\( obs _ L : L \rightarrow \mathcal {O}_ L \) is a location observation function.
4.3 Semantics of POPTAs
-
\(S = \{ (l,v) \in L \times \mathbb {T}^\mathcal {X}\mid v \models inv (l)\}\) and \({\bar{s}}= (\overline{l},\mathbf {0})\);
-
for any \((l,v) \in S\) and \(a \in A \cup \mathbb {T}\), we have \(P((l,v),a) = \mu \) if and only if one of the following conditions hold:
-
(time transitions) \(a \in \mathbb {T}\), \(\mu = \delta _{(l,v + a)}\) and \(v + a \models inv (l)\) for all \(0 \leqslant t' \leqslant a\);
-
(action transition) \(a \in A \), \(v \models enab (l,a)\) and for \((l',v') \in S\):$$\begin{aligned} \begin{array}{c} \mu (l',v') = \sum \limits _{X \subseteq \mathcal {X}\wedge v' = v[X:=0]} prob (l,a)(X,l') \end{array} \end{aligned}$$
-
-
for any \((l,v) \in S\) and \(a \in A \cup \mathbb {T}\):$$\begin{aligned} R _S(l,v)= & {} r _{ L }(l) \\ R _A((l,v),a)= & {} \left\{ \begin{array}{ll} r _{ L }(l){\cdot }a &{}\quad if a \in {\mathbb {T}} \\ r _{ A }(l,a) &{}\quad {if a \in { A }.} \end{array} \right. \end{aligned}$$
-
\((S,{\bar{s}}, A \cup \mathbb {T},P,R)\) is the semantics of the PTA \(( L , \overline{l}, \mathcal {X}, A , inv , enab , prob , r )\);
-
for any \((l,v) \in S\), we have \( obs (l,v)=( obs _ L (l),v)\).
4.4 Parallel composition of POPTAs
-
If \(a \in A _1 \cap A _2\), then since \(X \subseteq \mathcal {X}_1 \cup \mathcal {X}_2\) either \(x \in \mathcal {X}_1\) or \(x \in \mathcal {X}_2\). When \(x \in \mathcal {X}_1\), since \(\mathsf{P}_1\) satisfies Assumption 2, it follows that \(v \not \models inv _1(l_1)\) or \(v \not \models enab _1(l_1,a)\). On the other hand, when \(x \in \mathcal {X}_2\), since \(\mathsf{P}_2\) satisfies Assumption 2, it follows that \(v \not \models inv _2(l_2)\) or \(v \not \models enab _2(l_2,a)\). In either case, if follows from Definition 17 that \(v \not \models inv (l)\) or \(v \not \models enab (l,a)\).
-
If \(a \in A _1\), then by Definition 17 and since \( prob (l,a)(X,l'){>}0\) we have \(X \subseteq \mathcal {X}_1\) and \( prob (l_1,a)(X,l_1'){>}0\). Therefore \(x \in \mathcal {X}_1\) using the fact that \(\mathsf{P}_1\) satisfies Assumption 2 it follows that \(v \not \models inv _1(l_1)\) or \(v \not \models enab _1(l_1,a)\). Again using Definition 17 it follows that \(v \not \models inv (l)\) or \(v \not \models enab (l,a)\).
-
If \(a \in A _2\), then using similar arguments to the case above and the fact \(\mathsf{P}_2\) satisfies Assumption 2 we have \(v \not \models inv (l)\) or \(v \not \models enab (l,a)\).
4.5 Example POPTAs
5 Verification and strategy synthesis for POPTAs
5.1 Property specification
5.2 Verification and strategy synthesis
-
decide if \({ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R},{\sigma }{\,\models \,}\phi \) holds for all strategies \({\sigma }{\in }{\Sigma }_{{ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R}}\);
-
find, if it exists, a strategy \({\sigma }{\in }{\Sigma }_{{ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R}}\) such that \({ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R},{\sigma }{\,\models \,}\phi \).
5.3 Numerical computation algorithms
5.4 Correctness of the digital clocks reduction
-
\({ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R},{\sigma }{\,\models \,}\phi \) holds for all strategies \({\sigma }{\in }{\Sigma }_{{ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R}}\) if and only if \({ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {N},{\sigma }{\,\models \,}\phi \) holds for all strategies \({\sigma }{\in }{\Sigma }_{{ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {N}}\);
-
there exists a strategy \({\sigma }{\in }{\Sigma }_{{ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R}}\) such that \({ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R},{\sigma }{\,\models \,}\phi \) if and only if there exists a strategy \({\sigma }' {\in }{\Sigma }_{{ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {N}}\) such that \({ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {N},{\sigma }'{\,\models \,}\phi \);
-
if a strategy \({\sigma }{\in }{\Sigma }_{{ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {N}}\) is such that \({ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {N},{\sigma }{\,\models \,}\phi \), then \({\sigma }{\in }{\Sigma }_{{ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R}}\) and \({ [ \! [ {\mathsf{P}} ] \! ]}_\mathbb {R},{\sigma }{\,\models \,}\phi \).
-
\({ Dist }( L , obs _ L )\) denotes the subset of \({ Dist }( L )\) where \(\lambda \in { Dist }( L , obs _ L )\) if and only if, for \(l,l' \in L \) such that \(\lambda (l){>}0\) and \(\lambda (l'){>}0\) we have \( obs _ L (l)= obs _ L (l')\);
-
the invariant condition \( inv ^{\mathcal {B}}: { Dist }( L , obs _ L ) {{\rightarrow }} CC ({\mathcal {X}})\) and enabling condition \( enab ^{\mathcal {B}}: { Dist }( L , obs _ L ) \times A {\rightarrow } CC ({\mathcal {X}})\) are such that, for \(\lambda \in { Dist }( L , obs _ L )\) and \(a \in A \), we have \( inv ^{\mathcal {B}}(\lambda )= inv (l)\) and \( enab ^{\mathcal {B}}(\lambda ,a)= enab (l,a)\) where \(l \in L \) and \(\lambda (l){>}0\);
-
the probabilistic transition function:is such that, for any \(\lambda ,\lambda ' \in { Dist }( L , obs _ L )\), \(a \in A \) and \(X \subseteq \mathcal {X}\) we have:$$\begin{aligned} prob ^{\mathcal {B}}: { Dist }( L , obs _ L ) \times A {\rightarrow }{ Dist }(2^{\mathcal {X}} \times { Dist }( L , obs _ L )) \end{aligned}$$and, for any \(l' \in L \):$$\begin{aligned} \begin{array}{c} prob ^{\mathcal {B}}(\lambda ,a)(\lambda ',X) = \sum \limits _{l \in L } \lambda (l) \cdot \left( \sum \limits _{o \in O \wedge \lambda ^{a,o,X} = \lambda '} \sum \limits _{l' \in L \wedge obs _ L (l')=o} \!\!\!\!\!\! prob (l,a)(l',X) \right) \end{array} \end{aligned}$$$$\begin{aligned} \lambda ^{a,o,X}(l') = \left\{ \begin{array}{ll} \frac{\sum _{l \in L } prob (l,a)(l',X) {\cdot } \lambda (l)}{\sum _{l \in L } \lambda (l) {\cdot } \left( \sum _{l^{{\scriptstyle \prime }} \in L \wedge obs _{{\scriptstyle L }}(l^{{\scriptstyle \prime }})=o} prob (l,a)(l',X) \right) } &{} \quad {if\, obs _ L (l')=o} \\ 0 &{} \quad \text{ otherwise; } \end{array} \right. \end{aligned}$$
-
the reward structure \( r ^{\mathcal {B}}= ( r _{ L }^{\mathcal {B}}, r _{ A }^{\mathcal {B}})\) consists of a location reward function \( r _{ L }^{\mathcal {B}}: { Dist }( L , obs _ L ) {\rightarrow }\mathbb {R}\) and action reward function \( r _{ A }^{\mathcal {B}}: { Dist }( L , obs _ L ) \times A \rightarrow \mathbb {R}\) such that, for any \(\lambda \in { Dist }( L , obs _ L )\) and \(a \in A \):$$\begin{aligned} \begin{array}{c} r _{ L }^{\mathcal {B}}(\lambda ) = \sum _{l \in L } \lambda (l) \cdot r _{ L }(l) \qquad \text{ and } \qquad r _{ A }^{\mathcal {B}}(\lambda ,a) = \sum _{l \in L } \lambda (l) \cdot r _A(l,a) . \end{array} \end{aligned}$$
-
For any belief states \((\lambda ,v)\) and \((\lambda ',v')\) and action \(a \in A \):where for any \(l' \in L \):$$\begin{aligned}&P^{\mathcal {B}}((\lambda ,v),a)(\lambda ',v')\\&\quad = \, \sum \limits _{\begin{array}{c} o \in \mathcal {O}_ L \\ \lambda ^{a,(o,v^{{\scriptstyle \prime }})}=\lambda ' \end{array}}\sum \limits _{l \in L } \lambda (l) \cdot \left( \sum \limits _{\begin{array}{c} l' \in L \\ \mathcal {O}(l')=o \end{array}} P((l,v),a)(l',v') \right) \\&\quad = \, \sum \limits _{\begin{array}{c} o \in \mathcal {O}_ L \\ \lambda ^{a,(o,v^{{\scriptstyle \prime }})}=\lambda ' \end{array}}\sum \limits _{l \in L } \lambda (l) \cdot \left( \sum \limits _{\begin{array}{c} l' \in L \\ \mathcal {O}(l')=o \end{array}} prob (l,a)(X_{[v \mapsto v']},l') \right) \qquad \text{ by } (3) \\&\quad = \, \sum \limits _{l \in L } \lambda (l) \cdot \left( \sum \limits _{\begin{array}{c} o \in \mathcal {O}_ L \\ \lambda ^{a,(o,v^{{\scriptstyle \prime }})}=\lambda ' \end{array}} \sum \limits _{\begin{array}{c} l' \in L \\ \mathcal {O}(l')=o \end{array}} prob (l,a)(X_{[v \mapsto v']},l') \right) \qquad \text{ rearranging } \end{aligned}$$Using this result, together with Definitions 22 and 14, it follows that the probabilistic transition functions are isomorphic in the case. For the action reward functions, we have:$$\begin{aligned}&\lambda ^{a,(o,v')}(l') \\&\quad = \; \left\{ \begin{array}{ll} \frac{\sum _{l \in L } P((l,v),a)(l',v') \cdot \lambda (l)}{\sum _{l \in L } \lambda (l) \cdot \left( \sum _{l^{{\scriptstyle \prime \prime }} \in L \wedge obs _{{\scriptstyle L }}(l^{{\scriptstyle \prime \prime }})=o} P((l,v),a)(l'',v') \right) } &{} \quad {if\; obs _ L (l')=o} \\ 0 &{} \quad \text{ otherwise } \end{array} \right. \\&\quad = \; \left\{ \begin{array}{ll} \frac{\sum _{l \in L } prob (l,a)(X_{[v \mapsto v']},l') \cdot \lambda (l)}{\sum \limits _{l \in L } \lambda (l) \cdot \left( \sum \limits _{l^{{\scriptstyle \prime \prime }} \in L \wedge obs _{{\scriptstyle L }}(l^{{\scriptstyle \prime \prime }})=o} prob (l,a)(X_{[v \mapsto v^{{\scriptstyle \prime }}]},l') \right) } &{} \quad {if\; obs _ L (l')=o} \\ 0 &{} \quad \text{ otherwise } \end{array} \right. \qquad \text{ by } (3)\\&\quad = \; \lambda ^{a,o,X_{[v \mapsto v']}} \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{ by } \text{ Definition }~(22). \end{aligned}$$which, again from Definitions 22 and 14, shows that the reward functions are isomorphic in this case.$$\begin{aligned} \begin{array}{c} R ^{\mathcal {B}}_A((\lambda ,v),a) = \sum \limits _{l\in L } r _ A (l,a) {\cdot } \lambda (l) \end{array} \end{aligned}$$
-
For any belief states \((\lambda ,v)\) and \((\lambda ',v')\) and time duration \(t \in \mathbb {T}\):where for any \(l' \in L \):$$\begin{aligned} P^{\mathcal {B}}((\lambda ,v),t)(\lambda ',v')&= \; \left\{ \begin{array}{ll} \sum \limits _{l \in L } \lambda (l) \cdot P((l,v),a)(l,v') &{} \quad {if\; \lambda ^{t,(o_\lambda ,v')}=\lambda '} \\ 0 &{} \quad \text{ otherwise } \end{array} \right. \end{aligned}$$Substituting this expression for \(\lambda ^{t,(o_\lambda ,v')}\) into that of \(P^{\mathcal {B}}((\lambda ,v),t)\) we have:$$\begin{aligned} \lambda ^{t,(o_\lambda ,v')}(l')&= \left\{ \begin{array}{ll} \frac{\lambda (l')}{\sum \limits _{l \in L } \lambda (l)} &{} \quad {if\; v'=v + t} \\ 0 &{} \quad \text{ otherwise } \end{array} \right. \\&= \left\{ \begin{array}{ll} \lambda (l') &{} \quad {if \;v'=v + t} \\ 0 &{} \quad \text{ otherwise } \end{array} \right.&{\mathrm{since}\; \lambda \;\text {is a distribution}.} \end{aligned}$$which, from Definitions 22 and 14, shows the probabilistic transition functions are isomorphic. For the action reward function of \({\mathcal {B}}( [ \! [ {\mathsf{P}} ] \! ]_\mathbb {T})\), we have \( R ^{\mathcal {B}}_A((\lambda ,v),t) = \sum _{l\in L } ( r _ L (l) {\cdot } t ) {\cdot } \lambda (l)\) and, from Definitions 22 and 14, this implies that the action reward functions are isomorphic.$$\begin{aligned}&{P^{\mathcal {B}}((\lambda ,v),t)(\lambda ',v')} \\&\quad = \; \left\{ \begin{array}{ll} \sum \limits _{l \in L } \lambda (l) \cdot \left( \sum \limits _{l' \in L } P((l,v),a)(l',v') \right) &{} \quad \text{ if }\; \lambda =\lambda ' \;\mathrm{and}\; v'=v + t \\ 0 &{} \quad \text{ otherwise } \end{array} \right. \\&\quad = \; \left\{ \begin{array}{ll} \sum \limits _{l \in L } \lambda (l) &{} \quad \text{ if }\; \lambda =\lambda '\; \mathrm{and}\; v'=v + t \\ 0 &{} \quad \text{ otherwise } \end{array} \right. \qquad \text{ by }(4) \\&\quad = \; \left\{ \begin{array}{ll} 1 &{} \quad \text{ if }\; \lambda =\lambda '\; \mathrm{and}\; v'=v + t \\ 0 &{} \quad \text{ otherwise } \end{array} \right. \qquad \text{ since } \;\lambda \; \text {is a distribution} \end{aligned}$$
6 Implementation and case studies
6.1 Modelling POMDPs and POPTAs in PRISM
6.2 Wireless network scheduling
-
if the packet for the current time period has been sent;
-
the priority of the current packet to be sent;
-
the status of the channel.
-
\( \texttt {R}\{{``} priority {''}\}\texttt {max}=?[\texttt {F} \; ( sched =0 \; \& \; t = T {-}1 \; \& \; k = K {-}1) \; ]\);
-
\( \texttt {R}\{{``} dropped\_packets {''}\}\texttt {min}=?[\texttt {F} \; ( sched =0 \; \& \; t = T {-}1 \; \& \; k = K {-}1) \; ]\).
6.3 Task-graph scheduler
-
time for addition 2 and 5 picoseconds for processors \(P_1\) and \(P_2\);
-
time for multiplication 3 and 7 picoseconds for processors \(P_1\) and \(P_2\);
-
idle energy usage 10 and 20 Watts for processors \(P_1\) and \(P_2\);
-
active energy usage 90 and 30 Watts for processors \(P_1\) and \(P_2\).
6.4 The NRL pump
6.5 Non-repudiation protocol
6.6 The dining cryptographers protocol
Case study (parameters) | Property | Verification/strategy synthesis of POMDP | MDP result | |||||||
---|---|---|---|---|---|---|---|---|---|---|
States | Num. obs. | Num. hidd. | Res. (M) | Grid points | Time (s) | Result (bounds) | ||||
Wireless network sched. (c T K) | 2 2 20 |
\({\texttt {R}}_{\min =?}[{{\texttt {F}\ } done }]\) (dropped packets) | 754 | 214 | 4 | 16 | 151,811 | 34.2 | [19.3, 19.3] | 15.9 |
2 4 20 | 2029 | 533 | 4 | 16 | 457,233 | 190.3 | [10.2, 10.3] | 8.26 | ||
2 8 20 | 4589 | 1173 | 4 | 16 | 1,077,393 | 893.3 | [3.2, 3.2] | 2.56 | ||
3 3 8 | 1714 | 234 | 8 | 8 | 1,171,699 | 428.4 | [9.4, 9.9] | 6.61 | ||
3 4 8 | 4777 | 617 | 8 | 6 | 967,729 | 654.6 | [3.63, 4.20] | 2.51 | ||
3 5 8 | 6825 | 873 | 8 | 6 | 1,407,025 | 1461 | [2.00, 2.34] | 1.33 | ||
Wireless network sched.(c T K) | 2 2 8 |
\({\texttt {R}}_{\max =?}[{{\texttt {F}\ } done }]\) (priorities cumul.) | 1534 | 410 | 4 | 12 | 158,159 | 43.5 | [125, 125] | 143 |
2 4 8 | 3577 | 921 | 4 | 12 | 387,193 | 174.3 | [180, 180] | 191 | ||
2 8 8 | 7673 | 1945 | 4 | 12 | 853,113 | 707.9 | [222, 222] | 225 | ||
3 3 2 | 3932 | 524 | 8 | 4 | 133,915 | 90.51 | [44.1, 47.2] | 56.8 | ||
3 4 2 | 5971 | 779 | 8 | 4 | 215,899 | 167.8 | [55.5, 58.9] | 67.0 | ||
3 5 2 | 8019 | 1035 | 8 | 4 | 300,259 | 277.6 | [64.1, 67.4] | 73.6 | ||
nrp discrete (K) | 4 |
\({\texttt {P}}_{\max =?}[\,{{\texttt {F}\ } unfair }\,]\)
| 39 | 21 | 5 | 4 | 173 | 0.1 | [0.25, 0.375] | 1.0 |
4 | 39 | 21 | 5 | 12 | 1685 | 0.2 | [0.25, 0.25] | 1.0 | ||
8 | 125 | 41 | 9 | 4 | 2385 | 0.7 | [0.13, 0.38] | 1.0 | ||
8 | 125 | 41 | 9 | 16 | 1,038,321 | 124.0 | [0.13, 0.18] | 1.0 | ||
Dining crypt(N) | 3 |
\({\texttt {P}}_{\min =?}[\,{{\texttt {F}\ } paid }\,]\)
| 179 | 90 | 6 | 4 | 606 | 0.16 | [0.5, 0.5] | 0.0 |
4 | 964 | 282 | 15 | 8 | 674,398 | 210.5 | [0.082, 0.333] | 0.0 | ||
5 | 4741 | 842 | 36 | 4 | 746,020 | 907.5 | [0.0, 0.25] | 0.0 | ||
6 | 22,406 | 2458 | 85 | 2 | 210,256 | 505.7 | [0.0, 0.2] | 0.0 | ||
Dining crypt(N) | 3 |
\({\texttt {P}}_{\max =?}[\,{{\texttt {F}\ } paid }\,]\)
| 179 | 90 | 6 | 4 | 606 | 0.16 | [0.5, 0.5] | 1.0 |
4 | 964 | 90 | 15 | 8 | 674,398 | 209.8 | [0.333, 0.568] | 1.0 | ||
5 | 4741 | 842 | 36 | 4 | 746,020 | 1044 | [0.25, 1.0] | 1.0 | ||
6 | 22,406 | 2458 | 85 | 2 | 210,256 | 1046 | [0.2, 1.0] | 1.0 | ||
Grid(n) | 3 |
\({\texttt {R}}_{\min =?}[{{\texttt {F}\ } target }]\)
| 11 | 3 | 9 | 4 | 331 | 0.1 | [2.63, 2.88] | 2.0 |
3 | 11 | 3 | 9 | 8 | 6436 | 1.0 | [2.84, 2.88] | 2.0 | ||
4 | 17 | 3 | 16 | 4 | 3061 | 0.8 | [3.27, 4.13] | 2.73 | ||
4 | 17 | 3 | 16 | 8 | 319,771 | 60.6 | [3.91, 4.13] | 2.73 | ||
Grid(n k) | 3 1 |
\({\texttt {P}}_{\max =?}[\,{{\texttt {F}^{\leqslant k}\ } target }\,]\)
| 18 | 4 | 9 | 8 | 12,871 | 1.7 | [0.13, 0.13] | 0.25 |
3 2 | 27 | 6 | 9 | 4 | 991 | 0.4 | [0.38, 0.38] | 0.75 | ||
3 3 | 36 | 8 | 9 | 4 | 1321 | 0.3 | [0.75, 0.75] | 1.0 | ||
3 4 | 45 | 10 | 9 | 2 | 181 | 0.1 | [1.0, 1.0] | 1.0 | ||
4 2 | 48 | 6 | 16 | 3 | 2041 | 0.7 | [0.2, 0.2] | 0.33 | ||
4 4 | 80 | 10 | 16 | 6 | 193,801 | 24.5 | [0.53, 0.63] | 1.0 | ||
4 5 | 96 | 12 | 16 | 6 | 232,561 | 33.5 | [0.80, 0.85] | 1.0 | ||
4 6 | 112 | 14 | 16 | 2 | 841 | 0.6 | [1.0, 1.0] | 1.0 |
Case study (parameters) | Property | Verification/strategy synthesis of POPTA | PTA result | |||||||
---|---|---|---|---|---|---|---|---|---|---|
States (\( [ \! [ {\mathsf{P}} ] \! ]_\mathbb {N}\)) | Num. obs. | Num. hidd. | Res. (M) | Grid points | Time (s) | Result (bounds) | ||||
Scheduler basic(\( sleep \)) | 0.25 |
\({\texttt {R}}_{\min =?}[{{\texttt {F}\ } done }]\) (exec. time) | 2090 | 1619 | 2 | 2 | 2537 | 1.6 | [15.84, 15.84] | 15.59 |
0.5 | 2090 | 1619 | 2 | 2 | 2537 | 1.3 | [21.1, 21.1] | 18.0 | ||
0.75 | 2090 | 1619 | 2 | 4 | 3463 | 1.9 | [19.25, 19.25] | 20.38 | ||
Scheduler basic (\( sleep \)) | 0.25 |
\({\texttt {R}}_{\min =?}[{{\texttt {F}\ } done }]\) (energy cons.) | 2090 | 1619 | 2 | 2 | 2537 | 1.0 | [1.849, 1.849] | 1.834 |
0.5 | 2090 | 1619 | 2 | 2 | 2537 | 1.8 | [2.149, 2.149] | 2.119 | ||
0.75 | 2090 | 1619 | 2 | 4 | 3463 | 2.1 | [2.444, 2.444] | 2.399 | ||
Scheduler prob (\( sleep \)) | 0.25 |
\({\texttt {R}}_{\min =?}[{{\texttt {F}\ } done }]\) (exec. time) | 5484 | 4204 | 2 | 2 | 6662 | 4.5 | [16.21, 16.21] | 15.96 |
0.5 | 5484 | 4204 | 2 | 2 | 6662 | 3.4 | [18.73, 18.73] | 18.23 | ||
0.75 | 5484 | 4204 | 2 | 4 | 9154 | 5.2 | [21.29, 21.29] | 20.53 | ||
Scheduler prob (\( sleep \)) | 0.25 |
\({\texttt {R}}_{\min =?}[{{\texttt {F}\ } done }]\) (energy cons.) | 5484 | 4204 | 2 | 4 | 6662 | 3.5 | [1.890, 1.890] | 1.875 |
0.5 | 5484 | 4204 | 2 | 2 | 6662 | 4.0 | [2.177, 2.177] | 2.147 | ||
0.75 | 5484 | 4204 | 2 | 4 | 9154 | 4.7 | [2.461, 2.461] | 2.416 | ||
Pump (\(h_1\)
N) | 16 2 |
\({\texttt {P}}_{\max =?}[\,{{\texttt {F}\ } guess }\,]\)
| 243 | 145 | 3 | 2 | 342 | 0.7 | [0.940, 0.992] | 1.0 |
16 2 | 243 | 145 | 3 | 40 | 4845 | 4.0 | [0.940, 0.941] | 1.0 | ||
16 16 | 1559 | 803 | 3 | 2 | 2316 | 16.8 | [0.999, 0.999] | 1.0 | ||
Pump (\(h_1\)
N
D) | 8 4 50 |
\({\texttt {P}}_{\max =?}[\,{\texttt {F}^{\leqslant D}\, guess }\,]\)
| 12,167 | 7079 | 3 | 2 | 17,256 | 11.0 | [0.753, 0.808] | 1.0 |
8 4 50 | 12,167 | 7079 | 3 | 12 | 68,201 | 36.2 | [0.763, 0.764] | 1.0 | ||
16 8 50 | 26,019 | 13,909 | 3 | 2 | 38,130 | 52.8 | [0.501, 0.501] | 1.0 | ||
16 8 100 | 59,287 | 31,743 | 3 | 2 | 86,832 | 284.8 | [0.531, 0.532] | 1.0 | ||
nrp basic (K) | 4 |
\({\texttt {P}}_{\max =?}[\,{{\texttt {F}\ } unfair }\,]\)
| 365 | 194 | 5 | 8 | 5734 | 0.8 | [0.25, 0.281] | 1.0 |
4 | 365 | 194 | 5 | 24 | 79,278 | 5.9 | [0.25, 0.25] | 1.0 | ||
8 | 1273 | 398 | 9 | 4 | 23,435 | 4.8 | [0.125, 0.375] | 1.0 | ||
8 | 1273 | 398 | 9 | 8 | 318,312 | 304.6 | [0.125, 0.237] | 1.0 | ||
nrp complex(K) | 4 |
\({\texttt {P}}_{\max =?}[\,{{\texttt {F}\ } unfair }\,]\)
| 1501 | 718 | 5 | 4 | 7480 | 2.1 | [0.438, 0.519] | 1.0 |
4 | 1501 | 718 | 5 | 12 | 72,748 | 14.8 | [0.438, 0.438] | 1.0 | ||
8 | 5113 | 1438 | 9 | 2 | 16,117 | 6.1 | [0.344, 0.625] | 1.0 | ||
8 | 5113 | 1438 | 9 | 4 | 103,939 | 47.1 | [0.344, 0.520] | 1.0 |
-
Each cryptographer flips an unbiased coin and only informs the cryptographer on the right of the outcome.
-
Each cryptographer states whether the two coins that it can see (the one it flipped and the one the left-hand neighbour flipped) are the same (‘agree’) or different (‘disagree’). However, if a cryptographer actually paid for dinner, then the cryptographer instead states the opposite (‘disagree’ if the coins are the same and ‘agree’ if the coins are different).