StocHy：随机过程的自动化验证与综合
系统与控制
2024-12-20 v1 系统与控制
摘要
StocHy 是一个用于对离散时间随机混合系统（SHS）进行定量分析的软件工具。StocHy 接受随机模型的高层描述并构建等价的 SHS 模型。该工具允许（i）在给定时间范围内模拟 SHS 演化；并自动构建 SHS 的形式化抽象。抽象随后被用于（ii）形式化验证或（iii）控制（策略、战略）综合。StocHy 允许模块化建模，并具有独立的模拟、验证和综合引擎，它们作为独立库实现。这使得库易于使用且易于构建扩展。该工具用 C++ 实现，并采用基于矢量微积分的操作、稀疏矩阵的使用、概率核的符号化构建以及多线程。实验表明，与现有基于抽象的方法相比，StocHy 的性能显著改善：特别地，StocHy 在精度（抽象误差）和计算代价方面优于最先进工具，并最终实现对大型模型（12 个连续维度）的可扩展性。StocHy 可在 www.gitlab.com/natchi92/StocHy 获取。
引用
@article{arxiv.1901.10287,
title = {StocHy: automated verification and synthesis of stochastic processes},
author = {Nathalie Cauchi and Kurt Degiorgio and Alessandro Abate},
journal= {arXiv preprint arXiv:1901.10287},
year = {2024}
}