TEMPEST——概率环境中反应式系统与防护器的综合工具
计算机科学中的逻辑
2021-05-27 v1
摘要
我们提出 Tempest，一种综合工具，用于从概率环境中的定性或定量规约自动创建构造即正确的反应式系统与防护器。防护器是一类特殊的反应式系统，用于运行时强制实施；即，防护器在尽可能少地干扰运行系统操作的同时，强制实施该运行系统的给定定性或定量规约。强制实施定性或定量规约的防护器分别称为安全防护器或最优防护器。安全防护器可作为前置防护器或后置防护器实现，最优防护器则作为后置防护器实现。前置防护器置于系统之前并限制系统的选择。后置防护器实现于系统之后，能够覆盖系统的输出。Tempest 基于概率模型检测器 Storm，添加了针对具有安全与平均收益目标的随机博弈的模型检测算法。据我们所知，Tempest 是唯一能够在状态空间上无限制地求解具有平均收益目标的 2-1/2 博弈的综合工具。此外，Tempest 增加了综合实现反应式系统与防护器的安全策略和最优策略的功能。
引用
@article{arxiv.2105.12588,
title = {TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments},
author = {Stefan Pranger and Bettina Könighofer and Lukas Posch and Roderick Bloem},
journal= {arXiv preprint arXiv:2105.12588},
year = {2021}
}