Verification and Control of Turn-Based Probabilistic Real-Time Games

David Parker; Gethin Norman; Marta Kwiatkowska

arxiv: 1906.09142 · v3 · pith:XND3DVK5new · submitted 2019-06-21 · 💻 cs.LO

Verification and Control of Turn-Based Probabilistic Real-Time Games

Marta Kwiatkowska , Gethin Norman , David Parker This is my paper

Pith reviewed 2026-05-25 18:22 UTC · model grok-4.3

classification 💻 cs.LO

keywords turn-based gamesprobabilistic timed automatadigital clocksquantitative verificationreachability probabilityexpected pricemulti-player gamesreal-time systems

0 comments

The pith

Digital clocks abstraction extends to turn-based probabilistic timed multi-player games to compute reachability probabilities and expected prices.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces turn-based probabilistic timed multi-player games, which combine probabilistic choice, real-time clocks, and nondeterministic decisions by multiple players. Building on the digital clocks method previously used for probabilistic timed automata, it demonstrates how to calculate the probability and expected cumulative price of reaching a target state. This supports quantitative analysis for properties like safety and performance in real-time systems with multiple decision makers. Readers would care because it provides a way to obtain formal guarantees on system behavior in settings that mix timing, randomness, and strategic interaction.

Core claim

We propose the model of turn-based probabilistic timed multi-player games, which incorporates probabilistic choice, real-time clocks and nondeterministic behaviour across multiple players. Building on the digital clocks approach for the simpler model of probabilistic timed automata, we show how to compute the key measures that underlie quantitative verification, namely the probability and expected cumulative price to reach a target. We illustrate this on case studies from computer security and task scheduling.

What carries the argument

The digital clocks abstraction applied to turn-based probabilistic timed multi-player games, used to compute the probability and expected cumulative price to reach a target.

If this is right

Quantitative verification can now address multi-player real-time probabilistic systems for safety, reliability and performance guarantees.
Controllers can be synthesised that ensure the computed probability and expected price measures meet required thresholds.
The same approach applies to case studies involving computer security and task scheduling.
The underlying measures of probability and expected price to a target become computable in this game setting.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The method could be tested on games with more than two players to check scalability of the abstraction.
It may connect to analysis of systems where timing influences the outcomes of player interactions.
Practical extensions could involve integrating the computation into existing verification software for timed systems.

Load-bearing premise

The digital clocks abstraction and associated algorithms for probabilistic timed automata extend directly to the multi-player turn-based game setting while preserving correctness of the computed probability and expected price values.

What would settle it

A concrete turn-based probabilistic timed game example where the probability or expected price computed after the digital clocks abstraction differs from the value obtained in the original continuous-time model.

Figures

Figures reproduced from arXiv: 1906.09142 by David Parker, Gethin Norman, Marta Kwiatkowska.

**Figure 1.** Figure 1: An example TPTG satisfied and action a can be performed only if the enabling condition is satisfied. If action a is taken in location l, then the probability of moving to location l 0 and resetting the set of clocks X equals prob(l, a)(X, l0 ). TPTGs have both location prices, which are accumulated at rate rL(l) when time passes in location l, and action prices, where rAct(l, a) is accumulated when perform… view at source ↗

**Figure 2.** Figure 2: PTAs used to model the non-repudiation protocol Randomisation is fundamental to the protocol as, in the initialisation step, O randomly selects a positive integer N that is never revealed to R during execution. Timing is also fundamental as, to prevent R potentially gaining an advantage, if O does not receive an acknowledgement within a specific timeout value (denoted AD), the protocol is stopped and O st… view at source ↗

**Figure 3.** Figure 3: Max. probability the protocol terminates successfully by time T (honest version) [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

**Figure 4.** Figure 4: Min. expected time until the protocol terminates successfully (honest version) For the ‘honest’ version, Figures 3 and 4 present results when different coalitions try to maximise the probability the protocol terminates successfully by time T when p=0.01 and p=0.1 and minimise expected time for successful termination as the parameter p varies. More precisely, we consider the coalition of both players (hhO… view at source ↗

**Figure 5.** Figure 5: Maximum probability R gains information by time T (malicious version 1) [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗

**Figure 6.** Figure 6: Maximum probability R gains information by time T (malicious version 2) – Time and energy usage of P2: [0, 5] picoseconds for addition, [0, 7] picoseconds multiplication, 20 Watts when idle and 30 Watts when active. A (non-probabilistic) TA model is considered in [12], which is the parallel composition of a TA for each processor and for the scheduler. Previously, in [45], we extended this model by adding … view at source ↗

**Figure 7.** Figure 7: Task graph for computing D×(C×(A+B))+((A+B)+(C×D)) Processors 4 p1_done p1_done p1_add p1_mult x:=0 x:=0 add x≤2 stby true mult x≤3 (a) Processor P1 Processors 4 add x≤2 p1_add p1_mult x:=0 x:=0 1-p x:=0 p p1_fail stby true mult x≤3 m_fail x=0 p1_done 1-p x:=0 p faults<k1 faults++ a_fail x=0 p1_fail p1_done faults<k1 faults++ (b) Faulty version of processor P1 [PITH_FULL_IMAGE:figures/full_fig_p013_7.png] view at source ↗

**Figure 8.** Figure 8: PTAs for the task-graph scheduling case study true. To specify the automaton for the scheduler and ensure that we can then build a turn-based game, we restrict the scheduler so that it decides what tasks to schedule initially and immediately after a task ends, then passes control to the environment, which decides the time for the next active task to end. In [PITH_FULL_IMAGE:figures/full_fig_p013_8.png] view at source ↗

**Figure 9.** Figure 9: Minimum expected time and energy to complete all tasks (k2=k1) properties. We have demonstrated the feasibility of the approach through two case studies. However, there are limitations of the method since, in particular, as for PTAs [38], the digital clocks semantics does not preserve stopwatch properties or general (nested) temporal logic specifications. We are investigating extending the approach to conc… view at source ↗

read the original abstract

Quantitative verification techniques have been developed for the formal analysis of a variety of probabilistic models, such as Markov chains, Markov decision process and their variants. They can be used to produce guarantees on quantitative aspects of system behaviour, for example safety, reliability and performance, or to help synthesise controllers that ensure such guarantees are met. We propose the model of turn-based probabilistic timed multi-player games, which incorporates probabilistic choice, real-time clocks and nondeterministic behaviour across multiple players. Building on the digital clocks approach for the simpler model of probabilistic timed automata, we show how to compute the key measures that underlie quantitative verification, namely the probability and expected cumulative price to reach a target. We illustrate this on case studies from computer security and task scheduling.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper lifts the digital-clocks reduction from probabilistic timed automata to turn-based multi-player games while keeping the reachability probabilities and expected prices intact under optimal play.

read the letter

The core contribution is a model of turn-based probabilistic timed multi-player games plus a direct reduction to finite-state turn-based games via digital clocks. This lets them compute the probability and expected cumulative price to reach a target. The reduction preserves the turn-based structure and the quantitative measures, which is the part that actually matters for verification and control. They demonstrate it on security and scheduling examples, which helps show the model is usable rather than purely theoretical. The construction appears to be a straightforward product-style extension that does not introduce new interactions between player choices and clock discretization that would break the abstraction. No load-bearing gaps show up in the argument as described. The main soft spot is the lack of fresh complexity bounds or scaling data; it inherits the state-space growth from the PTA case, and with more players that could become expensive quickly. There is also no discussion of how the method behaves when clock constraints are not integer or when the number of players increases beyond two. This work is aimed at people already inside probabilistic model checking who need to add real-time and adversarial elements. A reader who knows the PTA digital-clocks papers will see the incremental step clearly and can check the reduction themselves. It is worth sending to peer review because the claim is concrete and falsifiable through the reduction, even if the paper stays within the existing formal-methods toolkit rather than opening new territory.

Referee Report

0 major / 2 minor

Summary. The paper introduces the model of turn-based probabilistic timed multi-player games, which combine probabilistic choice, real-time clocks, and nondeterministic multi-player behavior. Building on the digital clocks abstraction previously developed for probabilistic timed automata, the authors present a reduction that computes the probability and expected cumulative price of reaching a target under optimal play, and illustrate the approach on case studies from computer security and task scheduling.

Significance. If the reduction is correct, the work extends quantitative verification to a new class of models that incorporate real-time constraints, probability, and turn-based multi-player interactions while preserving the computed reachability probabilities and expected prices. The presentation of the construction as a direct, correctness-preserving algorithmic reduction that maintains the turn-based structure is a strength; the case studies provide concrete evidence of applicability.

minor comments (2)

[Abstract] Abstract: the claim that the digital clocks approach 'extends' to the game setting would benefit from a one-sentence indication of the key property preserved (e.g., that optimal values remain unchanged under the discretization).
The notation for player strategies and the turn-based scheduler could be introduced with an explicit example in the preliminaries to aid readability for readers unfamiliar with multi-player game semantics.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper, recognition of its significance in extending quantitative verification to turn-based probabilistic timed multi-player games, and recommendation of minor revision. No major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents a direct algorithmic reduction extending the digital clocks abstraction from probabilistic timed automata to turn-based probabilistic timed multi-player games, preserving reachability probabilities and expected prices under optimal play. No equations, fitted parameters, self-definitional constructs, or load-bearing self-citations that reduce the central claim to its own inputs appear in the derivation. The contribution is an independent correctness-preserving construction on the turn-based structure and quantitative measures, making the result self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Only the abstract is available; the ledger therefore records the minimal background assumptions visible in the text.

axioms (1)

domain assumption Digital clocks abstraction preserves reachability probabilities and expected prices for probabilistic timed automata
The paper states it builds directly on this existing technique for the new game model.

pith-pipeline@v0.9.0 · 5648 in / 1146 out tokens · 26578 ms · 2026-05-25T18:22:51.555116+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Building on the digital clocks approach for probabilistic timed automata, we show how to compute the probability and expected cumulative price to reach a target in turn-based probabilistic timed multi-player games.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We prove the correspondence between these two semantics [dense-time vs. digital clocks].

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

65 extracted references · 65 canonical work pages

[1]

In: Proc

de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga., M.: The element of surprise in timed games. In: Proc. CONCUR’03, LNCS 2761. Springer (2003)

work page 2003
[2]

In: Proc

Aljazzar, H., Fischer, M., Grunske, L., Kuntz, M., Leitner, F., Leue, S.: Safety analysis of an airbag system using probabilistic FMEA and probabilistic counter examples. In: Proc. QEST’09. IEEE (2009)

work page 2009
[3]

In: Proc

Alur, R., Mikhail, B., Madhusudan, P.: Optimal reachability for weighted timed games. In: Proc. ICALP’04, LNCS 3142. Springer (2004)

work page 2004
[4]

Entropy 20(5) (2018) Veriﬁcation and Control of Turn-Based Probabilistic Real-Time Games 15

Alvim, M., Chatzikokolakis, K., Kawamoto, Y., Palamidessi, C.: A game-theoretic approach to information-ﬂow control via protocol composition. Entropy 20(5) (2018) Veriﬁcation and Control of Turn-Based Probabilistic Real-Time Games 15

work page 2018
[5]

In: Proc

Alvim, M., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proc. CSF’12. IEEE (2012)

work page 2012
[6]

In: Proc

Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed au- tomata. In: Proc. SSC’98. Elsevier (1998)

work page 1998
[7]

CACM 53(9) (2010)

Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. CACM 53(9) (2010)

work page 2010
[8]

Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K., Lime, D.: UPPAAL-Tiga: Time for playing games! In: Proc. CAV’07. Springer (2007)

work page 2007
[9]

In: Proc

Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Proc. HSCC’01, LNCS 2034. Springer (2001)

work page 2034
[10]

IPL 98 (2006)

Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. IPL 98 (2006)

work page 2006
[11]

In: Proc

Bouyer, P., Cassez, F., Fleury, E., Larsen, K.: Optimal strategies in priced timed game automata. In: Proc. FSTTCS’04, LNCS 3328. Springer (2004)

work page 2004
[12]

Bouyer, P., Fahrenberg, U., Larsen, K., Markey, N.: Quantitative analysis of real- time systems using priced timed automata. Comm. ACM 54(9) (2011)

work page 2011
[13]

In: Proc

Bouyer, P., Forejt, V.: Reachability in stochastic timed games. In: Proc. ICALP’09, LNCS 5556. Springer (2009)

work page 2009
[14]

Acta Informatica 55(2) (2018)

Bouyer, P., Markey, N., Randour, M., Larsen, K., Laursen, S.: Average-energy games. Acta Informatica 55(2) (2018)

work page 2018
[15]

In: Proc

Br´ azdil, T., Hermanns, H., Krc´ al, J., Kret´ ınsk´ y, J., Reh´ ak, V.: Veriﬁcation of open interactive Markov chains. In: Proc. FSTTCS’12, LIPIcs 18 (2012)

work page 2012
[16]

In: Proc

Br´ azdil, T., Krc´ al, J., Kret´ ınsk´ y, J., Kucera, A., Reh´ ak, V.: Stochastic real-time games with qualitative timed automata objectives. In: Proc. CONCUR’10 (2010)

work page 2010
[17]

In: Proc

Brihaye, T., Bruy` ere, V., Raskin, J.: On optimal timed strategies. In: Proc. FOR- MATS’05, LNCS 3829. Springer (2005)

work page 2005
[18]

In: Proc

Cassez, F., David, A., Larsen, K., Lime, D., Raskin, J.F.: Timed control with observation based and stuttering invariant strategies. In: Proc. ATVA’07 (2007)

work page 2007
[19]

In: Proc

Cassez, F., David, D., Fleury, E., Larsen, K., Lime, D.: Eﬃcient on-the-ﬂy al- gorithms for the analysis of timed games. In: Proc. CONCUR’05, LNCS 3653. Springer (2005)

work page 2005
[20]

Advances in computational complexity theory, DIMACS Series in DMTCS 13 (1993)

Condon, A.: On algorithms for simple stochastic games. Advances in computational complexity theory, DIMACS Series in DMTCS 13 (1993)

work page 1993
[21]

In: Proc

Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: A modern probabilistic model checker. In: Proc. CAV’17, LNCS 10427. Springer (2017)

work page 2017
[22]

Springer (1997)

Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer (1997)

work page 1997
[23]

In: Proc

Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. In: Proc. FORMATS’10, LNCS 6246. Springer (2010)

work page 2010
[24]

TCS 631 (2016)

Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. TCS 631 (2016)

work page 2016
[25]

Henzinger, T.: The temporal speciﬁcation and veriﬁcation of real-time systems. Ph.D. thesis, Stanford University (1991)

work page 1991
[26]

ICALP’92, LNCS 623

Henzinger, T., Manna, Z., Pnueli, A.: What good are digital clocks? In: Proc. ICALP’92, LNCS 623. Springer (1992)

work page 1992
[27]

LNCS 2428

Hermanns, H.: Interactive Markov Chains and the Quest for Quantiﬁed Quality. LNCS 2428. Springer (2002)

work page 2002
[28]

Research In Economics 57(3) (2003) 16 Marta Kwiatkowska, Gethin Norman, and David Parker

van der Hoek, W., Wooldridge, M.: Model checking cooperation, knowledge, and time - A case study. Research In Economics 57(3) (2003) 16 Marta Kwiatkowska, Gethin Norman, and David Parker

work page 2003
[29]

TCS 669 (2017)

Jovanovic, A., Kwiatkowska, M., Norman, G., Peyras, Q.: Symbolic optimal ex- pected time reachability computation and controller synthesis for probabilistic timed automata. TCS 669 (2017)

work page 2017
[30]

In: Proc

Jurdzi´ nski, M., Kwiatkowska, M., Norman, G., Trivedi, A.: Concavely-priced prob- abilistic timed automata. In: Proc. CONCUR’09, LNCS 5710. Springer (2009)

work page 2009
[31]

Springer (1976)

Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer (1976)

work page 1976
[32]

Master’s thesis, School of Informatics, Masaryk University, Brno (2009)

Krˇ c´ al, J.: Determinacy and optimal strategies in stochastic games. Master’s thesis, School of Informatics, Masaryk University, Brno (2009)

work page 2009
[33]

In: Proc

Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for veriﬁcation of probabilistic timed automata. In: Proc. FORMATS’09. Springer (2009)

work page 2009
[34]

In: Proc

Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Veriﬁcation of probabilistic real-time systems. In: Proc. CAV’11, LNCS 6806. Springer (2011)

work page 2011
[35]

In: Models, Algorithms, Logics and Tools, LNCS 10460

Kwiatkowska, M., Norman, G., Parker, D.: Symbolic veriﬁcation and strategy syn- thesis for linearly-priced probabilistic timed automata. In: Models, Algorithms, Logics and Tools, LNCS 10460. Springer (2017)

work page 2017
[36]

In: Proc

Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automated veriﬁcation of concurrent stochastic games. In: Proc. QEST’18, LNCS 11024. Springer (2018)

work page 2018
[37]

In: Proc

Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Equilibria-based proba- bilistic model checking for concurrent stochastic games. In: Proc. FM’19, LNCS. Springer (2019). To appear

work page 2019
[38]

FMSD 29 (2006)

Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. FMSD 29 (2006)

work page 2006
[39]

TCS 282 (2002)

Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic veriﬁcation of real-time systems with discrete probability distributions. TCS 282 (2002)

work page 2002
[40]

IC 205(7) (2007)

Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. IC 205(7) (2007)

work page 2007
[41]

STTT 20(2) (2018)

Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: Veriﬁcation and strat- egy synthesis for stochastic multi-player games with multiple objectives. STTT 20(2) (2018)

work page 2018
[42]

In: Proc

Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Automatic analysis of a non- repudiation protocol. In: Proc. QAPL’04, ENTCS 112 (2005)

work page 2005
[43]

In: Proc

Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Proc. STACS’95, LNCS 900. Springer (1995)

work page 1995
[44]

In: Proc

Markowitch, O., Roggeman, Y.: Probabilistic non-repudiation without trusted third party. In: Proc. Workshop Security in Communication Networks (1999)

work page 1999
[45]

FMSD 43(2) (2013)

Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed au- tomata. FMSD 43(2) (2013)

work page 2013
[46]

RTS 53(3) (2017)

Norman, G., Parker, D., Zou, X.: Veriﬁcation and control of partially observable probabilistic systems. RTS 53(3) (2017)

work page 2017
[47]

In: Proc

Oualhadj, Y., Reynier, P.A., Sankur, O.: Probabilistic robust timed games. In: Proc. CONCUR’14, LNCS 8704. Springer (2014)

work page 2014
[48]

McGraw-Hill (1976)

Rudin, W.: Principles of Mathematical Analysis, 3rd edn. McGraw-Hill (1976)

work page 1976
[49]

La Torre, S., Mukhopadhyay, S., Murano, A.: Optimal-reachability and control for acyclic weighted timed automata

S. La Torre, S., Mukhopadhyay, S., Murano, A.: Optimal-reachability and control for acyclic weighted timed automata. In: Proc. TCS’02. Kluwer (2002)

work page 2002
[50]

Schrijver, A.: Theory of Linear and Integer Programming. J. Wiley and Sons (1986)

work page 1986
[51]

In: Proc

Tripakis, S.: Verifying progress in timed systems. In: Proc. ARTS’99, LNCS 1601. Springer (1999)

work page 1999
[52]

In: Proc

Tripakis, S., Altisen, K.: On-the-ﬂy controller synthesis for discrete and dense-time systems. In: Proc. FM’99, LNCS 1708. Springer (1999)

work page 1999
[53]

FMSD 26(3) (2005)

Tripakis, S., Yovine, S., Bouajjan, A.: Checking timed B¨ uchi automata emptiness eﬃciently. FMSD 26(3) (2005)

work page 2005
[54]

Supporting material. www.prismmodelchecker.org/ﬁles/tptgs/ Veriﬁcation and Control of Turn-Based Probabilistic Real-Time Games 17 A Proofs from Section 4 In this appendix we include the details omitted from Section 4 as they closely follow those for PTAs presented in [38]. As in Section 4, we ﬁx a TPTG P, coalition of players C and target set of locations...

work page
[55]

We can construction the strategy proﬁle σ=(σ1,σ 2) of [ [P] ]C R where the strategies σ1 and σ2 make the same choices as those of σ′ 1 and σ′ 2 respectively

of [ [P] ]C N . We can construction the strategy proﬁle σ=(σ1,σ 2) of [ [P] ]C R where the strategies σ1 and σ2 make the same choices as those of σ′ 1 and σ′ 2 respectively. The only diﬀerence is in the states reached as values of a clocks in [ [P] ]R are not bounded. It then follows that Pσ(FR) = Pσ′ (FN) and Eσ(FR) = Eσ′ (FN) as required. ⊓ ⊔ We now pre...

work page
[56]

of [ [P] ]C N is deﬁned as follows. For any ﬁnite path π of [ [P] ]C N and 1⩽i⩽2 such that last (π)∈Si : – if [π]−1 ε is non-empty, then for any (t,a )∈ A(last(π)), then the probability of σε i choosing (t,a ) after π has been performed is given by σε i (π)(t,a ) = Probσ([π t,a −−→]−1 ε ) Probσ([π]−1 ε ) – if [π]−1 ε is the empty set, then letσε i choose ...

work page
[57]

Now, from the construction of Probσε , see [31], it is suﬃcient to show that: Probσε (π) = Probσ([π]−1 ε ) for all π∈ FPathsσε (1) which we prove by induction on the length of π

of [ [P] ]C N . Now, from the construction of Probσε , see [31], it is suﬃcient to show that: Probσε (π) = Probσ([π]−1 ε ) for all π∈ FPathsσε (1) which we prove by induction on the length of π. Therefore, consider any path π∈ IPathsσε . If|π|=0, thenπ=¯s and Probσε (π) = 1 = Probσ([π]−1 ε ) as required. Next, suppose |π|=n+1 and by induction the lemma ho...

work page
[58]

Combining (3) with (2) it follows that: Pσ(FR) = Probσ{π∈ IPathsσ′ |π(i)∈F for some i∈ N} = Pσ′ (FN) by deﬁnition of Pσ′ (FN)

of [ [P] ]C N using Proposition 3. Combining (3) with (2) it follows that: Pσ(FR) = Probσ{π∈ IPathsσ′ |π(i)∈F for some i∈ N} = Pσ′ (FN) by deﬁnition of Pσ′ (FN). Since the player 2 strategy σ2 was arbitrary it follows that: infσ2∈Σ2 [ [P] ]C R Pσ1,σ2(FR) ⩾ infσ′ 2∈Σ2 [ [P] ]C N Pσ′ 1,σ′ 2(FN). Following dual arguments and using Proposition 2 we have: infσ...

work page
[59]

A is totally unimodular; 20 Marta Kwiatkowska, Gethin Norman, and David Parker

work page
[60]

Theorem 4 ([50] Corollary 19.1.a)

each collection of columns of A can be split into two parts so that the sum of the columns in one part minus the sum of the columns in the other part is a vector with entries only 0, +1 and−1. Theorem 4 ([50] Corollary 19.1.a). Let A be a totally unimodular matrix, and let b and c be integral vectors. Then both problems in the linear programming duality e...

work page
[61]

The set of ﬁnite paths of the proﬁle ( σt 1,σ t

which match the action choices of the proﬁle σ, although the durations may diﬀer. The set of ﬁnite paths of the proﬁle ( σt 1,σ t

work page
[62]

The construction all ﬁnite paths of the proﬁle ( σt 1,σ t

when starting from the initial state is given by {[π]t|π∈ FPathsσ1,σ2}, which we deﬁne inductively as follows: – if π = (l, 0), then [π]t =π; – if π is of the form π′ t,a −−→(l,v ), then: [π]t def = [ π′]t t′,a −−→(l,v′) wheret′ =tπ−tπ′ and for any clock x we havev′(x) =tπ−tπ(j) forj ⩽|π| such that v(x) = dur(π,|π|)− dur(π,j ), which exists by Lemma 4. Th...

work page
[63]

yields also the choices made by the proﬁle and by construction the action choices match those of the proﬁleσ although the durations may diﬀer. The fact that these choices are valid choices of [ [P] ]C R follows from Lemma 4, equations (4a)–(4d) and since we restrict attention to closed, diagonal-free probabilistic timed games (Assumption 1). For any state...

work page
[64]

and Deﬁnition 6 and Deﬁnition 12, it follows that Eσt 1,σt 2 n (FR) equals: ∑ π∈FPathsσ∧|π|⩽n ∧∀i⩽|π|.π (i)̸∈FR Probσt 1,σt 2(π)· (tπ−tπ|π|−1)·rL(last(π)) + Aσt 1,σt 2 n (FR) = ∑ π∈FPathsσ∧|π|⩽n ∧∀i⩽|π|.π (i)̸∈FR Probσ(π)· (tπ−tπ|π|−1)·rL(last(π)) + Aσ n(FR) (5) since the action choices of σ and (σt 1,σ t

work page
[65]

are the same. Now suppose we ﬁx some n∈ N and consider the following linear program- ming problem over the variables⟨tπ⟩π∈FPathsσ n, where FPathsσ n is subset of paths of FPathsσ with length at most n: maximise (5) such that the constraints of (4a)–(4d) are satisﬁed. From Assumption 1 we have that all probabilities are rational, and therefore we can scale...

work page

[1] [1]

In: Proc

de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga., M.: The element of surprise in timed games. In: Proc. CONCUR’03, LNCS 2761. Springer (2003)

work page 2003

[2] [2]

In: Proc

Aljazzar, H., Fischer, M., Grunske, L., Kuntz, M., Leitner, F., Leue, S.: Safety analysis of an airbag system using probabilistic FMEA and probabilistic counter examples. In: Proc. QEST’09. IEEE (2009)

work page 2009

[3] [3]

In: Proc

Alur, R., Mikhail, B., Madhusudan, P.: Optimal reachability for weighted timed games. In: Proc. ICALP’04, LNCS 3142. Springer (2004)

work page 2004

[4] [4]

Entropy 20(5) (2018) Veriﬁcation and Control of Turn-Based Probabilistic Real-Time Games 15

Alvim, M., Chatzikokolakis, K., Kawamoto, Y., Palamidessi, C.: A game-theoretic approach to information-ﬂow control via protocol composition. Entropy 20(5) (2018) Veriﬁcation and Control of Turn-Based Probabilistic Real-Time Games 15

work page 2018

[5] [5]

In: Proc

Alvim, M., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proc. CSF’12. IEEE (2012)

work page 2012

[6] [6]

In: Proc

Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed au- tomata. In: Proc. SSC’98. Elsevier (1998)

work page 1998

[7] [7]

CACM 53(9) (2010)

Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. CACM 53(9) (2010)

work page 2010

[8] [8]

Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K., Lime, D.: UPPAAL-Tiga: Time for playing games! In: Proc. CAV’07. Springer (2007)

work page 2007

[9] [9]

In: Proc

Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Proc. HSCC’01, LNCS 2034. Springer (2001)

work page 2034

[10] [10]

IPL 98 (2006)

Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. IPL 98 (2006)

work page 2006

[11] [11]

In: Proc

Bouyer, P., Cassez, F., Fleury, E., Larsen, K.: Optimal strategies in priced timed game automata. In: Proc. FSTTCS’04, LNCS 3328. Springer (2004)

work page 2004

[12] [12]

Bouyer, P., Fahrenberg, U., Larsen, K., Markey, N.: Quantitative analysis of real- time systems using priced timed automata. Comm. ACM 54(9) (2011)

work page 2011

[13] [13]

In: Proc

Bouyer, P., Forejt, V.: Reachability in stochastic timed games. In: Proc. ICALP’09, LNCS 5556. Springer (2009)

work page 2009

[14] [14]

Acta Informatica 55(2) (2018)

Bouyer, P., Markey, N., Randour, M., Larsen, K., Laursen, S.: Average-energy games. Acta Informatica 55(2) (2018)

work page 2018

[15] [15]

In: Proc

Br´ azdil, T., Hermanns, H., Krc´ al, J., Kret´ ınsk´ y, J., Reh´ ak, V.: Veriﬁcation of open interactive Markov chains. In: Proc. FSTTCS’12, LIPIcs 18 (2012)

work page 2012

[16] [16]

In: Proc

Br´ azdil, T., Krc´ al, J., Kret´ ınsk´ y, J., Kucera, A., Reh´ ak, V.: Stochastic real-time games with qualitative timed automata objectives. In: Proc. CONCUR’10 (2010)

work page 2010

[17] [17]

In: Proc

Brihaye, T., Bruy` ere, V., Raskin, J.: On optimal timed strategies. In: Proc. FOR- MATS’05, LNCS 3829. Springer (2005)

work page 2005

[18] [18]

In: Proc

Cassez, F., David, A., Larsen, K., Lime, D., Raskin, J.F.: Timed control with observation based and stuttering invariant strategies. In: Proc. ATVA’07 (2007)

work page 2007

[19] [19]

In: Proc

Cassez, F., David, D., Fleury, E., Larsen, K., Lime, D.: Eﬃcient on-the-ﬂy al- gorithms for the analysis of timed games. In: Proc. CONCUR’05, LNCS 3653. Springer (2005)

work page 2005

[20] [20]

Advances in computational complexity theory, DIMACS Series in DMTCS 13 (1993)

Condon, A.: On algorithms for simple stochastic games. Advances in computational complexity theory, DIMACS Series in DMTCS 13 (1993)

work page 1993

[21] [21]

In: Proc

Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: A modern probabilistic model checker. In: Proc. CAV’17, LNCS 10427. Springer (2017)

work page 2017

[22] [22]

Springer (1997)

Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer (1997)

work page 1997

[23] [23]

In: Proc

Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. In: Proc. FORMATS’10, LNCS 6246. Springer (2010)

work page 2010

[24] [24]

TCS 631 (2016)

Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. TCS 631 (2016)

work page 2016

[25] [25]

Henzinger, T.: The temporal speciﬁcation and veriﬁcation of real-time systems. Ph.D. thesis, Stanford University (1991)

work page 1991

[26] [26]

ICALP’92, LNCS 623

Henzinger, T., Manna, Z., Pnueli, A.: What good are digital clocks? In: Proc. ICALP’92, LNCS 623. Springer (1992)

work page 1992

[27] [27]

LNCS 2428

Hermanns, H.: Interactive Markov Chains and the Quest for Quantiﬁed Quality. LNCS 2428. Springer (2002)

work page 2002

[28] [28]

Research In Economics 57(3) (2003) 16 Marta Kwiatkowska, Gethin Norman, and David Parker

van der Hoek, W., Wooldridge, M.: Model checking cooperation, knowledge, and time - A case study. Research In Economics 57(3) (2003) 16 Marta Kwiatkowska, Gethin Norman, and David Parker

work page 2003

[29] [29]

TCS 669 (2017)

Jovanovic, A., Kwiatkowska, M., Norman, G., Peyras, Q.: Symbolic optimal ex- pected time reachability computation and controller synthesis for probabilistic timed automata. TCS 669 (2017)

work page 2017

[30] [30]

In: Proc

Jurdzi´ nski, M., Kwiatkowska, M., Norman, G., Trivedi, A.: Concavely-priced prob- abilistic timed automata. In: Proc. CONCUR’09, LNCS 5710. Springer (2009)

work page 2009

[31] [31]

Springer (1976)

Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer (1976)

work page 1976

[32] [32]

Master’s thesis, School of Informatics, Masaryk University, Brno (2009)

Krˇ c´ al, J.: Determinacy and optimal strategies in stochastic games. Master’s thesis, School of Informatics, Masaryk University, Brno (2009)

work page 2009

[33] [33]

In: Proc

Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for veriﬁcation of probabilistic timed automata. In: Proc. FORMATS’09. Springer (2009)

work page 2009

[34] [34]

In: Proc

Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Veriﬁcation of probabilistic real-time systems. In: Proc. CAV’11, LNCS 6806. Springer (2011)

work page 2011

[35] [35]

In: Models, Algorithms, Logics and Tools, LNCS 10460

Kwiatkowska, M., Norman, G., Parker, D.: Symbolic veriﬁcation and strategy syn- thesis for linearly-priced probabilistic timed automata. In: Models, Algorithms, Logics and Tools, LNCS 10460. Springer (2017)

work page 2017

[36] [36]

In: Proc

Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automated veriﬁcation of concurrent stochastic games. In: Proc. QEST’18, LNCS 11024. Springer (2018)

work page 2018

[37] [37]

In: Proc

Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Equilibria-based proba- bilistic model checking for concurrent stochastic games. In: Proc. FM’19, LNCS. Springer (2019). To appear

work page 2019

[38] [38]

FMSD 29 (2006)

Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. FMSD 29 (2006)

work page 2006

[39] [39]

TCS 282 (2002)

Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic veriﬁcation of real-time systems with discrete probability distributions. TCS 282 (2002)

work page 2002

[40] [40]

IC 205(7) (2007)

Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. IC 205(7) (2007)

work page 2007

[41] [41]

STTT 20(2) (2018)

Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: Veriﬁcation and strat- egy synthesis for stochastic multi-player games with multiple objectives. STTT 20(2) (2018)

work page 2018

[42] [42]

In: Proc

Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Automatic analysis of a non- repudiation protocol. In: Proc. QAPL’04, ENTCS 112 (2005)

work page 2005

[43] [43]

In: Proc

Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Proc. STACS’95, LNCS 900. Springer (1995)

work page 1995

[44] [44]

In: Proc

Markowitch, O., Roggeman, Y.: Probabilistic non-repudiation without trusted third party. In: Proc. Workshop Security in Communication Networks (1999)

work page 1999

[45] [45]

FMSD 43(2) (2013)

Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed au- tomata. FMSD 43(2) (2013)

work page 2013

[46] [46]

RTS 53(3) (2017)

Norman, G., Parker, D., Zou, X.: Veriﬁcation and control of partially observable probabilistic systems. RTS 53(3) (2017)

work page 2017

[47] [47]

In: Proc

Oualhadj, Y., Reynier, P.A., Sankur, O.: Probabilistic robust timed games. In: Proc. CONCUR’14, LNCS 8704. Springer (2014)

work page 2014

[48] [48]

McGraw-Hill (1976)

Rudin, W.: Principles of Mathematical Analysis, 3rd edn. McGraw-Hill (1976)

work page 1976

[49] [49]

La Torre, S., Mukhopadhyay, S., Murano, A.: Optimal-reachability and control for acyclic weighted timed automata

S. La Torre, S., Mukhopadhyay, S., Murano, A.: Optimal-reachability and control for acyclic weighted timed automata. In: Proc. TCS’02. Kluwer (2002)

work page 2002

[50] [50]

Schrijver, A.: Theory of Linear and Integer Programming. J. Wiley and Sons (1986)

work page 1986

[51] [51]

In: Proc

Tripakis, S.: Verifying progress in timed systems. In: Proc. ARTS’99, LNCS 1601. Springer (1999)

work page 1999

[52] [52]

In: Proc

Tripakis, S., Altisen, K.: On-the-ﬂy controller synthesis for discrete and dense-time systems. In: Proc. FM’99, LNCS 1708. Springer (1999)

work page 1999

[53] [53]

FMSD 26(3) (2005)

Tripakis, S., Yovine, S., Bouajjan, A.: Checking timed B¨ uchi automata emptiness eﬃciently. FMSD 26(3) (2005)

work page 2005

[54] [54]

Supporting material. www.prismmodelchecker.org/ﬁles/tptgs/ Veriﬁcation and Control of Turn-Based Probabilistic Real-Time Games 17 A Proofs from Section 4 In this appendix we include the details omitted from Section 4 as they closely follow those for PTAs presented in [38]. As in Section 4, we ﬁx a TPTG P, coalition of players C and target set of locations...

work page

[55] [55]

We can construction the strategy proﬁle σ=(σ1,σ 2) of [ [P] ]C R where the strategies σ1 and σ2 make the same choices as those of σ′ 1 and σ′ 2 respectively

of [ [P] ]C N . We can construction the strategy proﬁle σ=(σ1,σ 2) of [ [P] ]C R where the strategies σ1 and σ2 make the same choices as those of σ′ 1 and σ′ 2 respectively. The only diﬀerence is in the states reached as values of a clocks in [ [P] ]R are not bounded. It then follows that Pσ(FR) = Pσ′ (FN) and Eσ(FR) = Eσ′ (FN) as required. ⊓ ⊔ We now pre...

work page

[56] [56]

of [ [P] ]C N is deﬁned as follows. For any ﬁnite path π of [ [P] ]C N and 1⩽i⩽2 such that last (π)∈Si : – if [π]−1 ε is non-empty, then for any (t,a )∈ A(last(π)), then the probability of σε i choosing (t,a ) after π has been performed is given by σε i (π)(t,a ) = Probσ([π t,a −−→]−1 ε ) Probσ([π]−1 ε ) – if [π]−1 ε is the empty set, then letσε i choose ...

work page

[57] [57]

Now, from the construction of Probσε , see [31], it is suﬃcient to show that: Probσε (π) = Probσ([π]−1 ε ) for all π∈ FPathsσε (1) which we prove by induction on the length of π

of [ [P] ]C N . Now, from the construction of Probσε , see [31], it is suﬃcient to show that: Probσε (π) = Probσ([π]−1 ε ) for all π∈ FPathsσε (1) which we prove by induction on the length of π. Therefore, consider any path π∈ IPathsσε . If|π|=0, thenπ=¯s and Probσε (π) = 1 = Probσ([π]−1 ε ) as required. Next, suppose |π|=n+1 and by induction the lemma ho...

work page

[58] [58]

Combining (3) with (2) it follows that: Pσ(FR) = Probσ{π∈ IPathsσ′ |π(i)∈F for some i∈ N} = Pσ′ (FN) by deﬁnition of Pσ′ (FN)

of [ [P] ]C N using Proposition 3. Combining (3) with (2) it follows that: Pσ(FR) = Probσ{π∈ IPathsσ′ |π(i)∈F for some i∈ N} = Pσ′ (FN) by deﬁnition of Pσ′ (FN). Since the player 2 strategy σ2 was arbitrary it follows that: infσ2∈Σ2 [ [P] ]C R Pσ1,σ2(FR) ⩾ infσ′ 2∈Σ2 [ [P] ]C N Pσ′ 1,σ′ 2(FN). Following dual arguments and using Proposition 2 we have: infσ...

work page

[59] [59]

A is totally unimodular; 20 Marta Kwiatkowska, Gethin Norman, and David Parker

work page

[60] [60]

Theorem 4 ([50] Corollary 19.1.a)

each collection of columns of A can be split into two parts so that the sum of the columns in one part minus the sum of the columns in the other part is a vector with entries only 0, +1 and−1. Theorem 4 ([50] Corollary 19.1.a). Let A be a totally unimodular matrix, and let b and c be integral vectors. Then both problems in the linear programming duality e...

work page

[61] [61]

The set of ﬁnite paths of the proﬁle ( σt 1,σ t

which match the action choices of the proﬁle σ, although the durations may diﬀer. The set of ﬁnite paths of the proﬁle ( σt 1,σ t

work page

[62] [62]

The construction all ﬁnite paths of the proﬁle ( σt 1,σ t

when starting from the initial state is given by {[π]t|π∈ FPathsσ1,σ2}, which we deﬁne inductively as follows: – if π = (l, 0), then [π]t =π; – if π is of the form π′ t,a −−→(l,v ), then: [π]t def = [ π′]t t′,a −−→(l,v′) wheret′ =tπ−tπ′ and for any clock x we havev′(x) =tπ−tπ(j) forj ⩽|π| such that v(x) = dur(π,|π|)− dur(π,j ), which exists by Lemma 4. Th...

work page

[63] [63]

yields also the choices made by the proﬁle and by construction the action choices match those of the proﬁleσ although the durations may diﬀer. The fact that these choices are valid choices of [ [P] ]C R follows from Lemma 4, equations (4a)–(4d) and since we restrict attention to closed, diagonal-free probabilistic timed games (Assumption 1). For any state...

work page

[64] [64]

and Deﬁnition 6 and Deﬁnition 12, it follows that Eσt 1,σt 2 n (FR) equals: ∑ π∈FPathsσ∧|π|⩽n ∧∀i⩽|π|.π (i)̸∈FR Probσt 1,σt 2(π)· (tπ−tπ|π|−1)·rL(last(π)) + Aσt 1,σt 2 n (FR) = ∑ π∈FPathsσ∧|π|⩽n ∧∀i⩽|π|.π (i)̸∈FR Probσ(π)· (tπ−tπ|π|−1)·rL(last(π)) + Aσ n(FR) (5) since the action choices of σ and (σt 1,σ t

work page

[65] [65]

are the same. Now suppose we ﬁx some n∈ N and consider the following linear program- ming problem over the variables⟨tπ⟩π∈FPathsσ n, where FPathsσ n is subset of paths of FPathsσ with length at most n: maximise (5) such that the constraints of (4a)–(4d) are satisﬁed. From Assumption 1 we have that all probabilities are rational, and therefore we can scale...

work page