{'fraction_non_alphanumeric': 0.024125452352231604, 'fraction_numerical': 0.0012062726176115801, 'mean_word_length': 4.763888888888889, '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}}
A First-Order Extension of Modal μ- calculus

Modal μ-calculus is a modal logic with fixed-point operators and well-known in mathematics and computer scince. For example, many verification properties of a system are expressed by formulas of modal μcalculus in computer science. However some verification properties of a system can not be expressed by a formula of modal μ-calculus as we will show later, and quantifiers of first-order logic are essentially required for expressing the verification properties. Therefore a first-order extension of modal μ-calculus is needed for expressing such verification properties. In this paper we introduce a first-order extension of modal μ-calculus and show that it is Σ 1 -complete. Moreover we express some verification properties of a system by its formulas for showing its usefulness.