强化学习,特别是近些年兴起的深度强化学习在很多领域中都成功地获得了应用。但与此同时,由于强化学习中安全性保障机制的缺乏,人们对其安全性的担忧和需求也日益强烈,使得强化学习难以应用于智能安全攸关系统中。在智能体所处的环境中充满了各种不确定因素,仅仅依靠最大化长期回报的策略学习方式难以应对系统中的各种风险。此外,环境中的信息扰动也为智能体的安全决策带来了很大的干扰,威胁着智能体和其所处的物理环境的安全。形式化方法基于严谨的数学理论为安全攸关系统的安全性保障提供了可信的理论和工具支持。但已有的形式化方法并不能很好地适用于智能体所要应对的复杂环境。本文针对强化学习的安全性问题和已有方法的不足,借助于形式化建模与验证理论和工具,提出了一种通用的安全强化学习方法,采用运行时验证的方式为强化学习提供安全性保障。本文的主要工作包括:（1）提出了概率时距计算树逻辑（Probabilistic interval Computation Tree Logic,Pi CTL）,并形式化地定义了其语法语义,以用于对不确定的实时系统进行系统属性/约束的描述。此外,在PRISM的基础上进行二次开发,实现了对Pi CTL公式的验证。（2）提出一种安全学习算法,称之为基于监视器的安全控制（Generic Safe Control with Supervisor,GSCS）,将形式化验证与强化学习有机结合起来,将安全性约束转化为算法所学习到的策略的一部分。基于形式化验证的控制监视器实时监控系统状态,对智能体的决策进行安全性验证,当且仅当该决策将会使系统发生危险时对系统的运行进行干预。此外,对存在信息扰动的系统,本文引入了安全阈值的概念,监视器采取最大安全策略尽可能将风险最小化。（3）以汽车自适应巡航系统为蓝本,设计了一个基于Open AI Gym框架的模拟评估环境,基于双深度Q网络（Double Deep Q-network,DDQN）构建了一个智能体。利用该环境,评估了GSCS算法在不同实验条件下的表现,并与经典的强化学习算法相比较,证明了GSCS算法的可行性和有效性。