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...
| Main Authors: | , |
|---|---|
| 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 |
| _version_ | 1818942724991090688 |
|---|---|
| author | Luca Bortolussi Jane Hillston |
| author_facet | Luca Bortolussi Jane Hillston |
| author_sort | Luca Bortolussi |
| collection | DOAJ |
| 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. |
| first_indexed | 2024-12-20T07:15:59Z |
| format | Article |
| id | doaj.art-79a31a374b7f4411932f2d8d57114d3c |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-20T07:15:59Z |
| publishDate | 2015-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-79a31a374b7f4411932f2d8d57114d3c2022-12-21T19:48:48ZengOpen 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 |
| spellingShingle | Luca Bortolussi Jane Hillston Efficient Checking of Individual Rewards Properties in Markov Population Models Electronic Proceedings in Theoretical Computer Science |
| title | 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_short | Efficient Checking of Individual Rewards Properties in Markov Population Models |
| title_sort | efficient checking of individual rewards properties in markov population models |
| url | http://arxiv.org/pdf/1509.08561v1 |
| work_keys_str_mv | AT lucabortolussi efficientcheckingofindividualrewardspropertiesinmarkovpopulationmodels AT janehillston efficientcheckingofindividualrewardspropertiesinmarkovpopulationmodels |