CINECA IRIS Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Torino.
AperTO è l'archivio istituzionale Open Access destinato a raccogliere, rendere visibile e conservare la produzione scientifica dell'Università degli Studi di Torino.
EnglishThe Markov Decision Process (MDP) formalism is a well-known mathematical formalism to study systems with unknown scheduling mechanisms or with transitions whose next-state probability distribution is not known with precision. Analysis methods for MDPs are based generally on the identification of the strategies that maximize (or minimize) a target function based on the MDP’s rewards (or costs). Alternatively, formal languages can be defined to express quantitative properties that we want to be ensured by an MDP, including those which extend classical temporal logics with probabilistic operators. The MDP formalism is low level: to facilitate the representation of complex real-life distributed systems higher-level languages have been proposed. In this chapter we consider Markov Decision Well-formed Nets (MDWN), which are probabilistic extensions of Petri nets that allow one to describe complex nondeterministic (proba- bilistic) behavior as a composition of simpler nondeterministic (probabilistic) steps, and which inherit the efficient analysis algorithms originally devised for well-formed Petri nets. The features of the formalism and the type of properties that can be studied are illustrated by an example of a peer-to-peer illegal botnet.
| Titolo: | Modeling and Verification of Distributed Systems using Markov Decision Processes | |
| Autori Riconosciuti: | ||
| Autori: | Beccuti, Marco; Franceschinis, Giuliana; Sproston, Jeremy | |
| Data di pubblicazione: | 2015 | |
| Abstract: | The Markov Decision Process (MDP) formalism is a well-known mathematical formalism to study systems with unknown scheduling mechanisms or with transitions whose next-state probability distribution is not known with precision. Analysis methods for MDPs are based generally on the identification of the strategies that maximize (or minimize) a target function based on the MDP’s rewards (or costs). Alternatively, formal languages can be defined to express quantitative properties that we want to be ensured by an MDP, including those which extend classical temporal logics with probabilistic operators. The MDP formalism is low level: to facilitate the representation of complex real-life distributed systems higher-level languages have been proposed. In this chapter we consider Markov Decision Well-formed Nets (MDWN), which are probabilistic extensions of Petri nets that allow one to describe complex nondeterministic (proba- bilistic) behavior as a composition of simpler nondeterministic (probabilistic) steps, and which inherit the efficient analysis algorithms originally devised for well-formed Petri nets. The features of the formalism and the type of properties that can be studied are illustrated by an example of a peer-to-peer illegal botnet. | |
| Editore: | Wiley-Scrivener | |
| Titolo del libro: | Quantitative Assessments of Distributed Systems: Methodologies and Techniques | |
| Pagina iniziale: | 3 | |
| Pagina finale: | 26 | |
| Digital Object Identifier (DOI): | 10.1002/9781119131151.ch1 | |
| ISBN: | 978-1118595213 1118595211 | |
| Parole Chiave: | Markov decision processes, modeling and verification | |
| Appare nelle tipologie: | 02A-Contributo in volume |
File in questo prodotto:
Copyright © 2022