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.

Efficient Checking of Individual Rewards Properties in Markov Population Models

BORTOLUSSI, LUCA;
2015-01-01

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.
File in questo prodotto:
File Dimensione Formato  
QAPL2015-2.pdf

accesso aperto

Descrizione: pdf editoriale
Tipologia: Documento in Versione Editoriale
Licenza: Digital Rights Management non definito
Dimensione 435.61 kB
Formato Adobe PDF
435.61 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/2856198
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 4
social impact