FAUST$^2$：不可数状态随机过程的形式抽象
系统与控制
2014-03-14 v1
摘要
FAUST 是一款软件工具，用于生成定义在不可数（连续）状态空间上的（可能是非确定性的）离散时间马尔可夫过程（dtMP）的形式抽象。dtMP 模型在 MATLAB 中指定，并被抽象为有限状态马尔可夫链或马尔可夫决策过程。抽象过程在 MATLAB 中运行，采用基于向量微积分的并行计算和快速操作。通过用户定义的由抽象过程引入的近似误差最大阈值，将抽象模型与具体 dtMP 正式建立联系。FAUST 允许将抽象模型导出到知名的概率模型检测器，如 PRISM 或 MRMC。或者，它可以在内部处理抽象模型上的 PCTL 属性（例如安全性或 reach-avoid）计算，并通过依赖于抽象过程和给定公式的量化误差，在具体 dtMP 上细化结果。该工具箱可在 http://sourceforge.net/projects/faust2/ 获取。
引用
@article{arxiv.1403.3286,
title = {FAUST$^2$: Formal Abstractions of Uncountable-STate STochastic processes},
author = {S. Esmaeil Zadeh Soudjani and C. Gevaerts and A. Abate},
journal= {arXiv preprint arXiv:1403.3286},
year = {2014}
}
备注
This paper is submitted to the 26th International Conference on Computer Aided Verification (CAV 2014)