<p>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 <i>distributed</i> 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 rs<span>ctlk</span>&#xa0;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 rs<span>ctlk</span>&#xa0; model checking problem that is shown to be <span>pspace</span> -complete.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Model checking for distributed reaction systems with temporal-epistemic properties

  • Artur Meski,
  • Maciej Koutny,
  • Łukasz Mikulski,
  • Ion Petre,
  • Wojciech Penczek,
  • Marcin Piatkowski

摘要

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.