This case study concerns the problem of scheduling tasks between several processors.

The models here are partially observable probabilistic timed automata (POPTAs),
as described in [NPZ17]. These extend the the probabilistic timed automaton (PTA)
version from [NPS13]. Both are extensions of the timed automaton example from [BFLM11].

For more information, see: http://www.prismmodelchecker.org/casestudies/task_graph.php

=====================================================================================

[BFLM11]
P. Bouyer, U. Fahrenberg, K. Larsen and N. Markey
Quantitative Analysis of Real-Time Systems Using Priced Timed Automata
Communications of the ACM, 54(9), pages 78-87, 2011

[KNP19]
Marta Kwiatkowska, Gethin Norman and David Parker
Verification and Control of Turn-Based Probabilistic Real-Time Games
In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy (Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday), volume 11760 of LNCS, pages 379-396, Springer, 2019

[NPS13]
Gethin Norman, David Parker and Jeremy Sproston
Model Checking for Probabilistic Timed Automata
Formal Methods in System Design, 43(2), pages 164-190, Springer, 2013

[NPZ17]
Gethin Norman, David Parker and Xueyi Zou
Verification and Control of Partially Observable Probabilistic Systems
Real-Time Systems, 53(3), pages 354-402, Springer, 2017