{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T09:10:10Z","timestamp":1762938610885,"version":"3.45.0"},"reference-count":61,"publisher":"Wiley","issue":"25-26","license":[{"start":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T00:00:00Z","timestamp":1761091200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/S021892\/1"],"award-info":[{"award-number":["EP\/S021892\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["onlinelibrary.wiley.com"],"crossmark-restriction":true},"short-container-title":["Concurrency and Computation"],"published-print":{"date-parts":[[2025,11,30]]},"abstract":"<jats:title>ABSTRACT<\/jats:title>\n                  <jats:p>The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction\u2010based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its consideration of transitions from unreachable safe states to unsafe states. Invariants that reduce the state space to an over\u2010approximation of reachable states, excluding transitions from safe to unsafe states, can help remove these false positives. However, such invariants are difficult to deduce automatically. In previous work, we have demonstrated that reinforcement learning (RL) and descriptive statistics can be used to generate candidate invariants, trivially within small programs, and can be realistically scaled to industrial settings using hardware\u2010accelerated implementations. This paper extends our hybrid approach that uses General Purpose Graphics Processing Units (GPGPUs) to overcome these challenges while scaling effortlessly horizontally and in a distributed manner. We detail the implementation of a three\u2010kernel pipeline responsible for consuming streamed data and computing correlation coefficients. Finally, we present a breadth of time samples that highlight the performance and scalability of this approach.<\/jats:p>","DOI":"10.1002\/cpe.70353","type":"journal-article","created":{"date-parts":[[2025,10,23]],"date-time":"2025-10-23T01:19:44Z","timestamp":1761182384000},"update-policy":"https:\/\/doi.org\/10.1002\/crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Scaling Invariant Generation Using State Space Embeddings and GPU Streaming"],"prefix":"10.1002","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4628-8295","authenticated-orcid":false,"given":"Ben","family":"Lloyd\u2010Roberts","sequence":"first","affiliation":[{"name":"Department of Computer Science Swansea University  Swansea UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7817-6450","authenticated-orcid":false,"given":"Filippos","family":"Pantekis","sequence":"additional","affiliation":[{"name":"Department of Computer Science Swansea University  Swansea UK"}]},{"given":"Phillip","family":"James","sequence":"additional","affiliation":[{"name":"Department of Computer Science Swansea University  Swansea UK"}]},{"given":"Liam","family":"O'Reilly","sequence":"additional","affiliation":[{"name":"Department of Computer Science Swansea University  Swansea UK"}]},{"given":"Michael","family":"Edwards","sequence":"additional","affiliation":[{"name":"Department of Computer Science Swansea University  Swansea UK"}]}],"member":"311","published-online":{"date-parts":[[2025,10,22]]},"reference":[{"key":"e_1_2_11_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1995.521887"},{"key":"e_1_2_11_3_1","first-page":"141","volume-title":"Modelling and Verification of Relay Interlocking Systems","author":"Haxthausen A.","year":"2008"},{"key":"e_1_2_11_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.015"},{"key":"e_1_2_11_5_1","first-page":"1","article-title":"Automatically Verifying Railway Interlockings Using SAT\u2010Based Model Checking","volume":"35","author":"James P.","year":"2011","journal-title":"Electronic Communications of the EASST"},{"key":"e_1_2_11_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_2_11_7_1","first-page":"253","volume-title":"Verification of Solid State Interlocking Programs","author":"James P.","year":"2013"},{"key":"e_1_2_11_8_1","first-page":"205","volume-title":"Applied Bounded Model Checking for Interlocking System Designs","author":"Haxthausen A.","year":"2013"},{"key":"e_1_2_11_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0304-7"},{"key":"e_1_2_11_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33951-1_10"},{"key":"e_1_2_11_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66197-1_15"},{"key":"e_1_2_11_12_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603007"},{"key":"e_1_2_11_13_1","first-page":"125","volume-title":"NORMA: A Tool for the Analysis of Relay\u2010Based Railway Interlocking Systems","author":"Amendola A.","year":"2022"},{"key":"e_1_2_11_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.2009147"},{"volume-title":"Mining Invariants From State Space Observations","year":"2022","author":"Lloyd\u2010Roberts B.","key":"e_1_2_11_15_1"},{"key":"e_1_2_11_16_1","first-page":"1","volume-title":"Improving Railway Safety: Human\u2010In\u2010The\u2010Loop Invariant Finding","author":"Lloyd\u2010Roberts B.","year":"2023"},{"key":"e_1_2_11_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CANDAR64496.2024.00017"},{"volume-title":"IEC 61131\u20133: Programming Industrial Automation Systems","year":"2010","author":"Tiegelkamp M.","key":"e_1_2_11_18_1"},{"key":"e_1_2_11_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_11_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_23"},{"key":"e_1_2_11_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_80"},{"key":"e_1_2_11_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_11_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020\u20100190(82)90022\u20109"},{"volume-title":"Reinforcement Learning: An Introduction","year":"2018","author":"Sutton R.","key":"e_1_2_11_24_1"},{"key":"e_1_2_11_25_1","first-page":"331","volume-title":"Markov Decision Processes","author":"Puterman M.","year":"1990"},{"key":"e_1_2_11_26_1","first-page":"387","volume-title":"Deterministic Policy Gradient Algorithms","author":"Silver D.","year":"2014"},{"key":"e_1_2_11_27_1","first-page":"15931","volume-title":"Learning to Utilize Shaping Rewards: A New Approach of Reward Shaping","author":"Hu Y.","year":"2020"},{"key":"e_1_2_11_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390156.1390240"},{"key":"e_1_2_11_29_1","unstructured":"V.Mnih K.Kavukcuoglu D.Silver et al. \u201cPlaying Atari With Deep Reinforcement Learning \u201d(2013) https:\/\/arxiv.org\/abs\/1312.5602."},{"key":"e_1_2_11_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0925-2312(93)90006-O"},{"key":"e_1_2_11_31_1","unstructured":"V.Mnih A. P.Badia M.Mirza et al. \u201cAsynchronous Methods for Deep Reinforcement Learning \u201d2016arXiv preprint arXiv:1602.01783."},{"key":"e_1_2_11_32_1","unstructured":"J.Schulman F.Wolski P.Dhariwal A.Radford andO.Klimov \u201cProximal Policy Optimization Algorithms \u201d(2017) https:\/\/arxiv.org\/abs\/1707.06347."},{"key":"e_1_2_11_33_1","article-title":"The Phi\u2010Coefficient, the Tetrachoric Correlation Coefficient, and the Pearson\u2010Yule Debate","author":"Ekstr\u00f6m J.","year":"2011","journal-title":"UCLA Department of Statistics"},{"key":"e_1_2_11_34_1","article-title":"Exploration: A Study of Count\u2010Based Exploration for Deep Reinforcement Learning","volume":"30","author":"Tang H.","year":"2017","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_2_11_35_1","doi-asserted-by":"crossref","unstructured":"C.Gordillo J.Bergdahl K.Tollmar andL.Gissl\u00e9n \u201cImproving Playtesting Coverage via Curiosity Driven Reinforcement Learning Agents \u201d(2021) https:\/\/arxiv.org\/abs\/2103.13798.","DOI":"10.1109\/CoG52621.2021.9619048"},{"key":"e_1_2_11_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63307-3_73"},{"key":"e_1_2_11_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-15-4095-0_15"},{"key":"e_1_2_11_38_1","first-page":"13550","article-title":"Heuristic\u2010Guided Reinforcement Learning","volume":"34","author":"Cheng C. A.","year":"2021","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_2_11_39_1","unstructured":"A.Aubret L.Matignon andS.Hassas \u201cA Survey on Intrinsic Motivation in Reinforcement Learning \u201d(2019) https:\/\/arxiv.org\/abs\/1908.06976."},{"key":"e_1_2_11_40_1","first-page":"1479","volume-title":"Unifying Count\u2010Based Exploration and Intrinsic Motivation","author":"Bellemare M. G.","year":"2016"},{"key":"e_1_2_11_41_1","unstructured":"J.Schulman S.Levine P.Moritz M. I.Jordan andP.Abbeel \u201cTrust Region Policy Optimization \u201d(2017) https:\/\/arxiv.org\/abs\/1502.05477."},{"key":"e_1_2_11_42_1","unstructured":"A. V.Clemente H. N.Castej\u00f2n andA.Chandra \u201cEfficient Parallel Methods for Deep Reinforcement Learning \u201d(2017) https:\/\/arxiv.org\/abs\/1705.04862."},{"key":"e_1_2_11_43_1","unstructured":"D.Horgan J.Quan D.Budden et al. \u201cDistributed Prioritized Experience Replay \u201d(2018) https:\/\/arxiv.org\/abs\/1803.00933."},{"key":"e_1_2_11_44_1","doi-asserted-by":"publisher","DOI":"10.1201\/b15072"},{"issue":"11","key":"e_1_2_11_45_1","first-page":"2579","article-title":"Visualizing Data Using t\u2010SNE","volume":"9","author":"Maaten V. d. L.","year":"2008","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_11_46_1","unstructured":"D.M\u00fcllner \u201cModern Hierarchical Agglomerative Clustering Algorithms \u201d(2011) https:\/\/arxiv.org\/abs\/1109.2378."},{"volume-title":"Introduction","year":"2022","author":"Peddie J.","key":"e_1_2_11_47_1"},{"key":"e_1_2_11_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108855273"},{"key":"e_1_2_11_49_1","doi-asserted-by":"publisher","DOI":"10.3390\/app10113711"},{"key":"e_1_2_11_50_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.8004"},{"key":"e_1_2_11_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703\u2010023\u201000432\u2010z"},{"key":"e_1_2_11_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/LDAV.2017.8231847"},{"key":"e_1_2_11_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2833179.2833189"},{"key":"e_1_2_11_54_1","unstructured":"NVIDIA Corporation \u201cNVIDIA Ampere GA102 GPU Architecture. Whitepaper NVIDIA; 2788 San Tomas Expressway Santa Clara CA. 95050 \u201d2020."},{"key":"e_1_2_11_55_1","unstructured":"NVIDIA Corporation \u201cParallel Thread Execution ISA Version 8.8 \u201d(2025) https:\/\/web.archive.org\/web\/20250510202712\/https:\/\/docs.nvidia.com\/cuda\/parallel\u2010thread\u2010execution\/index.html."},{"key":"e_1_2_11_56_1","unstructured":"NVIDIA Corporation \u201cCUDA Binary Utilities 12.5 \u201d(2025) https:\/\/web.archive.org\/web\/20250415174228\/https:\/\/docs.nvidia.com\/cuda\/cuda\u2010binary\u2010utilities\/."},{"key":"e_1_2_11_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2019.8661186"},{"key":"e_1_2_11_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPEC55821.2022.9926299"},{"key":"e_1_2_11_59_1","unstructured":"J.Zhe M.Marco S.Benjamin andP. S.Daniele \u201cDissecting the NVIDIA Volta GPU Architecture via Microbenchmarking \u201d(2018) https:\/\/arxiv.org\/abs\/1804.06826."},{"key":"e_1_2_11_60_1","unstructured":"Z.Jia M.Maggioni J.Smith andD. P.Scarpazza \u201cDissecting the NVidia Turing T4 GPU via Microbenchmarking \u201d(2019) https:\/\/arxiv.org\/abs\/1903.07486."},{"key":"e_1_2_11_61_1","first-page":"213","volume-title":"Dissecting the CUDA Scheduling Hierarchy: a Performance and Predictability Perspective","author":"Olmedo I. S.","year":"2020"},{"key":"e_1_2_11_62_1","unstructured":"NVIDIA Corporation \u201cCUDA C++ Programming Guide Release 12.9 \u201d(2025) https:\/\/web.archive.org\/web\/20250505133403\/https:\/\/docs.nvidia.com\/cuda\/cuda\u2010c\u2010programming\u2010guide\/."}],"container-title":["Concurrency and Computation: Practice and Experience"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/cpe.70353","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T09:05:22Z","timestamp":1762938322000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/cpe.70353"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,22]]},"references-count":61,"journal-issue":{"issue":"25-26","published-print":{"date-parts":[[2025,11,30]]}},"alternative-id":["10.1002\/cpe.70353"],"URL":"https:\/\/doi.org\/10.1002\/cpe.70353","archive":["Portico"],"relation":{},"ISSN":["1532-0626","1532-0634"],"issn-type":[{"type":"print","value":"1532-0626"},{"type":"electronic","value":"1532-0634"}],"subject":[],"published":{"date-parts":[[2025,10,22]]},"assertion":[{"value":"2025-05-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-04","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"e70353"}}