Efficient Checking of Individual Rewards Properties in Markov Population Models

TL;DR

This paper extends fluid model checking techniques for Markov population models to verify properties involving rewards, enhancing the analysis of individual agent behaviors within these stochastic systems.

Contribution

It introduces a method to verify reward-based properties in Markov population models, building on existing fluid model checking approaches.

Findings

Enables checking of reward properties in Markov models

Improves analysis of individual agent behaviors

Extends existing fluid model checking techniques

Abstract

In recent years fluid approaches to the analysis of Markov populations models have been demonstrated to have great pragmatic value. Initially developed to estimate the behaviour of the system in terms of the expected values of population counts, the fluid approach has subsequently been extended to more sophisticated interrogations of models through its embedding within model checking procedures. In this paper we extend recent work on checking CSL properties of individual agents within a Markovian population model, to consider the checking of properties which incorporate rewards.