【源码】基于C++的马尔可夫决策过程反例解释工具

项目简介

本项目开发的Counterexample Explanation (Countexex) 工具，旨在对马尔可夫决策过程（MDP）中的策略进行解释和简化。它利用机器学习的决策树学习算法，将复杂的策略转化为决策树，为策略提供一种可理解、简洁的表示形式。

项目的主要特性和功能

1. 计算宽松、ε - 最优策略：在每个状态下允许选择多个等价行动，为学习算法提供更大自由度，同时会对MDP应用最大端组件（MEC）分解。
2. 计算状态重要性：通过在MDP上模拟10,000次运行，统计每个状态的访问次数，确定状态重要性，以减少无关状态。
3. 学习决策树表示：运用决策树学习算法，结合调参进一步控制决策树大小，从而获得策略的简洁表示。

安装使用步骤

前提条件

已下载本项目的源码文件。

系统要求

支持以下操作系统： - macOS（x86或ARM架构CPU） - Debian 11及更高版本 - Ubuntu 20.04及更高版本 - Arch Linux

依赖项安装

• Storm依赖
• 若使用MILP，需安装Gurobi求解器 ，Linux系统可参考此指南

复制和编译

bash cd countexex mkdir build cd build cmake.. make 若有多核CPU且内存至少8GB，可使用make -j${NUMBER_OF_CORES}加速编译。

运行

1. 检查安装是否成功： bash ./countexex -h
2. 示例执行：
   • 命令行指定参数： bash ./countexex --model "PathToCountexex/examples/cycle.nm" --propertyMax max -l 1 -d 100 -i 0.01
   • 配置文件指定参数： 先创建配置文件config.txt并指定参数： minimumGainSplit = 1e-10 minimumLeafSize = 20 importanceDelta = 0.01 再运行： bash ./countexex --model "PathToCountexex/examples/cycle.nm" --propertyMax max -c "PathToConfig/config.txt"

输出处理

决策树存储在build/app/目录下的graph.dot文件中，可使用以下命令转换为PDF： bash dot -Tpdf graph.dot -o graph.pdf

注意事项

• 模型文件需为PRISM格式，所有最终状态应为汇状态，且无变量名为 "action"。
• 仅支持可达性目标，属性需为Pmax=? [ F "goal" ]或Pmin=? [ F "goal" ]形式，目标状态需标记为 'goal'。

下载地址

点击下载 【提取码: 4003】【解压密码: www.makuang.net】