{'fraction_non_alphanumeric': 0.02040816326530612, 'fraction_numerical': 0.0, 'mean_word_length': 4.94949494949495, '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}}
Model Checking Games for CTL

We define model checking games for the temporal logic CTL∗ and prove their correctness. They provide a technique for using model checking interactively in a verification/specification process. Their main feature is to construct paths in a transition system stepwise. That enables them to be the basis for a local model checking algorithm with a natural notion of justification. However, this requires configurations of a game to contain sets of formulas. Moreover, an additional structure on these sets, called focus, has to be used to guarantee correctness.