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.
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}
}
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} }