Modeling and Verification of Distributed Systems Using Markov Decision Processes

Marco Beccuti, Giuliana Annamaria FRANCESCHINIS, Jeremy Sproston

Risultato della ricerca: Capitolo in libro/report/atti di convegnoContributo in volume (Capitolo o Saggio)peer review

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 (probabilistic) 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.
Lingua originaleInglese
Titolo della pubblicazione ospiteQuantitative Assessments of Distributed Systems: Methodologies and Techniques
EditoreJohn Wiley & Sons, Ltd
Pagine1-26
Numero di pagine26
ISBN (stampa)9781119131151
DOI
Stato di pubblicazionePubblicato - 1 gen 2015

Keywords

  • Markov Decision Processes
  • Modeling and Verification

Fingerprint

Entra nei temi di ricerca di 'Modeling and Verification of Distributed Systems Using Markov Decision Processes'. Insieme formano una fingerprint unica.

Cita questo