Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its Challenges
State-space graphs and automata serve as fundamental tools for modeling and analyzing the behavior of computational systems. Recurrent neural networks (RNNs) and language models are deeply intertwined, as RNNS provide the foundational architecture that enables language models to process sequential d...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2025-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10993355/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849715219336527872 |
|---|---|
| author | Chanon Dechsupa Teerapong Panboonyuen Wiwat Vatanawood Praisan Padungweang Chakchai So-In |
| author_facet | Chanon Dechsupa Teerapong Panboonyuen Wiwat Vatanawood Praisan Padungweang Chakchai So-In |
| author_sort | Chanon Dechsupa |
| collection | DOAJ |
| description | State-space graphs and automata serve as fundamental tools for modeling and analyzing the behavior of computational systems. Recurrent neural networks (RNNs) and language models are deeply intertwined, as RNNS provide the foundational architecture that enables language models to process sequential data, capture contextual dependencies, and improve natural language processing tasks. Both RNNs and state-space graphs help evaluate discrete-time systems within this formal framework. However, the basic question of their equivalence remains an open challenge regarding the models governing sentence structure in natural language and the formal model in automata theory. In this paper, we present ENGRU (Enhanced Gated Recurrent Units), a novel deep learning-based approach for formal verification. ENGRU integrates concepts of model checking techniques, Colored Petri Nets (CPNs), and sequential learning to analyze systems at a high level of abstraction. CPN models undergo state-space enumeration via a model-checking tool, generating a state-space graph and an automaton from inherent state transition patterns. These graphs are transformed into sequential representations as sub-paths, enabling ENGRU to learn the execution paths and predict system behaviors. ENGRU effectively predicts goal states within discrete-time models by the competency of gated recurrent mechanisms, encouraging early bug detection and allowing predictive state-space exploration. Experimental results demonstrate that ENGRU’s ability achieves high accuracy and efficiency in goal state predictions. The source code for ENGRU is available at (<uri>https://github.com/kaopanboonyuen/ENGRU</uri>). |
| format | Article |
| id | doaj-art-ea0cf6b3e5294367b44c9a4b0ec902f8 |
| institution | DOAJ |
| issn | 2169-3536 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj-art-ea0cf6b3e5294367b44c9a4b0ec902f82025-08-20T03:13:29ZengIEEEIEEE Access2169-35362025-01-0113843578437910.1109/ACCESS.2025.356819410993355Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its ChallengesChanon Dechsupa0https://orcid.org/0000-0001-8441-8962Teerapong Panboonyuen1https://orcid.org/0000-0001-8464-4476Wiwat Vatanawood2https://orcid.org/0000-0003-0457-3474Praisan Padungweang3https://orcid.org/0000-0002-4358-7927Chakchai So-In4https://orcid.org/0000-0003-1026-191XDepartment of Computer Science, College of Computing, Khon Kaen University, Khon Kaen, ThailandDepartment of Computer Engineering, Faculty of Engineering, Chulalongkorn University, Bangkok, ThailandDepartment of Computer Engineering, Faculty of Engineering, Chulalongkorn University, Bangkok, ThailandDepartment of Computer Science, College of Computing, Khon Kaen University, Khon Kaen, ThailandDepartment of Computer Science, College of Computing, Khon Kaen University, Khon Kaen, ThailandState-space graphs and automata serve as fundamental tools for modeling and analyzing the behavior of computational systems. Recurrent neural networks (RNNs) and language models are deeply intertwined, as RNNS provide the foundational architecture that enables language models to process sequential data, capture contextual dependencies, and improve natural language processing tasks. Both RNNs and state-space graphs help evaluate discrete-time systems within this formal framework. However, the basic question of their equivalence remains an open challenge regarding the models governing sentence structure in natural language and the formal model in automata theory. In this paper, we present ENGRU (Enhanced Gated Recurrent Units), a novel deep learning-based approach for formal verification. ENGRU integrates concepts of model checking techniques, Colored Petri Nets (CPNs), and sequential learning to analyze systems at a high level of abstraction. CPN models undergo state-space enumeration via a model-checking tool, generating a state-space graph and an automaton from inherent state transition patterns. These graphs are transformed into sequential representations as sub-paths, enabling ENGRU to learn the execution paths and predict system behaviors. ENGRU effectively predicts goal states within discrete-time models by the competency of gated recurrent mechanisms, encouraging early bug detection and allowing predictive state-space exploration. Experimental results demonstrate that ENGRU’s ability achieves high accuracy and efficiency in goal state predictions. The source code for ENGRU is available at (<uri>https://github.com/kaopanboonyuen/ENGRU</uri>).https://ieeexplore.ieee.org/document/10993355/Model checkingcolored petri netstate-space analysisGRU attentionformal verification |
| spellingShingle | Chanon Dechsupa Teerapong Panboonyuen Wiwat Vatanawood Praisan Padungweang Chakchai So-In Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its Challenges IEEE Access Model checking colored petri net state-space analysis GRU attention formal verification |
| title | Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its Challenges |
| title_full | Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its Challenges |
| title_fullStr | Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its Challenges |
| title_full_unstemmed | Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its Challenges |
| title_short | Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its Challenges |
| title_sort | toward ai augmented formal verification a preliminary investigation of engru and its challenges |
| topic | Model checking colored petri net state-space analysis GRU attention formal verification |
| url | https://ieeexplore.ieee.org/document/10993355/ |
| work_keys_str_mv | AT chanondechsupa towardaiaugmentedformalverificationapreliminaryinvestigationofengruanditschallenges AT teerapongpanboonyuen towardaiaugmentedformalverificationapreliminaryinvestigationofengruanditschallenges AT wiwatvatanawood towardaiaugmentedformalverificationapreliminaryinvestigationofengruanditschallenges AT praisanpadungweang towardaiaugmentedformalverificationapreliminaryinvestigationofengruanditschallenges AT chakchaisoin towardaiaugmentedformalverificationapreliminaryinvestigationofengruanditschallenges |