In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will approximate the behaviour of a single agent with a time-inhomogeneous CTMC, which depends on the environment and on the other agents only through the solution of the fluid differential equation, and model check this process. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.

Model checking single agent behaviours by fluid approximation

BORTOLUSSI, LUCA;
2015-01-01

Abstract

In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will approximate the behaviour of a single agent with a time-inhomogeneous CTMC, which depends on the environment and on the other agents only through the solution of the fluid differential equation, and model check this process. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.
2015
Pubblicato
http://www.sciencedirect.com/science/article/pii/S0890540115000176
File in questo prodotto:
File Dimensione Formato  
InfComp2015-FMC.pdf

Open Access dal 01/07/2017

Descrizione: pdf post-print
Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Digital Rights Management non definito
Dimensione 1.65 MB
Formato Adobe PDF
1.65 MB Adobe PDF Visualizza/Apri
InfComp2015.pdf

Accesso chiuso

Descrizione: pdf editoriale
Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 1.95 MB
Formato Adobe PDF
1.95 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
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/2858274
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 17
social impact