近年来，基于模型的性质验证方法已经发展到定量验证阶段。在系统建模框架和性质规范语言的描述能力方面，定量验证方法相对于原有的模型检测方法均有了提升，使基于模型的验证方法的应用扩展到了DNA计算、微电网管理等更广泛的领域。然而，已有的基于模型的定量验证方法中缺少用于开放型系统空间属性验证的建模框架、规范语言以及相应的自动验证算法，也未实现知识前提和系统其它性质的统一定量验证。本文的工作将围绕上述问题展开，研究针对多主体模型中空间属性、知识前提及概率性质的定量验证方法。多主体模型也可称为多主体系统，其包含一组可交互的智能主体，主要用于对可以与环境进行交互的开放性系统进行建模。本文的主要工作是研究用于验证多主体模型中空间属性、知识前提以及概率性质的定量验证方法。在本文中，作者将对上述验证方法的建模框架、时态逻辑语言、验证算法以及验证工具软件展开研究，并基于概率时间自动机的定量验证方法来设计通用航空飞行计划管理方案。在研究过程中，构建可对系统空间属性、知识前提和随机行为进行抽象的多主体模型，定义能够定量描述多主体模型中空间属性、知识前提以及概率性质的时态逻辑语言和设计相应的验证算法是本文工作的核心，具体工作论述如下：本文提出了一种可对多主体模型中主体自身空间属性、主体与主体间的空间变化关系以及系统概率性质进行检测的定量验证方法。文中对该验证方法的表示逻辑、建模框架以及验证算法进行了研究：将度量逻辑MS[M]中描述空间距离关系的距离算子引入代价概率交替时态逻辑定义了概率空间时态逻辑，该逻辑是一种可对系统的空间属性进行描述的规范语言；为对主体的空间、时间信息进行建模，构建了多主体概率时空博弈模型；通过引入连续马尔可夫链的路径概率计算结构，定义了一种用于计算概率时空博弈模型路径概率的概率度量结构；设计了用来确立系统模型是否满足概率空间时态逻辑的以路径概率计算为核心的自动验证算法；设计和实现了支持上述定量验证方法的概率模型验证工具ST-PRISM。在实例研究中，使用上述定量验证方法对小型机场空管系统的飞行程序进行了建模，并得出了在确保安全飞行间隔的前提下，飞机成功降落到指定区域的最大、最小概率以及飞机完成降落的用时。针对知识前提和系统其它性质的统一定量验证问题，本文提出了一种基于概率交替时态认知逻辑的定量验证方法。该方法是对基于交替时态认知逻辑的验证方法的扩展，其将策略理论结合到认知模型中来描述状态迁移的不确定性，引入相应概率分布到认知模型中来描述系统的随机特性，并能够给出量化的验证结果，实现了对开放型系统中知识前提的定量验证。本文对上述验证方法的模型结构、性质描述逻辑以及自动验证算法三个组成部分均进行了研究：提出了用于对开放型系统建模的多主体概率认知博弈结构和基于回合的多主体概率认知博弈结构；定义了描述系统知识前提等性质的概率交替时态认知逻辑；设计了与验证概率空间时态逻辑算法类似的用来确立系统模型是否满足逻辑的以路径概率计算为核心的自动验证算法。基于概率交替时态认知逻辑的定量验证方法通过将知识算子及其是否被满足的结果定义成原子命题实现了对知识前提和系统其它性质的统一定量验证。在实例研究中，基于上述定量验证方法再次对小型机场空管系统飞行程序进行了建模，得出飞机降落过程中飞行员能够获取空管指令和飞行态势信息的概率。本文提出了一种基于概率时间自动机的通用航空飞行计划管理方案设计方法。本文提出的基于概率时间自动机的通用航空飞行计划管理方案设计方法在通用航空飞行计划管理方案初步设计后，依据单向业务流原则将方案分解为多个业务子单元。之后，使用概率时间自动机对子单元业务流程进行建模，同时基于概率时间逻辑描述方案子单元业务流程需满足的概率性质和时间约束。再之后，基于模型检测算法自动检测子单元的业务流程模型是否满足由概率时间逻辑公式描述的性质，并指出不满足性质时的模型中存在的问题，给出修改建议。在完成对子单元的验证后，使用同样的验证方法对整体流程进行性质验证和给出修改建议，最终目的是设计出能够适合我国通用航空产业发展的通用航空飞行计划管理方案。