学位论文 > 优秀研究生学位论文题录展示

微分几何和排队论中若干问题的研究及计算机实现

作　者: 韩玉群
导　师: 梁希泉
学　校: 青岛科技大学
专　业: 应用数学
关键词: 排队论 Mizar语言输入率服务率智能化证明
分类号: O226
类　型: 硕士论文
年　份: 2013年
下　载: 3次
引　用: 0次
阅　读: 论文下载

内容摘要

排队论在科学技术与国民经济的发展中起了重要的作用,也是通信,计算机等领域的专家学者必不可少的数学工具,当前排队服务系统的输入率与服务率依赖系统状态等相关问题受到学者的广泛关注,于是深入研究排队论中若干问题以及实现排队论复杂问题的计算机逻辑证明,成为当今研究的重要课题。Mizar语言系统是用于证明数学问题的一种语言系统,在数学命题的自动推理与证明的过程中逐步发展与完善。现在Mizar系统可智能化实现逻辑证明,复杂计算,校验排版等,并拥有世界上最大的数据库MML。本文首先对排队论以及Mizar语言系统进行了简单描述,然后对输入率和服务率依赖状态的排队模型进行了详细探讨,在此基础上,详细计算并给出了衡量排队论的重要指标,利用数学问题自动推理系统Mizar,以及微分几何知识,对排队论中的更新过程等问题进行了Mizar智能化推理,并且通过了系统验证。本文主要的工作如下：1、考虑输入率和服务率依赖系统状态,对M/M/s/K模型讨论了服务率可变的情形；对M/M/c模型同时考虑服务率和输入率可变的情形；对M/M/c/m+K/m模型考虑服务率可变的情形；对两个服务台串联模型考虑服务率可变的情形。对以上四个问题,本文都给出了严格的数学证明,并对每个模型进行深入研究,论证了系统的平稳分布,并得出系统中顾客的平均输入率,系统的平均服务强度,系统顾客的损失等衡量排队论性能的重要指标。2、首次用Mizar语言证明排队论问题,结合微分几何理论中微分差分等Grassmann代数理论,实现了排队论中几个问题的Mizar智能化推导证明。

全文目录

摘要  3-4
ABSTRACT  4-6
目录  6-9
1 绪论  9-14
  1.1 排队论起源  9-10
  1.2 数学问题计算机证明的发展现状及微分方面的发展近况  10-12
  1.3 用计算机自动证明排队论的意义  12
  1.4 本文主要研究的内容  12-14
2 排队论与计算机语言  14-25
  2.1 排队论预备知识  14-19
    2.1.1 排队系统描述  14-16
    2.1.2 排队系统记号  16-17
    2.1.3 排队系统指标  17
    2.1.4 排队论中有关概念  17-19
  2.2 MIZAR语言  19-25
    2.2.1 MIZAR文章结构  19-21
    2.2.2 MIZAR语言的数据类型和关键字  21-22
    2.2.3 MIZAR语言系统的定理证明的基本方法  22-23
    2.2.4 MIZAR语言的逻辑推理检验与优化  23-25
3 服务率可变的M/M/S/K模型研究  25-37
  3.1 M/M/S/K模型介绍  25
  3.2 模型假设  25-26
  3.3 状态转移图  26-27
  3.4 平稳分布  27-30
  3.5 主要指标  30-33
    3.5.1 统损失的概率  30
    3.5.2 平均损失顾客数  30
    3.5.3 进入系统的顾客数  30-31
    3.5.4 平均队长  31-32
    3.5.5 等待时间与逗留时间  32-33
  3.6 本章小结  33-37
    3.6.1 模型比较  33-34
    3.6.2 实例验证  34-37
4 一种服务率可变的串联排队服务系统研究  37-47
  4.1 模型假设  37-38
  4.2 马尔可夫过程  38
  4.3 服务台之间无排队位置的服务系统  38-42
    4.3.1 系统状态转移分析  38-40
    4.3.2 系统平衡方程  40
    4.3.3 系统指标分析  40-42
  4.4 服务台之间有排队位置的服务系统  42-46
    4.4.1 系统状态转移分析  42-44
    4.4.2 系统平衡方程  44-45
    4.4.3 系统指标分析  45-46
  4.5 本章小结  46-47
5 输入率与服务率依赖状态的M/M/C排队模型研究  47-55
  5.1 模型假设以及符号说明  47-48
  5.2 数学模型  48-49
  5.3 平稳分布  49-52
  5.4 主要指标  52-53
    5.4.1 顾客的平均输入率  52
    5.4.2 系统的平均服务强度  52
    5.4.3 平均队长  52
    5.4.4 服务机构繁忙率  52-53
    5.4.5 系统的损失概率  53
  5.5 本章小结  53-55
6 维修时间可变的有备用品的M/M/C/M+K/M模型研究  55-63
  6.1 问题叙述及假设  55-56
  6.2 维修工人数小于备用品的情形  56-59
    6.2.1 故障的机器数  56-58
    6.2.2 重要的指标  58-59
  6.3 维修工人数大于备用品的情形  59-61
    6.3.1 故障的机器数  59-60
    6.3.2 重要的指标  60-61
  6.4 本章小结  61-63
7 排队论中涉及微分的命题及其计算机实现  63-76
  7.1 微分几何中有关问题的介绍  63-68
    7.1.1 积分形式的转化原理  63-64
    7.1.2 多变量积分中的积分微元代换公式  64-65
    7.1.3 四个重要积分公式的同意描述  65-68
    7.1.4 Mizar数据库MML中关于微分几何方面的研究  68
  7.2 更新过程  68-69
  7.3 排队论基础问题的MIZAR实现  69-75
    7.3.1 环境部设置  69-70
    7.3.2 排队论中微分差分问题的MIZAR实现  70-75
  7.4 最终实现的MIZAR形式  75-76
总结与展望  76-77
参考文献  77-80
致谢  80-81
攻读学位期间发表的学术论文目录  81-82

微分几何和排队论中若干问题的研究及计算机实现

内容摘要

全文目录

相似论文