{'fraction_non_alphanumeric': 0.029312288613303268, 'fraction_numerical': 0.004509582863585118, 'mean_word_length': 5.3428571428571425, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Reachability analysis of protocols with FIFO channels

In a complete protocol design process, it is often important to validate the protocol for general correctness properties such as boundedness, deadlock absence, and well-formedness. However, for any general protocol modeled as a number of communicating finite state machines with unbounded FIFO channels, the above properties are known to be undecidable [Brand81a, Brand80a]. In this paper we demonstrate the decidability of those properties for a class of protocols, called <i>well-ordered</i> protocols. We introduce an algorithm for constructing a finite reachability tree for any given protocol with FIFO channels and show that by using this reachability tree, one can decide whether any given protocol is well-ordered, and if it is well-ordered whether it has an unbounded channel, a state deadlock, or an unspecified reception.