License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.10051.3
URN: urn:nbn:de:0030-drops-25173
Go to the corresponding Portal

Toben, Tobe ; Westphal, Bernd ; Rakow, Jan-Hendrik

Spotlight Abstraction of Agents and Areas

10051.TobenTobe.ExtAbstract.2517.pdf (0.1 MB)


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.

BibTeX - Entry

  author =	{Toben, Tobe and Westphal, Bernd and Rakow, Jan-Hendrik},
  title =	{{Spotlight Abstraction of Agents and Areas}},
  booktitle =	{Quantitative and Qualitative Analysis of Network Protocols},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10051},
  editor =	{Bengt Jonsson and J\"{o}rg Kreiker and Marta Kwiatkowska},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-25173},
  doi =		{10.4230/DagSemProc.10051.3},
  annote =	{Keywords: Spotlight Abstraction, Verification, Dynamic Communication Systems}

Keywords: Spotlight Abstraction, Verification, Dynamic Communication Systems
Collection: 10051 - Quantitative and Qualitative Analysis of Network Protocols
Issue Date: 2010
Date of publication: 13.04.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI