Network connectivity and energy conservation are two major goals in mobile ad-hoc networks (MANETs). In this paper we propose a probabilistic, energy-aware, broadcast calculus for the analysis of both such aspects of MANETs. We first present a probabilistic behavioural congruence together with a co-inductive proof technique based on the notion of bisimulation. Then we define an energy-aware preorder over networks. The behavioural congruence allows us to verify whether two networks exhibit the same (probabilistic) connectivity behaviour, while the preorder makes it possible to evaluate the energy consumption of different, but behaviourally equivalent, networks. In practice, the quantitative evaluation of the models is carried out by resorting to the statistical model checking implemented in the PRISM tool, i.e., a simulation of the probabilistic model. We consider two case studies: first we evaluate the performance of the Location Aided Routing protocol, then we compare the energy efficiency of the Go-Back-N protocol with that of the Stop-And-Wait in a network with mobility.

Connectivity and energy-aware preorders for mobile ad-hoc networks

GALLINA, LUCIA;MARIN, Andrea;ROSSI, Sabina
2016-01-01

Abstract

Network connectivity and energy conservation are two major goals in mobile ad-hoc networks (MANETs). In this paper we propose a probabilistic, energy-aware, broadcast calculus for the analysis of both such aspects of MANETs. We first present a probabilistic behavioural congruence together with a co-inductive proof technique based on the notion of bisimulation. Then we define an energy-aware preorder over networks. The behavioural congruence allows us to verify whether two networks exhibit the same (probabilistic) connectivity behaviour, while the preorder makes it possible to evaluate the energy consumption of different, but behaviourally equivalent, networks. In practice, the quantitative evaluation of the models is carried out by resorting to the statistical model checking implemented in the PRISM tool, i.e., a simulation of the probabilistic model. We consider two case studies: first we evaluate the performance of the Location Aided Routing protocol, then we compare the energy efficiency of the Go-Back-N protocol with that of the Stop-And-Wait in a network with mobility.
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Accesso chiuso-personale
Dimensione 2 MB
Formato Adobe PDF
2 MB Adobe PDF Visualizza/Apri

I documenti in ARCA 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/10278/3673294
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 1
social impact