Model checking mobile ad hoc networks

Fatemeh Ghassemi*, Wan Fokkink

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


Modeling arbitrary connectivity changes within mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We use constrained labeled transition systems as a semantic model to represent mobility. To model check MANET protocols with respect to the underlying topology and connectivity changes, we introduce a branching-time temporal logic. The path quantifiers are parameterized by multi-hop constraints over topologies, to discriminate the paths over which the temporal behavior should be investigated; the paths that violate the multi-hop constraints are not considered. A model checking algorithm is presented to verify MANETs that allow arbitrary mobility, under the assumption of reliable communication. It is applied to analyze a leader election protocol.

Original languageEnglish
Pages (from-to)159-189
Number of pages31
JournalFormal Methods in System Design
Issue number3
Publication statusPublished - 1 Dec 2016


  • Constrained labeled transition systems
  • Mobile ad hoc networks
  • Model checking
  • Multi-hop network constraints


Dive into the research topics of 'Model checking mobile ad hoc networks'. Together they form a unique fingerprint.

Cite this