ePrints

Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations

Lookup NU author(s): Artur Meski, Professor Maciej KoutnyORCiD

Downloads

• Accepted version [.pdf]

Licence

This is the authors' accepted manuscript of an article that has been published in its final definitive form by IOS Press, 2017.

For re-use rights please refer to the publisher's terms and conditions.

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.

Publication metadata

Author(s): Meski A, Koutny M, Penczek W

Publication type: Article

Publication status: Published

Journal: Fundamenta Informaticae

Year: 2017

Volume: 154

Issue: 1-4

Pages: 289-306

Online publication date: 09/08/2017

Acceptance date: 20/06/2017

Date deposited: 06/08/2017

ISSN (print): 0169-2968

ISSN (electronic): 1875-8681

Publisher: IOS Press

URL: https://doi.org/10.3233/FI-2017-1567

DOI: 10.3233/FI-2017-1567

Altmetrics

Share