{'fraction_non_alphanumeric': 0.0196078431372549, 'fraction_numerical': 0.0, 'mean_word_length': 5.526315789473684, '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}}
Finite Automata and the Analysis of Infinite Transition Systems

In this tutorial, we present basic concepts and results from automata theory for the description and analysis of infinite transition systems. We introduce and discuss the classes of rational, automatic, and prefix-recognizable graphs and in each case address the question whether over such graphs the model-checking problem (with respect to natural logics) is decidable. Then we treat two different extensions of prefix-recognizable graphs, namely the graphs of the “Caucal hierarchy” and the graphs presented by ground tree rewriting systems, again with an analysis of their suitability for model-checking. This application of automata theoretic ideas helps to clarify the balance between the expressiveness of frameworks for the specification of models and the possibility to automatize verification.