May, 2020

AMYTISS：用于大规模随机系统的并行自动控制器合成

PDF
TL;DR本文提出了一种名为 AMYTISS 的软件工具，用于为大规模随机系统设计构造正确控制器。该工具利用高性能计算平台和云计算服务解决了状况膨胀问题，并以几个案例研究来验证了其性能表现。
amytisscontroller synthesismarkov decision processesstochastic systemshigh-performance computing
发现论文，激发创造
  • 不确定性引导效率：用于随机混合系统的可扩展形式合成

    该研究旨在为线性动态的离散时间随机混合系统开发高效的抽象方法，通过不确定的 MARKOV 决策过程解决了现有形式方法的限制，可以计算精确的抽象误差，并应用于有限和无限时间范围内的合成步骤，大大缩减抽象误差，提高可缩放性。

    Jan, 2019

  • 基于形式抽象的随机和不确定动态模型自动构造控制

    自动化合成控制器，基于概率时间逻辑规范的随机动态模型，通过状态验证技术构建的 iMDP（带概率区间的马尔科夫决策过程），解决安全关键场景中面临的挑战。

    Nov, 2023

  • 具有不确定性动态的 Markov 跳跃线性系统的形式控制器综合

    该论文提出了一种使用概率计算树逻辑规范的方法来综合 Markov 跳变线性系统 (MJLS) 的控制器，该方法基于所生成的有限状态抽象，该抽象通过采样技术从 “场景方法” 中计算转换概率的区间，从而生成 MJLS 的概率上合理的近似，并将该近似评估到实际的温度控制，与空中飞行器交付问题等多个基准测试问题中。

    Dec, 2022

  • 概率不够用：针对存在认识不确定性的随机动态模型的形式控制器综合

    本文介绍一种使用区间 Markov 决策过程的抽象方式，在连续状态的模型中捕捉随机噪声和不确定参数的 aleatoric 和 epistemic 不确定性，进行控制器的综合。经实验验证，考虑 epistemic 不确定性可以提高控制器的鲁棒性。

    Oct, 2022

  • 通过正式抽象实现非高斯噪声动态系统的鲁棒控制

    该研究论文提出了一种新颖的控制器合成方法，它不需要任何明确表示噪声分布的方式，而是通过将控制系统抽象为捕捉噪声的有限状态模型，然后使用从场景方法中的工具来计算可能正确的限制，基于一些噪声的有限数量样本。通过缩小合成过程的复杂性，该方法在实际控制系统上的应用具有广泛的适用性。

    Jan, 2023

  • StocHy: 随机过程的自动验证和合成

    StocHy 是一个用于离散时间随机混合系统 (SHS) 的定量分析的软件工具，可以模拟 SHS 的演变并自动构建抽象，该抽象可用于形式验证或控制合成。

    Jan, 2019

  • Colossal-Auto：大规模模型并行化和激活检查点的统一自动化

    提出一种可同时优化分布式执行和渐进式检查点规划的系统，以支持在给定硬件上最小代码更改的情况下对模型进行并行训练，并提供易于使用的符号分析器生成任何 PyTorch 模型的内存和计算统计信息。

    Feb, 2023

  • 不确定性下的安全控制

    本文提出了一种新的逻辑 PrSTL 作为表达随机性质和强制其概率保证的表现语言，并展示了如何使用这种逻辑对具有随机性质的智能物理系统进行控制器合成，其关键特点是适应性逻辑并随着系统遇到附加数据而变化，并通过合成多种情况下无人机和自主车辆的控制器来演示我们的方法。

    Oct, 2015

  • 基于数据的安全证书的可伸缩合成及其在基于学习的控制中的应用

    本文提出了有效的技术来综合安全集合和控制律，通过基于凸优化问题的近似来提供改进的可伸缩性质，其中一种方法仅需要近似的线性系统模型和 Lipschitz 连续的未知非线性动力学，展示了数字示例，包括一个自主车队。

    Nov, 2017

  • 一种统一的云支持零散事件并行分布式仿真架构

    本文提出了一种基于 DEVS 形式主义的统一并行和分布式 M＆S 架构，具有足够的灵活性，可以在云中部署并行和分布式模拟，而无需修改底层模型源代码，并在并行实现中获得最大 15.95 倍的加速比。

    Feb, 2023