Quantitative μ-Calculus Analysis of Power Management in Wireless Networks

摘要

An important concern in wireless network technology is battery conservation. A promising approach to saving energy is to allow nodes periodically to enter a "low power mode", however this strategy contributes to message delay, and careful management is required so that the system-wide performance is not severely compromised.rnIn this paper we show how to manage power schedules using the quantitative modal μ-calculus which allows the specification of a quantitative performance property as a game in which a maximising player's optimal strategy corresponds to optimising overall performance relative to the specified property.rnWe extend the standard results on discounted games to a class of infinite state systems, and illustrate our results on a small case study.