Scaling Invariant Generation Using State Space Embeddings and GPU Streaming

Lloyd-Roberts, Ben; Pantekis, Filippos; James, Phillip; O'Reilly, Liam; Edwards, Mike

doi:10.1002/cpe.70353

Journal article 234 views 88 downloads

Scaling Invariant Generation Using State Space Embeddings and GPU Streaming

Ben Lloyd-Roberts, Filippos Pantekis

, Phillip James

, Liam O'Reilly, Mike Edwards

Concurrency and Computation: Practice and Experience, Volume: 37, Issue: 25-26, Start page: e70353

Swansea University Authors: Ben Lloyd-Roberts, Filippos Pantekis , Phillip James , Liam O'Reilly, Mike Edwards

PDF | Version of Record

© 2025 The Author(s). This is an open access article under the terms of the Creative Commons Attribution License (CC BY).
Download (5.87MB)

Check full text

DOI (Published version): 10.1002/cpe.70353

Abstract

The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its consideration of transitions from u...

Full description

Published in:	Concurrency and Computation: Practice and Experience
ISSN:	1532-0626 1532-0634
Published:	Wiley 2025
Online Access:	Check full text
URI:	https://cronfa.swan.ac.uk/Record/cronfa70761

first_indexed	2025-10-23T13:17:59Z
last_indexed	2025-10-24T18:48:39Z
id	cronfa70761
recordtype	SURis
fullrecord	<?xml version="1.0"?><rfc1807><datestamp>2025-10-23T14:20:38.9414884</datestamp><bib-version>v2</bib-version><id>70761</id><entry>2025-10-23</entry><title>Scaling Invariant Generation Using State Space Embeddings and GPU Streaming</title><swanseaauthors><author><sid>1195fd6c5ca360e99294de541c80587f</sid><firstname>Ben</firstname><surname>Lloyd-Roberts</surname><name>Ben Lloyd-Roberts</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>7e3976bc926b363ee1346c423ba74d11</sid><ORCID>0000-0001-7817-6450</ORCID><firstname>Filippos</firstname><surname>Pantekis</surname><name>Filippos Pantekis</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>fd3b15ff96c5ea91a100131abac558b6</sid><ORCID>0000-0002-4307-649X</ORCID><firstname>Phillip</firstname><surname>James</surname><name>Phillip James</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>5eca7cf79b7384130a1feef384d90508</sid><firstname>Liam</firstname><surname>O'Reilly</surname><name>Liam O'Reilly</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>684864a1ce01c3d774e83ed55e41770e</sid><ORCID>0000-0003-3367-969X</ORCID><firstname>Mike</firstname><surname>Edwards</surname><name>Mike Edwards</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-10-23</date><deptcode>MACS</deptcode><abstract>The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based 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-approximation 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-accelerated 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-kernel 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.</abstract><type>Journal Article</type><journal>Concurrency and Computation: Practice and Experience</journal><volume>37</volume><journalNumber>25-26</journalNumber><paginationStart>e70353</paginationStart><paginationEnd/><publisher>Wiley</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>1532-0626</issnPrint><issnElectronic>1532-0634</issnElectronic><keywords>distributed systems, formal verification, massively parallel, reinforcement learning</keywords><publishedDay>30</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2025</publishedYear><publishedDate>2025-11-30</publishedDate><doi>10.1002/cpe.70353</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm>SU Library paid the OA fee (TA Institutional Deal)</apcterm><funders>This work was supported by the EPSRC Center for Doctoral Training in Enhancing Human Interactions and Collaborations with Data and Intelligence Driven Systems (EP/S021892/1).</funders><projectreference/><lastEdited>2025-10-23T14:20:38.9414884</lastEdited><Created>2025-10-23T14:13:14.8954477</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Ben</firstname><surname>Lloyd-Roberts</surname><order>1</order></author><author><firstname>Filippos</firstname><surname>Pantekis</surname><orcid>0000-0001-7817-6450</orcid><order>2</order></author><author><firstname>Phillip</firstname><surname>James</surname><orcid>0000-0002-4307-649X</orcid><order>3</order></author><author><firstname>Liam</firstname><surname>O'Reilly</surname><order>4</order></author><author><firstname>Mike</firstname><surname>Edwards</surname><orcid>0000-0003-3367-969X</orcid><order>5</order></author></authors><documents><document><filename>70761__35453__2d2dc360a1514b9eb3dbb84881bed96c.pdf</filename><originalFilename>70761.VOR.pdf</originalFilename><uploaded>2025-10-23T14:16:50.2242111</uploaded><type>Output</type><contentLength>6150252</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>© 2025 The Author(s). This is an open access article under the terms of the Creative Commons Attribution License (CC BY).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>http://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling	2025-10-23T14:20:38.9414884 v2 70761 2025-10-23 Scaling Invariant Generation Using State Space Embeddings and GPU Streaming 1195fd6c5ca360e99294de541c80587f Ben Lloyd-Roberts Ben Lloyd-Roberts true false 7e3976bc926b363ee1346c423ba74d11 0000-0001-7817-6450 Filippos Pantekis Filippos Pantekis true false fd3b15ff96c5ea91a100131abac558b6 0000-0002-4307-649X Phillip James Phillip James true false 5eca7cf79b7384130a1feef384d90508 Liam O'Reilly Liam O'Reilly true false 684864a1ce01c3d774e83ed55e41770e 0000-0003-3367-969X Mike Edwards Mike Edwards true false 2025-10-23 MACS The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based 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-approximation 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-accelerated 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-kernel 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. Journal Article Concurrency and Computation: Practice and Experience 37 25-26 e70353 Wiley 1532-0626 1532-0634 distributed systems, formal verification, massively parallel, reinforcement learning 30 11 2025 2025-11-30 10.1002/cpe.70353 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University SU Library paid the OA fee (TA Institutional Deal) This work was supported by the EPSRC Center for Doctoral Training in Enhancing Human Interactions and Collaborations with Data and Intelligence Driven Systems (EP/S021892/1). 2025-10-23T14:20:38.9414884 2025-10-23T14:13:14.8954477 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ben Lloyd-Roberts 1 Filippos Pantekis 0000-0001-7817-6450 2 Phillip James 0000-0002-4307-649X 3 Liam O'Reilly 4 Mike Edwards 0000-0003-3367-969X 5 70761__35453__2d2dc360a1514b9eb3dbb84881bed96c.pdf 70761.VOR.pdf 2025-10-23T14:16:50.2242111 Output 6150252 application/pdf Version of Record true © 2025 The Author(s). This is an open access article under the terms of the Creative Commons Attribution License (CC BY). true eng http://creativecommons.org/licenses/by/4.0/
title	Scaling Invariant Generation Using State Space Embeddings and GPU Streaming
spellingShingle	Scaling Invariant Generation Using State Space Embeddings and GPU Streaming Ben Lloyd-Roberts Filippos Pantekis Phillip James Liam O'Reilly Mike Edwards
title_short	Scaling Invariant Generation Using State Space Embeddings and GPU Streaming
title_full	Scaling Invariant Generation Using State Space Embeddings and GPU Streaming
title_fullStr	Scaling Invariant Generation Using State Space Embeddings and GPU Streaming
title_full_unstemmed	Scaling Invariant Generation Using State Space Embeddings and GPU Streaming
title_sort	Scaling Invariant Generation Using State Space Embeddings and GPU Streaming
author_id_str_mv	1195fd6c5ca360e99294de541c80587f 7e3976bc926b363ee1346c423ba74d11 fd3b15ff96c5ea91a100131abac558b6 5eca7cf79b7384130a1feef384d90508 684864a1ce01c3d774e83ed55e41770e
author_id_fullname_str_mv	1195fd6c5ca360e99294de541c80587f_*_Ben Lloyd-Roberts 7e3976bc926b363ee1346c423ba74d11__Filippos Pantekis fd3b15ff96c5ea91a100131abac558b6__Phillip James 5eca7cf79b7384130a1feef384d90508__Liam O'Reilly 684864a1ce01c3d774e83ed55e41770e_**_Mike Edwards
author	Ben Lloyd-Roberts Filippos Pantekis Phillip James Liam O'Reilly Mike Edwards
author2	Ben Lloyd-Roberts Filippos Pantekis Phillip James Liam O'Reilly Mike Edwards
format	Journal article
container_title	Concurrency and Computation: Practice and Experience
container_volume	37
container_issue	25-26
container_start_page	e70353
publishDate	2025
institution	Swansea University
issn	1532-0626 1532-0634
doi_str_mv	10.1002/cpe.70353
publisher	Wiley
college_str	Faculty of Science and Engineering
hierarchytype
hierarchy_top_id	facultyofscienceandengineering
hierarchy_top_title	Faculty of Science and Engineering
hierarchy_parent_id	facultyofscienceandengineering
hierarchy_parent_title	Faculty of Science and Engineering
department_str	School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str	1
active_str	0
description	The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based 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-approximation 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-accelerated 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-kernel 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.
published_date	2025-11-30T05:33:40Z
_version_	1856896416442482688
score	11.096068

Scaling Invariant Generation Using State Space Embeddings and GPU Streaming

Similar Items