ArTS Archivio della ricerca di Trieste
ArTS è il sistema di gestione integrata dei dati della ricerca adottato dall' Università degli Studi di Trieste
EnglishWe address the problem of verifying timed properties of Markovian models of large populations of interacting agents, modelled as finite state automata. In particular, we focus on time-bounded properties of (random) individual agents specified by Deterministic Timed Automata (DTA) endowed with a single clock. Exploiting ideas from fluid approximation, we estimate the satisfaction probability of the DTA properties by reducing it to the computation of the transient probability of a subclass of Time-Inhomogeneous Markov Renewal Processes with exponentially and deterministically-timed transitions, and a small state space. For this subclass of models, we show how to derive a set of Delay Differential Equations (DDE), whose numerical solution provides a fast and accurate estimate of the satisfaction probability. In the paper, we also prove the asymptotic convergence of the approach, and exemplify the method on a simple epidemic spreading model. Finally, we also show how to construct a system of DDEs to efficiently approximate the average number of agents that satisfy the DTA specification.
| Titolo: | Fluid model checking of timed properties |
| Autori: | |
| Data di pubblicazione: | 2015 |
| Rivista: | |
| Abstract: | We address the problem of verifying timed properties of Markovian models of large populations of interacting agents, modelled as finite state automata. In particular, we focus on time-bounded properties of (random) individual agents specified by Deterministic Timed Automata (DTA) endowed with a single clock. Exploiting ideas from fluid approximation, we estimate the satisfaction probability of the DTA properties by reducing it to the computation of the transient probability of a subclass of Time-Inhomogeneous Markov Renewal Processes with exponentially and deterministically-timed transitions, and a small state space. For this subclass of models, we show how to derive a set of Delay Differential Equations (DDE), whose numerical solution provides a fast and accurate estimate of the satisfaction probability. In the paper, we also prove the asymptotic convergence of the approach, and exemplify the method on a simple epidemic spreading model. Finally, we also show how to construct a system of DDEs to efficiently approximate the average number of agents that satisfy the DTA specification. |
| Handle: | http://hdl.handle.net/11368/2856186 |
| ISBN: | 9783319229744 |
| URL: | http://springerlink.com/content/0302-9743/copyright/2005/ |
| Appare nelle tipologie: | 4.1 Contributo in Atti Convegno (Proceeding) |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| FORMATS2015-post.pdf | post-print | Bozza finale post-referaggio (post-print) | Digital Rights Management non definito | Open Access Visualizza/Apri |
| FORMATS2015.pdf | Documento in Versione Editoriale | Digital Rights Management non definito | Administrator Richiedi una copia |
http://hdl.handle.net/11368/2856186
