Affiliations: [a] Institute of Computer Science, PAS, Jana Kazimierza 5, 01-248 Warsaw, Poland | [b] Vector Software, Inc., London, UK. [email protected], [email protected] | [c] School of Computing Science, Newcastle University, Newcastle upon Tyne, NE1 7RU, UK. [email protected] | [d] Institute of Computer Science, PAS, Jana Kazimierza 5, 01-248 Warsaw, Poland | [e] University of Natural Sciences and Humanities, ICS, Siedlce, Poland. [email protected]
Correspondence:
[*]
Address for correspondence: Institute of Computer Science, PAS, Jana Kazimierza 5, 01-248 Warsaw, Poland
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.
Keywords: reaction systems, bounded model checking, linear time temporal logic
