A case study of policy synthesis for swarm robotics

Paul Piho, Jane Hillston

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Continuous time Markov chain models, derived from process algebraic descriptions of systems are a powerful method for studying the dynamics of collective adaptive systems. Here, we study a formal modelling framework, based on the CARMA process algebra, where information about the possible control actions of individual components in such systems can be incorporated in the process algebraic description. The formal semantics for such specifications are defined to give rise to continuous time Markov decision processes. Here we show how, together with a given specification of desired collective behaviour, such models can be readily treated as stochastic policy or control synthesis problems. This is demonstrated through an example scenario from swarm robotics.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation: Engineering Principles (ISoLA 2020)
PublisherSpringer
Pages491-506
Number of pages16
ISBN (Electronic)978-3-030-61470-6
ISBN (Print)978-3-030-61469-0
DOIs
Publication statusPublished - 27 Oct 2020
Event9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Rhodes, Greece
Duration: 26 Oct 202030 Oct 2020
http://isola-conference.org/isola2020/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12477
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Symposium

Symposium9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation
Abbreviated titleISoLA 2020
Country/TerritoryGreece
CityRhodes
Period26/10/2030/10/20
Internet address

Fingerprint

Dive into the research topics of 'A case study of policy synthesis for swarm robotics'. Together they form a unique fingerprint.

Cite this