Scalable Probabilistic Models for 802.11 Protocol Verification

From Simple Sci Wiki
Revision as of 15:39, 24 December 2023 by SatoshiNakamoto (talk | contribs) (Created page with "Title: Scalable Probabilistic Models for 802.11 Protocol Verification Abstract: This research aims to create more scalable and accurate models for the 802.11 protocol, enabling efficient verification of real-time properties. The authors identify ways to simplify probabilistic models, optimize them using probabilistic timed automata, and develop a formal framework to reduce state space. Their optimizations, including abstracting away the acknowledgment protocol and deter...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigation Jump to search

Title: Scalable Probabilistic Models for 802.11 Protocol Verification

Abstract: This research aims to create more scalable and accurate models for the 802.11 protocol, enabling efficient verification of real-time properties. The authors identify ways to simplify probabilistic models, optimize them using probabilistic timed automata, and develop a formal framework to reduce state space. Their optimizations, including abstracting away the acknowledgment protocol and deterministic waits, and considering only a subset of allowed packet sizes, do not change the probability measures. The reduced models are immediately verifiable in PRISM and can be used with other tools like RAPTURE. The results show a significant reduction in state space, making verification more feasible for networks of moderate size.

Link to Article: https://arxiv.org/abs/0403044v1 Authors: arXiv ID: 0403044v1

Retrieved from "https://simplesci.org/index.php?title=Scalable_Probabilistic_Models_for_802.11_Protocol_Verification&oldid=3158"