{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:28:57Z","timestamp":1772119737862,"version":"3.50.1"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T00:00:00Z","timestamp":1717200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T00:00:00Z","timestamp":1721779200000},"content-version":"vor","delay-in-days":53,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"PolLux\/FNR-CORE project SpaceVote"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Nat Comput"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Reaction systems are a formal model for computational processing in which reactions operate on sets of entities (molecules) providing a framework for dealing with qualitative aspects of biochemical systems. This paper is concerned with reaction systems in which entities can have discrete concentrations, and so reactions operate on multisets rather than sets of entities. The resulting framework allows one to deal with quantitative aspects of reaction systems, and a bespoke linear-time temporal logic allows one to express and verify a wide range of key behavioural system properties. In practical applications, a reaction system with discrete concentrations may only be partially specified, and the possibility of an effective automated calculation of the missing details provides an attractive design approach. With this idea in mind, the current paper discusses parametric reaction systems with parameters representing unknown parts of hypothetical reactions. The main result is a method aimed at replacing the parameters in such a way that the resulting reaction system operating in a specified external environment satisfies a given temporal logic formula.This paper provides an encoding of parametric reaction systems in\n                    <jats:sc>smt<\/jats:sc>\n                    , and outlines a synthesis procedure based on bounded model checking for solving the synthesis problem. It also reports on the initial experimental results demonstrating the feasibility of the novel synthesis method.\n                  <\/jats:p>","DOI":"10.1007\/s11047-024-09989-y","type":"journal-article","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T05:05:27Z","timestamp":1721797527000},"page":"323-343","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Reaction mining for reaction systems"],"prefix":"10.1007","volume":"23","author":[{"given":"Artur","family":"M\u0119ski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maciej","family":"Koutny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u0141ukasz","family":"Mikulski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,24]]},"reference":[{"issue":"1\u20134","key":"9989_CR1","first-page":"263","volume":"75","author":"A Ehrenfeucht","year":"2007","unstructured":"Ehrenfeucht A, Rozenberg G (2007) Reaction systems. Fundam Infor 75(1\u20134):263\u2013280","journal-title":"Fundam Infor"},{"key":"9989_CR2","doi-asserted-by":"crossref","unstructured":"Ehrenfeucht A, Kleijn J, Koutny M, Rozenberg G (2012) Reaction systems: a natural computing approach to the functioning of living cells. A computable universe, understanding and exploring nature as computation, pp 189\u2013208","DOI":"10.1142\/9789814374309_0010"},{"key":"9989_CR3","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.tcs.2016.12.031","volume":"682","author":"A Ehrenfeucht","year":"2017","unstructured":"Ehrenfeucht A, Kleijn J, Koutny M, Rozenberg G (2017) Evolving reaction systems. Theor Comput Sci 682:79\u201399","journal-title":"Theor Comput Sci"},{"issue":"4\u20135","key":"9989_CR4","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1016\/j.tcs.2008.09.043","volume":"410","author":"A Ehrenfeucht","year":"2009","unstructured":"Ehrenfeucht A, Rozenberg G (2009) Introducing time in reaction systems. Theor Comput Sci 410(4\u20135):310\u2013322","journal-title":"Theor Comput Sci"},{"key":"9989_CR5","doi-asserted-by":"crossref","unstructured":"Brijder R, Ehrenfeucht A, Rozenberg G (2011) Reaction systems with duration. In: Computation, cooperation, and life - essays dedicated to gheorghe paun on the occasion of his 60th birthday. LNCS 6610:191\u2013202","DOI":"10.1007\/978-3-642-20000-7_16"},{"key":"9989_CR6","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1016\/j.tcs.2011.12.032","volume":"429","author":"M Hirvensalo","year":"2012","unstructured":"Hirvensalo M (2012) On probabilistic and quantum reaction systems. Theor Comput Sci 429:134\u2013143","journal-title":"Theor Comput Sci"},{"key":"9989_CR7","doi-asserted-by":"crossref","unstructured":"Alhazov A, Aman B, Freund R, Ivanov S (2016) Simulating R systems by P systems. In: Membrane computing, 17th international conference, CMC 2016, Milan, Italy, pp 51\u201366","DOI":"10.1007\/978-3-319-54072-6_4"},{"key":"9989_CR8","doi-asserted-by":"crossref","unstructured":"Formenti E, Manzoni L, Porreca AE (2014a) Cycles and global attractors of reaction systems. In: Descriptional complexity of formal systems - 16th international workshop, DCFS 2014. LNCS, pp 114\u2013125","DOI":"10.1007\/978-3-319-09704-6_11"},{"key":"9989_CR9","doi-asserted-by":"crossref","unstructured":"Formenti E, Manzoni L, Porreca AE (2014b) Fixed points and attractors of reaction systems. In: Language, life, limits - 10th conference on computability in Europe, CiE 2014. LNCS, vol 8493, pp 194\u2013203","DOI":"10.1007\/978-3-319-08019-2_20"},{"key":"9989_CR10","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s11047-014-9456-3","volume":"14","author":"E Formenti","year":"2014","unstructured":"Formenti E, Manzoni L, Porreca AE (2014c) On the complexity of occurrence and convergence problems in reaction systems. Nat Comput 14:185\u2013191","journal-title":"Nat Comput"},{"key":"9989_CR11","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.tcs.2012.07.022","volume":"466","author":"A Salomaa","year":"2012","unstructured":"Salomaa A (2012a) Functions and sequences generated by reaction systems. Theor Comput Sci 466:87\u201396","journal-title":"Theor Comput Sci"},{"key":"9989_CR12","doi-asserted-by":"crossref","unstructured":"Salomaa A (2012b) On state sequences defined by reaction systems. In: Logic and program semantics, pp 271\u2013282","DOI":"10.1007\/978-3-642-29485-3_17"},{"issue":"1","key":"9989_CR13","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1142\/S0129054113500044","volume":"24","author":"A Salomaa","year":"2013","unstructured":"Salomaa A (2013a) Functional constructions between reaction systems and propositional logic. Int J Found Comput Sci 24(1):147\u2013160","journal-title":"Int J Found Comput Sci"},{"issue":"3","key":"9989_CR14","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s11047-013-9372-y","volume":"12","author":"A Salomaa","year":"2013","unstructured":"Salomaa A (2013b) Minimal and almost minimal reaction systems. Nat Comput 12(3):369\u2013376","journal-title":"Nat Comput"},{"key":"9989_CR15","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1016\/j.tcs.2015.06.001","volume":"598","author":"A Dennunzio","year":"2015","unstructured":"Dennunzio A, Formenti E, Manzoni L (2015a) Reaction systems and extremal combinatorics properties. Theor Comput Sci 598:138\u2013149","journal-title":"Theor Comput Sci"},{"key":"9989_CR16","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1016\/j.tcs.2015.05.046","volume":"608","author":"A Dennunzio","year":"2015","unstructured":"Dennunzio A, Formenti E, Manzoni L, Porreca AE (2015b) Ancestors, descendants, and gardens of Eden in reaction systems. Theor Comput Sci 608:16\u201326","journal-title":"Theor Comput Sci"},{"issue":"3\u20134","key":"9989_CR17","first-page":"299","volume":"131","author":"S Azimi","year":"2014","unstructured":"Azimi S, Iancu B, Petre I (2014) Reaction system models for the heat shock response. Fundam Inf 131(3\u20134):299\u2013312","journal-title":"Fundam Inf"},{"key":"9989_CR18","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.tcs.2012.04.003","volume":"454","author":"L Corolli","year":"2012","unstructured":"Corolli L, Maj C, Marini F, Besozzi D, Mauri G (2012) An excursion in reaction systems: from computer science to biology. Theor Comput Sci 454:95\u2013108","journal-title":"Theor Comput Sci"},{"key":"9989_CR19","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.tcs.2015.11.040","volume":"623","author":"S Azimi","year":"2016","unstructured":"Azimi S, Gratie C, Ivanov S, Manzoni L, Petre I, Porreca AE (2016) Complexity of model checking for reaction systems. Theor Comput Sci 623:103\u2013113","journal-title":"Theor Comput Sci"},{"key":"9989_CR20","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.tcs.2015.02.014","volume":"598","author":"S Azimi","year":"2015","unstructured":"Azimi S, Gratie C, Ivanov S, Petre I (2015) Dependency graphs and mass conservation in reaction systems. Theor Comput Sci 598:23\u201339","journal-title":"Theor Comput Sci"},{"key":"9989_CR21","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.ins.2015.03.048","volume":"313","author":"A M\u0119ski","year":"2015","unstructured":"M\u0119ski A, Penczek W, Rozenberg G (2015) Model checking temporal properties of reaction systems. Inf Sci 313:22\u201342","journal-title":"Inf Sci"},{"key":"9989_CR22","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.ic.2019.03.006","volume":"267","author":"A Dennunzio","year":"2019","unstructured":"Dennunzio A, Formenti E, Manzoni L, Porreca AE (2019) Complexity of the dynamics of reaction systems. Inf Comput 267:96\u2013109","journal-title":"Inf Comput"},{"key":"9989_CR23","unstructured":"Ferrando A, Malvone V (2021) Towards the verification of strategic properties in multi-agent systems with imperfect information. arXiv preprint arXiv:2112.13621"},{"key":"9989_CR24","doi-asserted-by":"crossref","unstructured":"Brodo L, Bruni R, Falaschi M (2023) Verification of reaction systems processes. In: Challenges of Software Verification, pp 243\u2013264","DOI":"10.1007\/978-981-19-9601-6_13"},{"key":"9989_CR25","doi-asserted-by":"crossref","unstructured":"M\u0119ski A, Koutny M, Penczek W (2016) Towards quantitative verification of reaction systems. In: Unconventional computation and natural computation: 15th international conference, UCNC 2016, Manchester, UK, Proceedings, pp 142\u2013154","DOI":"10.1007\/978-3-319-41312-9_12"},{"issue":"1\u20134","key":"9989_CR26","doi-asserted-by":"publisher","first-page":"289","DOI":"10.3233\/FI-2017-1567","volume":"154","author":"A M\u0119ski","year":"2017","unstructured":"M\u0119ski A, Koutny M, Penczek W (2017) Verification of linear-time temporal properties for reaction systems with discrete concentrations. Fundam Inform 154(1\u20134):289\u2013306","journal-title":"Fundam Inform"},{"issue":"2","key":"9989_CR27","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/BF00251225","volume":"47","author":"F Horn","year":"1972","unstructured":"Horn F, Jackson R (1972) General mass action kinetics. Arch Ration Mech Anal 47(2):81\u2013116","journal-title":"Arch Ration Mech Anal"},{"issue":"1","key":"9989_CR28","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0022-5193(73)90208-7","volume":"39","author":"L Glass","year":"1973","unstructured":"Glass L, Kauffman SA (1973) The logical analysis of continuous, non-linear biochemical control networks. J Theor Biol 39(1):103\u2013129","journal-title":"J Theor Biol"},{"issue":"1","key":"9989_CR29","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0304-3975(02)00136-6","volume":"287","author":"G Paun","year":"2002","unstructured":"Paun G, Rozenberg G (2002) A guide to membrane computing. Theor Comput Sci 287(1):73\u2013100","journal-title":"Theor Comput Sci"},{"key":"9989_CR30","doi-asserted-by":"crossref","unstructured":"Mart\u00edn-Vide C, Paun G, Pazos J, Rodr\u00edguez-Pat\u00f3n A (2003)  Tissue P systems.\nTheor Comput Sci 296(2): 295\u2013326","DOI":"10.1016\/S0304-3975(02)00659-X"},{"key":"9989_CR31","unstructured":"M\u0119ski A, Koutny M, Mikulski L, Penczek W (2023) Model checking for distributed reaction systems with rsCTLK (submitted)"},{"issue":"1","key":"9989_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1186\/s41236-017-0004-9","volume":"1","author":"JGT Za\u00f1udo","year":"2017","unstructured":"Za\u00f1udo JGT, Scaltriti M, Albert R (2017) A network modeling approach to elucidate drug resistance mechanisms and predict combinatorial drug treatments in breast cancer. Cancer Converg 1(1):1\u201325","journal-title":"Cancer Converg"},{"key":"9989_CR33","unstructured":"Kleijn J, Koutny M, Pietkiewicz-Koutny M, Rozenberg G (2011) Classifying boolean nets for region-based synthesis. In: Desel J, Yakovlev A (eds) Proceedings of the workshop applications of region theory 2011, Newcastle upon Tyne, UK, CEUR Workshop Proceedings, vol 725, pp 5\u201321"},{"issue":"1\u20134","key":"9989_CR34","doi-asserted-by":"publisher","first-page":"217","DOI":"10.3233\/FI-2011-539","volume":"110","author":"J Kleijn","year":"2011","unstructured":"Kleijn J, Koutny M (2011) Membrane systems with qualitative evolution rules. Fundam Inform 110(1\u20134):217\u2013230","journal-title":"Fundam Inform"},{"key":"9989_CR35","first-page":"124","volume":"9","author":"J Kleijn","year":"2014","unstructured":"Kleijn J, Koutny M, Pietkiewicz-Koutny M (2014) Tissue systems and petri net synthesis. Trans Petri Nets Other Model Concurr 9:124\u2013146","journal-title":"Trans Petri Nets Other Model Concurr"},{"key":"#cr-split#-9989_CR36.1","doi-asserted-by":"crossref","unstructured":"Kleijn J, Koutny M, Pietkiewicz-Koutny M, Rozenberg G (2012) Membrane systems and petri net synthesis. In: Ciobanu G","DOI":"10.4204\/EPTCS.100.1"},{"key":"#cr-split#-9989_CR36.2","doi-asserted-by":"crossref","unstructured":"(ed) Proceedings 6th workshop on membrane computing and biologically inspired process Calculi, MeCBIC 2012, Newcastle, UK, 8th September 2012. EPTCS, vol 100, pp 1-13","DOI":"10.4204\/EPTCS.100.0"},{"key":"9989_CR37","unstructured":"Petri CA (1973) Concepts of net theory. In: Mathematical foundations of computer science: proceedings of symposium and summer school, Strbsk\u00e9 Pleso, High Tatras, Czechoslovakia, September 3-8, 1973, pp 137\u2013146"},{"issue":"1","key":"9989_CR38","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/s00236-012-0170-2","volume":"50","author":"J Kleijn","year":"2013","unstructured":"Kleijn J, Koutny M, Pietkiewicz-Koutny M, Rozenberg G (2013) Step semantics of boolean nets. Acta Inform 50(1):15\u201339","journal-title":"Acta Inform"},{"key":"9989_CR39","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.tcs.2020.11.040","volume":"881","author":"M Koutny","year":"2021","unstructured":"Koutny M, Pietkiewicz-Koutny M, Yakovlev A (2021) Asynchrony and persistence in reaction systems. Theor Comput Sci 881:97\u2013110","journal-title":"Theor Comput Sci"},{"key":"9989_CR40","doi-asserted-by":"crossref","unstructured":"Meski A, Koutny M, Penczek W (2018) Reaction mining for reaction systems. In: Unconventional computation and natural computation - 17th international conference, UCNC 2018, Fontainebleau, France, Proceedings, pp 131\u2013144","DOI":"10.1007\/978-3-319-92435-9_10"},{"key":"9989_CR41","unstructured":"M\u0119ski A (2020) Model checking for reaction and multi-agent systems. PhD thesis, PhD thesis. Institute of Computer Science, Polish Academy of Sciences"},{"key":"9989_CR42","unstructured":"Meski A, Koutny M, Penczek W (2019) Model checking for temporal-epistemic properties of distributed reaction systems. School of Computing Technical Report Series"},{"key":"9989_CR43","unstructured":"Papadimitriou CH (1994) Computational complexity. Addison-Wesley"},{"key":"9989_CR44","doi-asserted-by":"crossref","unstructured":"Formenti E, Manzoni L, Porreca AE (2014) Cycles and global attractors of reaction systems. In: International workshop on descriptional complexity of formal systems, Springer, pp 114\u2013125","DOI":"10.1007\/978-3-319-09704-6_11"},{"key":"9989_CR45","doi-asserted-by":"crossref","unstructured":"Dennunzio A, Formenti E, Manzoni L, Porreca AE (2016) Reachability in resource-bounded reaction systems. In: International conference on language and automata theory and applications, Springer, pp 592\u2013602","DOI":"10.1007\/978-3-319-30000-9_45"},{"key":"9989_CR46","unstructured":"Baier C, Katoen J (2008) Principles of model checking. MIT Press"},{"key":"9989_CR47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-50497-0","volume-title":"Decision procedures - an algorithmic point of view","author":"D Kroening","year":"2016","unstructured":"Kroening D, Strichman O (2016) Decision procedures - an algorithmic point of view, 2nd edn. Texts in Theoretical Computer Science, An EATCS Series","edition":"2"},{"key":"9989_CR48","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of the 5th international conference on tools and algorithms for construction and analysis of systems. TACAS \u201999, pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"issue":"5","key":"9989_CR49","first-page":"1","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere A, Heljanko K, Junttila TA, Latvala T, Schuppan V (2006) Linear encodings of bounded LTL model checking. Log Methods Comput Sci 2(5):1","journal-title":"Log Methods Comput Sci"},{"key":"9989_CR50","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press"},{"key":"9989_CR51","doi-asserted-by":"crossref","unstructured":"Moura L, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: Proceedings of the 14th international conference on tools and algorithms for construction and analysis of systems. TACAS, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9989_CR52","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger TA, Vardi MY (1993) Parametric real-time reasoning. In: Proceedings of the twenty-fifth annual ACM symposium on theory of computing, San Diego, CA, USA, pp 592\u2013601","DOI":"10.1145\/167088.167242"},{"key":"9989_CR53","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52\u201353","author":"T Hune","year":"2002","unstructured":"Hune T, Romijn J, Stoelinga M, Vaandrager F (2002) Linear parametric model checking of timed automata. J Log Algebra Program 52\u201353:183\u2013220","journal-title":"J Log Algebra Program"},{"issue":"4","key":"9989_CR54","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2746337","volume":"14","author":"M Knapik","year":"2015","unstructured":"Knapik M, M\u0119ski A, Penczek W (2015) Action synthesis for branching time logic: theory and applications. ACM Trans Embedded Comput Syst 14(4):64\u201316423","journal-title":"ACM Trans Embedded Comput Syst"},{"key":"9989_CR55","unstructured":"Jones AV, Knapik M, Penczek W, Lomuscio A (2012) Group synthesis for parametric temporal-epistemic logic. In: International conference on autonomous agents and multiagent systems, AAMAS 2012, (3 Volumes), pp 1107\u20131114"}],"container-title":["Natural Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11047-024-09989-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11047-024-09989-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11047-024-09989-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,2]],"date-time":"2024-08-02T15:08:35Z","timestamp":1722611315000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11047-024-09989-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9989"],"URL":"https:\/\/doi.org\/10.1007\/s11047-024-09989-y","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-3592339\/v1","asserted-by":"object"}]},"ISSN":["1567-7818","1572-9796"],"issn-type":[{"value":"1567-7818","type":"print"},{"value":"1572-9796","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6]]},"assertion":[{"value":"18 April 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 July 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}}]}}