Model checking temporal properties of reaction systems

Authors

  • Artur Meski
  • Wojciech Penczek
  • Grzegorz Rozenberg

Abstract

This paper defines a temporal logic for reaction systems (rsCTL). The logic is interpreted over the models for the context restricted reaction systems that generalise standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for rsCTL over these systems. The model checking for rsCTL is proved to be PSPACE-complete. The proposed approach to model checking was implemented and experimentally evaluated using four benchmarks.

Publication Details

  • Date: 2015/8/20
  • Journal: Information Sciences
  • Volume 313, Pages 22-42
  • Publisher: Elsevier