احمد تقی نژاد نیار

The verification of complex systems has traditionally relied on semi-automatic theorem-proving methods. However, model checking represents a paradigm shift by enabling automated, exhaustive verification of behavioral properties through systematic state exploration. Among advanced formal verification tools, Colored Petri Net (CPN) stands out for its integration of the ML programming language, facilitating robust model checking and system validation. Nevertheless, the application of CPN to complex systems is often constrained by the state-space explosion problem, which presents a significant challenge in contemporary research. While state-space analysis offers powerful capabilities for validation and scenario extraction, its potential remains largely untapped due to computational complexity constraints. This limitation is particularly pronounced in concurrent systems with multiple interacting variables, exemplified by game systems where intricate rule sets, deadlock conditions, and termination scenarios demand sophisticated modeling approaches. This paper presents a novel methodological framework for modeling and analyzing such game riddles, introducing methods to mitigate the state-space explosion problem. We demonstrate the efficacy of our approach through a comprehensive case study of the Merchant Ship puzzle game, though the methodology generalizes across various game typologies. By synthesizing model-checking techniques with ML-based algorithmic implementations, we develop an optimized search strategy for traversing the state space graph, enabling the derivation of quantitative complexity metrics. These metrics encompass critical indicators such as the success-to-total scenario ratio and the minimal trajectory length for both successful and unsuccessful game completions. Our research contributes to both the theoretical understanding of game complexity analysis and practical applications in game design through formal methods.

Network communication shows a variety of issues with the fast expansion of computer devices, ranging from network administration to traffic engineering. A well-known method for improving these connections is Software-Defined Networking (SDN). The SDN is a networking architecture that separates the control plane from the data plane to ease network administration. The main advantage of the SDN is the central controller. However, it has security flaws like unreachability in Distributed Denial-of-Service attacks (DDoS). Hence, defending SDN against DDoS attacks is critical. We proposed a framework for detecting DDoS attacks and a fault-tolerant method to replace faulty leader controller in distributed multi-controller SDN. We used multi-controllers architecture and leader election algorithm to present a fault-tolerant framework to select a new leader controller, in the case of a leader controller failure. In addition, an early DDoS attack detection algorithm using the entropy of destination IP addresses and the packet window initiation rate is presented. To evaluate our proposed method in various configurations, we simulated exhaustive experiments in Mininet and Floodlight. The results show that our approach outperforms similar algorithms in various network configurations and multi-victim attacks.