Abstract DiffServ was introduced by the IETF as a standard model to offer QoS across core networks. DiffServ supports a QoS feature based on differentiated traffic. So far, little interest has been shown in machine learning features in QoS. In this paper, we evaluate the effectiveness of this model in QoS in various scenarios. We show that under a heavy network load, DiffServ with... DiffServ was introduced by the IETF as a standard model to offer QoS across core networks. DiffServ supports a QoS feature based on differentiated traffic. So far, little interest has been shown in machine learning features in QoS. In this paper, we evaluate the effectiveness of this model in QoS in various scenarios. We show that under a heavy network load, DiffServ with machine learning classification (MLC) has a limited effect on the QoS parameter. Read More Read Less

Abstract This work focuses on the Datagram Congestion Control Protocol (DCCP) and its mechanisms for handling connection management, particularly in environments involving Network Address Translators (NATs). DCCP is a transport protocol designed for applications prioritizing timeliness over reliability. The study extends the Coloured Petri Net (CPN) model of DCCP's connection management procedures to incorporate the simultaneousopen procedure defined in RFC 5596. This extension addresses scenarios... This work focuses on the Datagram Congestion Control Protocol (DCCP) and its mechanisms for handling connection management, particularly in environments involving Network Address Translators (NATs). DCCP is a transport protocol designed for applications prioritizing timeliness over reliability. The study extends the Coloured Petri Net (CPN) model of DCCP's connection management procedures to incorporate the simultaneousopen procedure defined in RFC 5596. This extension addresses scenarios where both communication endpoints attempt to establish a connection simultaneously, especially when servers are behind NATs. To facilitate peer-to-peer communication through NATs, the paper explores "hole punching" techniques, which involve exchanging public IP addresses and ports via a rendezvous server before mutual connection attempts. However, modeling NAT behavior alongside DCCP procedures leads to state explosion issues. To mitigate this, the authors apply prioritized transitions and the sweep-line method to reduce computational complexity during state-space exploration. Experimental results demonstrate the effectiveness of these approaches in managing state space growth while analyzing the correctness of DCCP's simultaneous-open mechanism. Dead markings-indicating terminal states-are classified into two types: Type I represents successful connections, while Type II indicates failed attempts. Contributions include extending CPN models for DCCP analysis, addressing state explosion challenges, and validating protocol behavior under real-world constraints like NAT traversal. The work highlights formal verification's importance in ensuring reliable protocol design and offers insights into modeling complex multilayer protocols. Read More Read Less

Abstract This paper presented an optimized algorithm for computing the unfolding of Petri nets, a technique used in formal verification to combat the state-space explosion problem. The method builds upon McMillan's unfolding approach, which represents system behavior using an acyclic structure called an event net. This structure captures causal relationships between events without explicitly enumerating all reachable states. The proposed algorithm improves efficiency by dynamically... This paper presented an optimized algorithm for computing the unfolding of Petri nets, a technique used in formal verification to combat the state-space explosion problem. The method builds upon McMillan's unfolding approach, which represents system behavior using an acyclic structure called an event net. This structure captures causal relationships between events without explicitly enumerating all reachable states. The proposed algorithm improves efficiency by dynamically managing the set of potential extensions (events) during the unfolding process. It introduces a novel strategy for selecting and processing events, reducing redundant computations. The performance of the new algorithm is compared with existing tools like Punf and Mole. Experimental results indicate that the new approach achieves better time and memory efficiency while generating the same finite complete prefix, which is crucial for deadlock and reachability analysis. The paper emphasizes scalability in model checking and contributes to advancing efficient verification techniques for concurrent systems modeled as Petri nets. This work is particularly valuable for analyzing complex protocols and systems where exhaustive state exploration is computationally expensive. Read More Read Less