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 language | English |
---|---|
Title of host publication | Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles (ISoLA 2020) |
Publisher | Springer |
Pages | 491-506 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-030-61470-6 |
ISBN (Print) | 978-3-030-61469-0 |
DOIs | |
Publication status | Published - 27 Oct 2020 |
Event | 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Rhodes, Greece Duration: 26 Oct 2020 → 30 Oct 2020 http://isola-conference.org/isola2020/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 12477 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Symposium
Symposium | 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation |
---|---|
Abbreviated title | ISoLA 2020 |
Country/Territory | Greece |
City | Rhodes |
Period | 26/10/20 → 30/10/20 |
Internet address |