2026-07-23T22:06:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2517 2024-03-06T11:09:08Z ddc:004 open_access

Spotlight Abstraction of Agents and Areas Toben, Tobe Westphal, Bernd Rakow, Jan-Hendrik Spotlight Abstraction Verification Dynamic Communication Systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Tobe Toben and Bernd Westphal and Jan-Hendrik Rakow 2010 Is Part Of Dagstuhl Seminar Proceedings, Volume 10051, Quantitative and Qualitative Analysis of Network Protocols (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.10051.3 urn:nbn:de:0030-drops-25173 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10051.3 eng https://creativecommons.org/licenses/by/4.0/legalcode