Uppaal Stratego combines various analysis techniques from different Uppaal branches and focuses on strategies. In particular Uppaal Stratego facilitates generation, optimization, comparison as well as consequence and performance exploration of strategies for stochastic priced timed games in a user-friendly manner. The tool allows for efficient and flexible “strategy-space” exploration before adaptation in a final implementation by maintaining strategies as first class objects in the model-checking query language.
A game is a mathematical model of a system consisting of several players (processes) which have independent objectives, often they are competing and sometimes oposing and even conflicting. To win a game the player needs to achieve the objective (goal). The simplest game consists of two players. Sometimes the game is symmetric (e.g. for reasons of fairness) where starting positions and objectives of the players are equivalent, but in general it does not need to be symmetric and most often it is not. Solving a game means finding a winning strategy leading to the goal or proving that the goal is not achievable. Games are interesting because game modeling is relatively easy (easier than proving theorems) and many mathematical proofs can be reduced to solving a game, therefore game solving tools help automate proving properties about a rich set of systems. Moreover, its diagnostic artefacts (strategies) can be used to generate controller algorithms, therefore effectively achieving correct-by-design controller synthesis.
A strategy is a prescription of one player's actions (transitions) for any possible situation (system state) eventually leading to achieving the player's goal. The winning strategy does not always exists. Deterministic strategy specifies a single action per state and non-deterministic strategy may specify several alternatives. Fully permissive strategy specifies all alternative actions leading to the goal.
Uppaal timed game is a two-player game specified by a network of timed automata with two types of edges: solid and dashed, corresponding to the player- and oponent-chosen transitions. Uppaal Tiga uses symbolic techniques to solve timed games with dense time.
A stochastic timed game is a probabilistic extension to a timed game.
A stochastic priced timed game is a further extention with continuous price expressions which allow estimating the distribution of cost in a timed game.
Below is an overview of various models and strategies and their relations in Uppaal Stratego, where solid arrows indicate transformation and computation and dashed arrows indicate reuse of the objects:
The top layer is dedicated to symbolic methods, such as solving a timed game G by computing a strategy σ, which can already be achieved by Uppaal Tiga. The novelty here is that the newly computed strategy σ is stored in the memory and the model G can repeatedly be evaluated under the σ strategy using queries applicable to (stochastic) timed automata G|σ.
The bottom layer is dedicated to simulation-based methods, such as statistical model checking and learning-based synthesis of extended stochastic models. The stochastic extensions are similar to the ones introduced in Uppaal Smc except that the continuous dynamics is limited to price variable derivatives, whereas the price variable itself cannot be constrained (similar to cost variable in Uppaal Cora, except there can be many price variables). The stochastic priced timed game P contains probabilistic and priced extensions, but its behavior is compatible with the original timed game in a sense that probabilistic transitions can be treated as non-deterministic and price variables act only as monitors and thus can be ignored in a timed game setting. Therefore the model can be described in one coherent document as a stochastic priced timed game P and internally converted into a timed game G on demand while preserving the syntactic structure.
Some of the strategies σ, notably the most permissive kind, from timed game G describe a union of all possible strategies and thus contain multiple (non-determistic) options and thus these options can be price-optimized by synthesyzing another strategy σ° on a stochastic priced timed game P which shares the same structure as G, thus affectively solving a stochastic priced timed game.
Similar to the above layer, the optimized strategies σ° can be further examined by (statistical) model checking P under σ°.