Spotlight Abstraction of Agents and Areas

Authors Tobe Toben, Bernd Westphal, Jan-Hendrik Rakow

Thumbnail PDF


  • Filesize: 109 kB
  • 4 pages

Document Identifiers

Author Details

Tobe Toben
Bernd Westphal
Jan-Hendrik Rakow

Cite AsGet BibTex

Tobe Toben, Bernd Westphal, and Jan-Hendrik Rakow. Spotlight Abstraction of Agents and Areas. In Quantitative and Qualitative Analysis of Network Protocols. Dagstuhl Seminar Proceedings, Volume 10051, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


We present "spotlight abstraction" as a generic abstraction technique for the analysis of systems comprising an unbounded number of communicating agents. The abstraction principle is heterogeneous in the sense that the behaviour of a finite number of agents is preserved while the others are only abstractly represented. The precision of the abstraction can be tuned by an iterative procedure based on the analysis of counterexamples. Going beyond existing work, we show how to use the spotlight principle for analysing systems where the physical position of agents is relevant. To this end, we put the spotlight on areas rather than on fixed sets of agents.
  • Spotlight Abstraction
  • Verification
  • Dynamic Communication Systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail