Artur Meski, Maciej Koutny, Wojciech Penczek: Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations. Fundam. Inform. 154(1-4): 289-306 (2017)
Abstract. Reaction systems are a formal model for computational processes inspired by the functioning of the living cell. This paper introduces reaction systems with discrete concentrations, which are an extension of reaction systems allowing for quantitative modelling. We demonstrate that although reaction systems with discrete concentrations are semantically equivalent to the original qualitative reaction systems, they provide much more succinct representations in terms of the number of entities being used. We define a variant of Linear Time Temporal Logic interpreted over models of reaction systems with discrete concentrations. We provide its suitable encoding in SMT, together with bounded model checking, and present experimental results demonstrating the scalability of the verification method for reaction systems with discrete concentrations.
Artur Męski, Wojciech Penczek, Grzegorz Rozenberg: Model checking temporal properties of reaction systems. Information Sciences 313: 22-42 (2015)
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.