Nicolas Markey

Résumé

Model checking (MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. Realizing that the distributed power control (PC) problem can be modeled by a timed game between a given transmitter and its environment, the authors wanted to know whether this approach can be applied to distributed PC. It turns out that it can be applied successfully and allows one to analyze realistic scenarios including the case of discrete transmit powers and games with incomplete information. The proposed methodology is as follows. We state some objectives a transmitter-receiver pair would like to reach. The network is modeled by a game where transmitters are considered as timed automata interacting with each other. The objectives are then translated into timed alternating-time temporal logic formulae and MC is exploited to know whether the desired properties are verified and determine a winning strategy.

@article{jwcn2010(861472)-BJLMO,
  author =              {Brihaye, {\relax Th}omas and Jungers, Marc and
                         Lasaulce, Samson and Markey, Nicolas and Oreiby,
                         Ghassan},
  title =               {Using Model Checking for Analyzing Distributed Power
                         Control Problems},
  publisher =           {Hindawi Publishing Corp.},
  journal =             {EURASIP Journal on Wireless Communications and
                         Networking},
  volume =              {2010},
  number =              {861472},
  year =                {2010},
  month =               jun,
  doi =                 {10.1155/2010/861472},
  abstract =            {Model checking~(MC) is a formal verification
                         technique which has been known and still knows a
                         resounding success in the computer science
                         community. Realizing that the distributed power
                         control~(PC) problem can be modeled by a timed game
                         between a given transmitter and its environment, the
                         authors wanted to know whether this approach can be
                         applied to distributed~PC. It~turns out that it can
                         be applied successfully and allows one to analyze
                         realistic scenarios including the case of discrete
                         transmit powers and games with incomplete
                         information. The proposed methodology is as follows.
                         We state some objectives a transmitter-receiver pair
                         would like to reach. The network is modeled by a
                         game where transmitters are considered as timed
                         automata interacting with each other. The objectives
                         are then translated into timed alternating-time
                         temporal logic formulae and MC is exploited to know
                         whether the desired properties are verified and
                         determine a winning strategy.},
}