Model checking temporal properties of reaction systems, Męski, A., Penczek, W., & Rozenberg, G.

[RS-Repo]

Męski, A., Penczek, W., & Rozenberg, G. (2015). Model checking temporal properties of reaction systems. Information Sciences, 313, 22-42.

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.

Link to the online copy

Bibtex file
@Article{mkeski2015model,
title={Model checking temporal properties of reaction systems},
author={M{\k{e}}ski, Artur and Penczek, Wojciech and Rozenberg, Grzegorz},
journal={Information Sciences},
volume={313},
pages={22--42},
year={2015},
publisher={Elsevier}
}