Verification and External Parameter Inference for Stochastic World Models

TL;DR

This work introduces ULTIMATE, a framework and tool for verifying properties of heterogeneous, interdependent multi-model stochastic systems. By modeling a system as $U=(M,D,E)$ and resolving dependencies via a dependency graph and SCC decomposition, ULTIMATE combines probabilistic, parametric, and Bayesian/frequentist methods to compute $pmc(m_v,c_v)$ for models within the network, even in the presence of circular dependencies. The approach is implemented in an open-source Java tool and validated on five case studies (e.g., RAD, SMD, RoboFleet, DPM-FX, RoCo), demonstrating that complex inter-model verification can be automated and executed within seconds on standard hardware. This work advances PMC by enabling joint verification and synthesis across heterogeneous stochastic models, expanding practical applicability to software-intensive systems with partial observability and multiple inference paradigms.

Abstract

Given its ability to analyse stochastic models ranging from discrete and continuous-time Markov chains to Markov decision processes and stochastic games, probabilistic model checking (PMC) is widely used to verify system dependability and performance properties. However, modelling the behaviour of, and verifying these properties for many software-intensive systems requires the joint analysis of multiple interdependent stochastic models of different types, which existing PMC techniques and tools cannot handle. To address this limitation, we introduce a tool-supported UniversaL stochasTIc Modelling, verificAtion and synThEsis (ULTIMATE) framework that supports the representation, verification and synthesis of heterogeneous multi-model stochastic systems with complex model interdependencies. Through its unique integration of multiple PMC paradigms, and underpinned by a novel verification method for handling model interdependencies, ULTIMATE unifies-for the first time-the modelling of probabilistic and nondeterministic uncertainty, discrete and continuous time, partial observability, and the use of both Bayesian and frequentist inference to exploit domain knowledge and data about the modelled system and its context. A comprehensive suite of case studies and experiments confirm the generality and effectiveness of our novel verification framework.

Figures (6)

• Figure 1: ULTIMATE multi-model verification
• Figure 2: Examples of stochastic models from Table \ref{['table:model-types']}: DTMC modelling an agent's execution of a task which, being tried in state $s_0$, succeeds with probability 0.8 (leading to a DTMC transition to state $s_1$), fails with probability 0.1 (leading to a transition to state $s_2$), or times out with probability 0.1 (yielding a transition to state $s_3$, where the task is re-tried with probability 0.5, or the agent gives up and the task fails with probability 0.5); MDP modelling a variant of the agent in which two actions are available in both state $s_0$ ($a$ and $a'$) and $s_3$ ($b$ and $b'$); POMDP modelling the scenario in which states $s_2$ and $s_3$ are indistinguishable to the agent from the MDP; SG modelling the scenario in which two different agents decide the action selected in state $s_0$ ($a$ or $a'$) and $s_3$ ($b$ or $b'$); PA modelling the presence of two transition probability distributions for action $a$ from state $s_0$; CTMC modelling the rates of transition between the states of the same agent.
• Figure 3: RAD stochastic models and dependencies
• Figure 4: RAD system verification using the ULTIMATE tool
• Figure 5: Stochastic models and dependencies for the SMD, RoboFleet, DPM-FX and RoCo case studies

Theorems & Definitions (23)

• Definition 1
• Example 1
• Definition 2
• Definition 3
• Example 2
• Definition 4
• Example 3
• Theorem 1
• proof
• Definition 5: Discrete time Markov chain