{'fraction_non_alphanumeric': 0.010624169986719787, 'fraction_numerical': 0.0, 'mean_word_length': 5.130081300813008, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, '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}}
Completeness of Partial Deduction for Coverability Problems of Petri Nets

In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper characterises some classes of problems which can be decided by this approach. In particular, we show that a restricted form of partial deduction is already powerful enough to decide all coverability properties of Petri Nets. We also prove that two particular instances of partial deduction can be used to exactly compute the Karp-Miller tree as well as Finkel’s minimal coverability set. We thus establish a quite surprising link between algorithms for Petri nets and logic program specialisation.