Study On Some Issues Of The Queuing Theory And Differential Geometry And Computer Implementation

Queuing theory has been an essential mathematical tool for experts and scholars engaged in communications, computer and other fields, and queuing service system of the input rate and service rate depend on the state of the system has received widespread attention, more in-depth study knowledge of queuing theory and realization of complex problems’ computer logic proof, become an important research topic today.The Mizar system is used to demonstrate math problems on computer, and it is being gradually improved as the automatic proof. Nowadays, Mizar system can intelligent achieves logical proof and complex calculation and typesetting and so on, and Mizar system has the largest date library of MML in the world.First, this paper briefly describe knowledge of queuing theory and Mizar system, then discuss some queuing models of input rate and service rate depends on the state in detail. Calculate some important indicators of queuing theory. Based on the mathematical theorem automatic reasoning system, using differential geometry knowledge, achieve Mizar intelligent proof about some problem of queuing theory, and through the system verification. This paper’ highlights and main work as follows:1. Consider the input rate and the service rate depend on the state of the system. For the model of M/M/s/K, we only consider service rate depends on the state; For the model of M/M/c/, we consider both service rate and input rate depend on the state; For the model of M/M/c/m+K/m, we only consider the service rate depends on the state; For the model of series connection of two service station, we only consider the service rate depends on the state. In-depth study of each model and demonstrate the stationary distribution of the system, obtain some important indicators of queuing such as the average customer input rate, the average service strength and the loss of customer and so on.2.For the first time using Mizar language proves queuing problems, combining the theory of differential geometry, implements some basic issues use Mizar system and realize intelligent deduction.