Model Checking for Probabilistic Timed Black-box Systems (S)

Probabilistic timed systems are increasingly crucial in modern system architecture.Ensuring the correctness of system behavior has become a crucial problem, and model checking offers a solution.However, it is a challenge to obtain model for black-box systems.Currently, there is a lack of model checking method for probabilistic timed black box systems.Thus, we propose a passive model learning algorithm for probabilistic timed automata, combine it with the existing framework for the model checking of probabilistic timed black-box systems.We also carried out relevant experiments and the results demonstrate the accuracy of this approach.