Efficient Checking of Individual Rewards Properties in Markov Population Models

Efficient Checking of Individual Rewards Properties in Markov Population Models

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 m...

Full description

Bibliographic Details
Main Authors: Luca Bortolussi, Jane Hillston
Format: Article
Language:English
Published: Open Publishing Association 2015-09-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1509.08561v1
id doaj-79a31a374b7f4411932f2d8d57114d3c
record_format Article
spelling doaj-79a31a374b7f4411932f2d8d57114d3c2020-11-24T21:00:27ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-09-01194Proc. QAPL 2015324710.4204/EPTCS.194.3:6Efficient Checking of Individual Rewards Properties in Markov Population ModelsLuca Bortolussi0Jane Hillston1 University of Trieste University of Edinburgh 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.http://arxiv.org/pdf/1509.08561v1
collection DOAJ
language English
format Article
sources DOAJ
author Luca Bortolussi
Jane Hillston
spellingShingle Luca Bortolussi
Jane Hillston
Efficient Checking of Individual Rewards Properties in Markov Population Models
Electronic Proceedings in Theoretical Computer Science
author_facet Luca Bortolussi
Jane Hillston
author_sort Luca Bortolussi
title Efficient Checking of Individual Rewards Properties in Markov Population Models
title_short Efficient Checking of Individual Rewards Properties in Markov Population Models
title_full Efficient Checking of Individual Rewards Properties in Markov Population Models
title_fullStr Efficient Checking of Individual Rewards Properties in Markov Population Models
title_full_unstemmed Efficient Checking of Individual Rewards Properties in Markov Population Models
title_sort efficient checking of individual rewards properties in markov population models
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2015-09-01
description 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.
url http://arxiv.org/pdf/1509.08561v1
work_keys_str_mv AT lucabortolussi efficientcheckingofindividualrewardspropertiesinmarkovpopulationmodels
AT janehillston efficientcheckingofindividualrewardspropertiesinmarkovpopulationmodels
_version_ 1716779621717901312

Similar Items