{'fraction_non_alphanumeric': 0.03148854961832061, 'fraction_numerical': 0.003816793893129771, 'mean_word_length': 5.4753086419753085, '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}}
The Demand for Reliability in Probabilistic Verification

For formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results. First we present an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. This motivates the investigation at which points inaccuracies are introduced during the model checking process. We then give ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential problems: (1) to introduce a “degree of belief” for each sub-formula, (2) to use exact (rational) arithmetic, (3) to use interval arithmetic to obtain safe approximations of the actual probabilities, and (4) to provide certificates which testify that the result is correct.