On the use of MTBDDs for performability analysis and verification of stochastic systems

This paper describes how to employ multi-terminal binary decision diagrams (MTBDDs) for the construction and analysis of a general class of models that exhibit stochastic, probabilistic and non-deterministic behaviour. It is shown how the notorious problem of state space explosion can be circumvented by compositionally constructing symbolic (i.e. MTBDD-based) representations of complex systems from small-scale components. We emphasise, however, that compactness of the representation can only be achieved if heuristics are applied with insight into the structure of the system under investigation. We report on our experiences concerning compact representation, performance analysis and verification of performability properties.     

Parametric probabilistic transition systems for system design and analysis

We develop a model of parametric probabilistic transition Systems (PPTSs), where probabilities associated with transitions may be parameters. We show how to find instances of the parameters that satisfy a given property and instances that either maximize or minimize the probability of reaching a certain state. As an application, we model a probabilistic non-repudiation protocol with a PPTS. The theory we develop allows us to find instances that maximize the probability that the protocol ends in a fair state (no participant has an advantage over the others). A preliminary version of this paper was presented at SEFM’04 [LMT04]. 05 April 2006     

Dynamic vehicle allocation control for automated material handling system in semiconductor manufacturing

The current study examines the dynamic vehicle allocation problems of the automated material handling system (AMHS) in semiconductor manufacturing. With the uncertainty involved in wafer lot movement, dynamically allocating vehicles to each intrabay is very difficult. The cycle time and overall tool productivity of the wafer lots are affected when a vehicle takes too long to arrive. In the current study, a Markov decision model is developed to study the vehicle allocation control problem in the AMHS. The objective is to minimize the sum of the expected long-run average transport job waiting cost. An interesting exhaustive structure in the optimal vehicle allocation control is found in accordance with the Markov decision model. Based on this exhaustive structure, an efficient algorithm is then developed to solve the vehicle allocation control problem numerically. The performance of the proposed method is verified by a simulation study. Compared with other methods, the proposed method can significantly reduce the waiting cost of wafer lots for AMHS vehicle transportation.     

Performance sensitivities for parameterized Markov systems

It is known that the performance potentials (or equivalently, perturbation realization factors) can be used as building blocks for performance sensitivities of Markov systems. In parameterized systerns, the changes in parameters may only affect some states, and the explicit transition probability matrix may not be known. In this paper, we use an example to show that we can use potentials to construct performance sensitivities m a more flexible way; only the potentials at the affected states need to be estimated, and the transition probability matrix need not be known. Policy iteration algorithms, which are simpler than the standard one, can be established.     

Performance analysis of two-loop closed production systems

A production line with a limited number of carts or pallets is regarded as a closed loop manufacturing system. Such production lines are very useful in various manufacturing systems, such as semiconductor production systems. In this paper, we study a two-loop closed production system by means of block-structured Markov chains, and propose an effective RG-factorization solution to evaluate performance measures of the system, including throughput and WIP level. Based on this, the system can be numerically analyzed with respect to several crucial parameters. This leads to improvement on the design of the carts quantities, which are always crucial factors in closed-loop production lines.     

Algebraic reasoning for probabilistic action systems and while-loops

Back and von Wright have developed algebraic laws for reasoning about loops in a total correctness framework using the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems and probabilistic while-loops. In particular we focus on developing data refinement rules for these two constructs. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible.     

A component-based simulation environment for statistical process control systems analysis

This paper describes a simulation environment, called Prosim, which permits a user to define components, subsystems, and their interconnections to analyse a statistical process control (SPC) system. The components and systems are defined and analysed interactively. A library of standard SPC objects containing models for the Xbar, range, exponential weighted moving average, p-chart and other SPC techniques have been created which help define the control application. The PC-based tool is tested on theoretical, and real data, and is useful for the design and trouble shooting of a manufacturing system. It is also an effective teaching and research tool.     

Encouraging probabilistic thinking

Abstract  This paper reports on research which indicates the weak understanding of tree diagrams of pupils aged 11–16 years and describes a computer program which seeks to overcome this, allowing the pupil to construct and analyse a simulated channel system down which balls may be rolled.     

激励学习的最优判据研究

激励学习智能体通过最优策略的学习与规划来求解序贯决策问题,因此如何定义策略的最优判所是激励学习研究的核心问题之一,本文讨论了一系列来自动态规划的最优判据,通过实例检验了各种判据对激励学习的适用性和优缺点,分析了设计各种判据的激励学习算法的必要性。     

Performance analysis of probabilistic timed automata using digital clocks

Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a modelling formalism suitable for describing formally both nondeterministic and probabilistic aspects of real-time systems, and is amenable to model checking against probabilistic timed temporal logic properties. However, the previously developed verification algorithms either suffer from high complexity, give only approximate results, or are restricted to a limited class of properties. In the case of classical (non-probabilistic) timed automata it has been shown that for a large class of real-time verification problems correctness can be established using an integral model of time (digital clocks) as opposed to a dense model of time. Based on these results we address the question of under what conditions digital clocks are sufficient for the performance analysis of probabilistic timed automata and show that this reduction is possible for an important class of systems and properties including probabilistic reachability and expected reachability. We demonstrate the utility of this approach by applying the method to the performance analysis of three probabilistic real-time protocols: the dynamic configuration protocol for IPv4 link-local addresses, the IEEE 802.11 wireless local area network protocol and the IEEE 1394 FireWire root contention protocol.

Optimization of a PH/PH/1/N Queue with Controllable Service Time and Partial Information

We study a queueing system where both inter-arrival and service times are distributed according to phase-type distributions. This system is modeled as a Markov decision process with full and partial information. The objective is to minimize the long-run average cost of the system. Numerical results are presented.     

Polynomial-time probabilistic observability analysis of sampled-data piecewise affine systems

This paper proposes a polynomial-time probabilistic approach to solve the observability problem of sampled-data piecewise affine systems. First, an algebraic characterization for the system to be observable is derived. Next, based on the characterization, we propose a randomized algorithm that can determine if the system is observable in a probabilistic sense or the system is not observable in a deterministic sense. Finally, it is shown with some examples, for which it is hopeless to check the observability in a deterministic way, that the proposed algorithm is very useful.     

Impact of demand correlation and information sharing in a capacity constrained supply chain with multiple-retailers

This paper considers a single product, two-echelon capacity constrained supply chain consisting of a supplier and two retailers facing correlated end-item demand. We use a decentralized Markov decision process with restricted observations to represent this system and conduct a numerical study to quantify the benefits of information sharing to the retailers under varying levels of supplier capacity and supply allocation mechanisms. Our results show an inverse relationship between capacity and information and indicate the retailers can achieve significant benefits as a result of the information sharing partnership.     

效用驱动的Markov强化学习

对智能体Q强化学习方法进行了扩展,讨论效用驱动的Markov强化学习问题。与单吸收状态相比,学习过程不再是状态驱动,而是效用驱动的。智能体的学习将不再与特定的目标状态相联系,而是最大化每步的平均期望收益,即最大化一定步数内的收益总和,因此学习结果是一个平均收益最大的最优循环。证明了多吸收状态下强化学习的收敛性,将栅格图像看作具有多个吸收状态的格子世界,测试了确定性环境下多吸收状态Q学习的有效性。     

连续时间Markov决策过程互模拟等价及逻辑保持

模型检测中,Markov决策过程可以建模具有不确定性的系统,然而状态空间爆炸问题将会影响系统验证的成败与效率,互模拟等价可以用于系统状态的简约.在强互模拟关系的基础上,给出Markov决策过程模型弱互模拟等价关系的概念,导出了连续时间Markov决策过程及其内嵌离散时间Markov决策过程互模拟等价关系的内在联系;在强互模拟等价关系逻辑特征保持的基础上,给出弱互模拟等价关系下的逻辑保持性质,证明了弱互模拟等价的两个状态,同时满足除下一步算子外的连续随机逻辑公式,从而可以将原模型中的验证问题转换为简约后模型的验证问题,提高验证的效率.     

Performance of ARQ-protocols for HDX-transmission in hierarchical polling systems

Two different ARQ-protocols are analyzed for half-duplex transmission between a primary station and an arbitrary number of polled secondary stations. The protocols differ in the retransmission scheme after error detection of transmitted frames (packets): immediate retransmission or retransmission within the next polling cycle. Both cases are modeled by a multi-queue, single server system with feedback, batch arrival processes, general service (transmission and overhead) times, and cyclic interqueue discipline. Both queueing models are analyzed through an imbedded Markov chain on the basis of an independence assumption for the cycle times. The analysis yields explicit results for the Laplace-Stieltjes transforms and averages of the packet delay and interdeparture times as functions of the most important design parameters as number of stations, load, arrival clusters, packet length, overhead (control, change of transmission direction), error rate, and retransmission schemes. Some numerical results are given which show the influences of these parameters on the system performance.