The Study Of Approximate ω-Regular Languages Based On Metric Theory

The reliability and security of computer hardware and software systems are directly related to the usability of the whole computer system.Formal method was proposed to guarantee the reliability and security of the system.Formal method is a method to describe,develop and analyzes computer hardware and software systems based on strict mathematical basis.Model checking has become one of the most effective automation techniques to analyze the correctness of software and hardware system designs.Formal languages and automaton theory,as the theoretical basis of model checking,can transform models into mathematical systems for extended research.As the computer system becomes increasingly large and complex,the actual system is endowed with uncertain behavior characteristics,so only qualitative analysis can no longer effectively deal with the uncertain or inconsistent information of the system.The combination of classical formal languages and automaton with metric theory is helpful to evaluate system uncertainty behavior more accurately.Aiming at the important regular languages and ω-regular languages in formal languages,there is no corresponding formal definition when they are extended to the metric background.At the same time,combined with the concept of distance in metric theory,describing the relationship between languages and automaton can accurately describe the system behavior and evaluate the satisfaction degree between the system behavior and the given specification more accurately.Based on metric theory,this paper studies the generalization of regular languages and ω-regular languages as well as the properties after the generalization and the characterization of automaton.The main work is as follows:1.Based on the concept of pseudo-metric in metric theory,the regular languages andω-regular languages in formal languages are quantitatively expanded,and the good properties of classical formal languages are retained as much as possible.First,based on the concepts of classical regular languages and ω-regular languages,the definitions of approximate regular languages and approximate ω-regular languages are generalized.Secondly,according to the closure of classical regular languages and ω-regular languages about regular operations,it is proved that approximate regular languages and approximateω-regular languages have the same closure about regular operations.2.Based on the traditional Büchi automaton,a metric Büchi automaton is defined by introducing pseudo-metric and distance threshold α,and the acceptance conditions are redefined to approximate the acceptance languages.Then the definition of infinite strings and languages as well as the distance between two languages is given to measure the acceptance relationship between Büchi automaton and input languages.3.The relationship between approximate ω-regular languages and metric Büchi automaton is studied.Based on the metric Büchi automaton,the proposed approximate ω-regular languages is described,and the equivalence between the approximate ω-regular languages and the metric Büchi automaton is proved.