Stationarity of a class of stochastically interconnecteil discrete-timesystems is analyzed by utilizins results from ergodic theory of general stateMarkov chains, incorporated with the so called large-scale system app...Stationarity of a class of stochastically interconnecteil discrete-timesystems is analyzed by utilizins results from ergodic theory of general stateMarkov chains, incorporated with the so called large-scale system approach.展开更多
Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyz...Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model- checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain （DTMC） that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications： a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.展开更多
The authors discuss a discrete-time Geo/G/1 retrial queue with J-vacation policy and general retrial times.As soon as the orbit is empty,the server takes a vacation.However,the server is allowed to take a maximum numb...The authors discuss a discrete-time Geo/G/1 retrial queue with J-vacation policy and general retrial times.As soon as the orbit is empty,the server takes a vacation.However,the server is allowed to take a maximum number J of vacations,if the system remains empty after the end of a vacation.If there is at least one customer in the orbit at the end of a vacation,the server begins to serve the new arrivals or the arriving customers from the orbit.For this model,the authors focus on the steady-state analysis for the considered queueing system.Firstly,the authors obtain the generating functions of the number of customers in the orbit and in the system.Then,the authors obtain the closed-form expressions of some performance measures of the system and also give a stochastic decomposition result for the system size.Besides,the relationship between this discrete-time model and the corresponding continuous-time model is also investigated.Finally,some numerical results are provided.展开更多
This paper concerns a discrete-time Geo/Geo/1 retrial queue with both positive and negative customers where the server is subject to breakdowns and repairs due to negative arrivals. The arrival of a negative customer ...This paper concerns a discrete-time Geo/Geo/1 retrial queue with both positive and negative customers where the server is subject to breakdowns and repairs due to negative arrivals. The arrival of a negative customer causes one positive customer to be killed if any is present, and simultaneously breaks the server down. The server is sent to repair immediately and after repair it is as good as new. The negative customer also causes the server breakdown if the server is found idle, but has no effect on the system if the server is under repair. We analyze the Markov chain underlying the queueing system and obtain its ergodicity condition. The generating function of the number of customers in the orbit and in the system are also obtained, along with the marginal distributions of the orbit size when the server is idle, busy or down. Finally, we present some numerical examples to illustrate the influence of the parameters on several performance characteristics of the system.展开更多
A device is subject to damage caused by environmental shocks.Shocks occur randomly indiscrete time according to a properly defined family of independent random variables.Theincremental damage caused by a shock depends...A device is subject to damage caused by environmental shocks.Shocks occur randomly indiscrete time according to a properly defined family of independent random variables.Theincremental damage caused by a shock depends on the magnitude of the shock.The device has athreshold τ and it fails once the damage exceeds the threshold.The first failure time T of the deviceand its failure rate are examined.If τ is random,under mild conditions we show that the lifedistribution properties of the random threshold are inherited by the first failure time T.For fixed τ,the conditions for the failure rate to increase or to have an increasing average are also found.Finally,as an application of the main results,the additive deterioration models are briefly discussed.展开更多
为研究塔台管制员在不同工作负荷下注视转移模式的差异,构建了模拟塔台管制的眼动试验平台,根据航班流量密度设计简单和困难2组试验。利用NASA-TLX量表评价被试者在2组试验中的工作负荷,应用离散时间马尔科夫链(discrete time Markov ch...为研究塔台管制员在不同工作负荷下注视转移模式的差异,构建了模拟塔台管制的眼动试验平台,根据航班流量密度设计简单和困难2组试验。利用NASA-TLX量表评价被试者在2组试验中的工作负荷,应用离散时间马尔科夫链(discrete time Markov chain,DTMC)计算被试者在兴趣区间的注视一步转移概率,利用SPSS软件分析2组试验中被试在各兴趣区组的注视一步转移概率差异性。结果发现:被试者的工作负荷随航班流量密度增大而增大。航班流量密度增大后,被试者在场面监视雷达区内的注视转移显著增加,由场面监视雷达区向空域监视雷达区和指令栏区的注视转移显著减少,在进程单区内的注视转移显著增加。管制员的注意力更容易向能获取更多信息的区域发生转移。展开更多
文摘Stationarity of a class of stochastically interconnecteil discrete-timesystems is analyzed by utilizins results from ergodic theory of general stateMarkov chains, incorporated with the so called large-scale system approach.
文摘Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model- checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain （DTMC） that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications： a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.
基金supported by the National Natural Science Foundation of China under Grant No.71071133
文摘The authors discuss a discrete-time Geo/G/1 retrial queue with J-vacation policy and general retrial times.As soon as the orbit is empty,the server takes a vacation.However,the server is allowed to take a maximum number J of vacations,if the system remains empty after the end of a vacation.If there is at least one customer in the orbit at the end of a vacation,the server begins to serve the new arrivals or the arriving customers from the orbit.For this model,the authors focus on the steady-state analysis for the considered queueing system.Firstly,the authors obtain the generating functions of the number of customers in the orbit and in the system.Then,the authors obtain the closed-form expressions of some performance measures of the system and also give a stochastic decomposition result for the system size.Besides,the relationship between this discrete-time model and the corresponding continuous-time model is also investigated.Finally,some numerical results are provided.
基金Supported by the National Natural Science Foundation of China(No.10871020)
文摘This paper concerns a discrete-time Geo/Geo/1 retrial queue with both positive and negative customers where the server is subject to breakdowns and repairs due to negative arrivals. The arrival of a negative customer causes one positive customer to be killed if any is present, and simultaneously breaks the server down. The server is sent to repair immediately and after repair it is as good as new. The negative customer also causes the server breakdown if the server is found idle, but has no effect on the system if the server is under repair. We analyze the Markov chain underlying the queueing system and obtain its ergodicity condition. The generating function of the number of customers in the orbit and in the system are also obtained, along with the marginal distributions of the orbit size when the server is idle, busy or down. Finally, we present some numerical examples to illustrate the influence of the parameters on several performance characteristics of the system.
基金This work was supported by grant No.1880492 from the National Natural Science Foundation of China
文摘A device is subject to damage caused by environmental shocks.Shocks occur randomly indiscrete time according to a properly defined family of independent random variables.Theincremental damage caused by a shock depends on the magnitude of the shock.The device has athreshold τ and it fails once the damage exceeds the threshold.The first failure time T of the deviceand its failure rate are examined.If τ is random,under mild conditions we show that the lifedistribution properties of the random threshold are inherited by the first failure time T.For fixed τ,the conditions for the failure rate to increase or to have an increasing average are also found.Finally,as an application of the main results,the additive deterioration models are briefly discussed.
文摘为研究塔台管制员在不同工作负荷下注视转移模式的差异,构建了模拟塔台管制的眼动试验平台,根据航班流量密度设计简单和困难2组试验。利用NASA-TLX量表评价被试者在2组试验中的工作负荷,应用离散时间马尔科夫链(discrete time Markov chain,DTMC)计算被试者在兴趣区间的注视一步转移概率,利用SPSS软件分析2组试验中被试在各兴趣区组的注视一步转移概率差异性。结果发现:被试者的工作负荷随航班流量密度增大而增大。航班流量密度增大后,被试者在场面监视雷达区内的注视转移显著增加,由场面监视雷达区向空域监视雷达区和指令栏区的注视转移显著减少,在进程单区内的注视转移显著增加。管制员的注意力更容易向能获取更多信息的区域发生转移。
