{'fraction_non_alphanumeric': 0.02214022140221402, 'fraction_numerical': 0.0, 'mean_word_length': 5.074626865671642, '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}}
Formal Modeling and Verification of Multi-agent System Based on Timed Automata

The safety and credibility of the safety-critical systems is a research problem that has received wide attention. Introducing the theory of multi-agent systems into the research of safety-critical systems is very important. In this paper, the characteristics of the multi-agent system and the interaction between agents are considered, and the use of Time Automata to formally model and verify the multi-agent system is proposed. Finally, taking the Radio Block Center (RBC) scenario in the train control system as an example, the proposed method is introduced in detail. The results show that the method proposed in this paper has particular reference significance for the safety and credibility research of safety-critical systems.