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

• Autorzy: Męski A. , Koutny M. , Penczek W.

Identyfikatory

DOI

10.3233/FI-2017-1567

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

reaction system; bounded model checking; linear time temporal logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 154, nr 1/4
• Strony: 289--306
• Opis fizyczny: Bibliogr. 27 poz., rys., tab., wykr.

Twórcy

autor

Męski A.

• Institute of Computer Science, PAS, Jana Kazimierza 5, 01-248 Warsaw, Poland
• Vector Software, Inc., London, UK

autor

Koutny M.

• School of Computing Science, Newcastle University, Newcastle upon Tyne, NE1 7RU, UK

autor

Penczek W.

• Institute of Computer Science, PAS, Jana Kazimierza 5, 01-248 Warsaw, Poland
• University of Natural Sciences and Humanities, ICS, Siedlce, Poland

Bibliografia

• [1] Ehrenfeucht A, Rozenberg G. Reaction Systems. Fundamenta Informaticae, 2007;75(1-4):263–280. URL http://content.iospress.com/articles/fundamenta-informaticae/fi75-1-4-15.
• [2] Ehrenfeucht A, Kleijn J, Koutny M, Rozenberg G. Reaction Systems: A Natural Computing Approach to the Functioning of Living Cells. A Computable Universe, Understanding and Exploring Nature as Computation, 2012. pp. 189–208. doi:10.1142/9789814374309_0010.
• [3] Ehrenfeucht A, Kleijn J, Koutny M, Rozenberg G. Evolving reaction systems. Theoretical Computer Science, 2017;682:79–99. doi:10.1016/j.tcs.2016.12.031.
• [4] Ehrenfeucht A, Rozenberg G. Introducing time in reaction systems. Theoretical Computer Science, 2009;410(4-5):310–322. doi:10.1016/j.tcs.2008.09.043.
• [5] Hirvensalo M. On probabilistic and quantum reaction systems. Theoretical Computer Science, 2012;429:134–143. doi:10.1016/j.tcs.2011.12.032.
• [6] Alhazov A, Aman B, Freund R, Ivanov S. Simulating R Systems by P Systems. In: Membrane Computing, 17th International Conference, CMC 2016, Milan, Italy, July 25-29, 2016. 2016 pp. 51–66. doi: 10.1007/978-3-319-54072-6_4.
• [7] Formenti E, Manzoni L, Porreca AE. Cycles and Global Attractors of Reaction Systems. In: Descriptional Complexity of Formal Systems-16th International Workshop, DCFS 2014, LNCS. 2014 pp. 114–125. doi:10.1007/978-3-319-09704-6_11.
• [8] Formenti E, Manzoni L, Porreca AE. Fixed Points and Attractors of Reaction Systems. In: Language, Life, Limits-10th Conference on Computability in Europe, CiE 2014, volume 8493 of LNCS. Springer, 2014 pp. 194–203. doi:10.1007/978-3-319-08019-2_20.
• [9] Formenti E, Manzoni L, Porreca AE. On the complexity of occurrence and convergence problems in reaction systems. Natural Computing, 2014. pp. 1–7. doi:10.1007/s11047-014-9456-3.
• [10] Salomaa A. Functions and sequences generated by reaction systems. Theoretical Computer Science, 2012;466:87–96. doi:10.1016/j.tcs.2012.07.022.
• [11] Salomaa A. On State Sequences Defined by Reaction Systems. In: Logic and Program Semantics. 2012 pp. 271–282. doi:10.1007/978-3-642-29485-3_17.
• [12] Salomaa A. Functional Constructions between reaction Systems and Propositional Logic. Int. J. of Foundations of Computer Science, 2013;24(1):147–160. doi:10.1142/S0129054113500044.
• [13] Salomaa A. Minimal and almost minimal reaction systems. Natural Computing, 2013;12(3):369–376. doi: 10.1007/s11047-013-9372-y.
• [14] Azimi S, Iancu B, Petre I. Reaction System Models for the Heat Shock Response. Fundamenta Informaticae, 2014;131(3-4):299–312. doi:10.3233/FI-2014-1016.
• [15] Corolli L, Maj C, Marini F, Besozzi D, Mauri G. An excursion in reaction systems: From computer science to biology. Theoretical Computer Science, 2012;454:95–108. doi:10.1016/j.tcs.2012.04.003.
• [16] Azimi S, Gratie C, Ivanov S, Manzoni L, Petre I, Porreca AE. Complexity of Model Checking for Reaction Systems. Theoretical Computer Science, 2016;623:103–113. doi:10.1016/ j.tcs.2015.11.040.
• [17] Azimi S, Gratie C, Ivanov S, Petre I. Dependency Graphs and Mass Conservation in Reaction Systems. Theoretical Computer Science, 2015;598:23–39. doi:10.1016/ j.tcs.2015.02.014.
• [18] Męski A, Penczek W, Rozenberg G. Model Checking Temporal Properties of Reaction Systems. Information Sciences, 2015;313:22–42. doi:10.1016/j.ins.2015.03.048.
• [19] Męski A, Koutny M, Penczek W. Towards Quantitative Verification of Reaction Systems. In: Unconventional Computation and Natural Computation: 15th International Conference, UCNC 2016, Manchester, UK, July 11-15, 2016, Proceedings. 2016 pp. 142–154. doi:10.1007/978-3-319-41312-9_12.
• [20] Horn F, Jackson R. General mass action kinetics. Archive for Rational Mechanics and Analysis, 1972;47(2):81–116. doi:10.1007/BF00251225.
• [21] Brijder R, Ehrenfeucht A, Rozenberg G. Reaction Systems with Duration. In: Computation, Cooperation, and Life-Essays Dedicated to Gheorghe Pǎun on the Occasion of His 60th Birthday, volume 6610 of LNCS. Springer, 2011 pp. 191–202. doi:10.1007/978-3-642-20000-7_16.
• [22] Kroening D, Strichman O. Decision Procedures-An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2016. doi:10.1007/978-3-662-50497-0.
• [23] Biere A, Cimatti A, Clarke EM, Zhu Y. Symbolic Model Checking Without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS ’99. Springer-Verlag, 1999 pp. 193–207. doi:10.1007/3-540-49059-0_14.
• [24] Biere A, Heljanko K, Junttila TA, Latvala T, Schuppan V. Linear Encodings of Bounded LTL Model Checking. Logical Methods in Computer Science, 2006; 2(5). doi:10.2168/LMCS-2(5:5)2006.
• [25] Clarke E, Grumberg O, Peled D. Model Checking. MIT Press, 1999. ISBN 978-0-262-03270-4.
• [26] de Moura L, Bjørner N. Z3: An Efficient SMT Solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2008. Springer-Verlang, 2008 pp. 337–340. doi:10.1007/978-3-540-78800-3_24.
• [27] Clarke EM, Kroening D, Ouaknine J, Strichman O. Completeness and Complexity of Bounded Model Checking. In: Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Proceedings. 2004 pp. 85–96. doi:10.1007/978-3-540-24622-0_9.