Efficient Graph Monte Carlo Hopcroft–Karp Hungarian Neural Network for Analyzing Büchi Automata

Büchi Automata models verify the systems with infinite sequences, which is crucial for formal verification, program synthesis, and model checking of reactive systems, wherein the analysis struggles with accurate verification. Hence, Graph Monte Carlo Bidirectional Hopcroft–Karp Hungarian Neural Network (GMBHN) is proposed to analyze Buchi automata properties. During the automata analysis, loop with asymmetric transition dependencies and self-reinforcing nondeterministic loops creates delays in the acceptance conditions and selecting the same state subsets, which leads to false convergence, and leaves a vast area unverified. To mitigate this, Monte Carlo Tree Bidirectional Long Short-Term Memory(MCT-BLSTM) is employed in GNN’s first hidden layer, which traces all probable execution routes based on probabilistic weight assignments while learning asymmetric patterns for verifying acceptance. Moreover, micro-phase misalignment from asymmetric transition delays, independent event clocks, or unseen microstate dependencies induces phantom livelocks trapping the system in oscillatory cycles and nonconverging state trajectories, causing verification failures. Thus, Hopcroft-Karp Hungarian algorithm(HKHA) is integrated in GNN’s second layer for mapping optimal states and optimizing assignments, thereby reducing livelocks. Additionally, the non-deterministic Buchi automata (NBW) execute multiple runs for the same input due to state ambiguity, overlapping acceptance conditions, or conflicting transition priorities, which complicates universality verification. The proposed GMBHN tackles this issue by universality-based ranking of the possible execution paths, which is refined by eliminating redundant transitions, thereby satisfying the acceptance conditions. Experimental evaluations showed higher classification accuracy of 98% and precision of 97%, proving its higher performance in Büchi Automata analysis with accurate misleading loops detection.