A1 Refereed original research article in a scientific journal

Model checking for distributed reaction systems with temporal-epistemic properties




AuthorsMeski, Artur; Koutny, Maciej; Mikulski, Łukasz; Petre, Ion; Penczek, Wojciech; Piatkowski, Marcin

Publisher Springer Nature

Publication year2025

Journal: Natural Computing

ISSN1567-7818

eISSN1572-9796

DOIhttps://doi.org/10.1007/s11047-025-10044-7

Publication's open availability at the time of reportingOpen Access

Publication channel's open availability Partially Open Access publication channel

Web address https://doi.org/10.1007/s11047-025-10044-7

Self-archived copy’s web addresshttps://research.utu.fi/converis/portal/detail/Publication/505447385


Abstract

Reaction systems are a model of computation inspired by the biochemistry exhibited by living cells. This paper introduces the notion of agency as an extension to the reaction systems formalism, leading to distributed reaction systems. Adding agents in the reaction systems setting, allows for the natural modelling and representation of multi-agent and distributed systems. To support the specification of temporal-epistemic properties of distributed reaction systems, we introduce the logic rsctlk and present experimental results of its associated model checking procedure run on a biological benchmark of within-cell signal transduction networks. The experimental results are encouraging despite the complexity of the rsctlk  model checking problem that is shown to be pspace -complete.


Downloadable publication

This is an electronic reprint of the original article.
This reprint may differ from the original in pagination and typographic detail. Please cite the original version.





Last updated on 2025-19-11 at 14:13