Journal article 162 views 67 downloads
Scaling Invariant Generation Using State Space Embeddings and GPU Streaming
,
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)
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...
| 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 |
| 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. |
|---|---|
| Keywords: |
distributed systems, formal verification, massively parallel, reinforcement learning |
| College: |
Faculty of Science and Engineering |
| 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). |
| Issue: |
25-26 |
| Start Page: |
e70353 |