公开(公告)号：CN111553539A

公开(公告)日：2020-08-18

申请号：CN202010387663.9

申请日：2020-05-09

Applicant: 上海大学 ,  上海上大海润信息系统有限公司

Inventor： 高洪皓 ,  黄婉秋 ,  施建刚 ,  周琳 ,  邱彬洋

IPC: G06Q10/04 ,  G08G1/01 ,  G06F30/18

Abstract: 本发明涉及一种基于概率模型检验的行驶路径规划方法，包括以下步骤：对智能交通系统的交通路网结构进行特征提取，构建交通网络有向图；根据预先统计的交通路网的车流数据，获取概率车流关系；构建基于马尔可夫链的交通系统车辆行为模型；构建基于概率标签迁移系统的PCTL公式，对交通系统车辆行为模型各路径进行性质检验；在概率模型检验软件中对交通系统车辆行为模型进行建模，并对各PCTL公式进行验证，得到检验结果；判断检验结果是否超过预设的路径可达性阈值，若是，则推荐对应的路径，否则不推荐。与现有技术相比，本发明考虑交通道路中复杂多变的阻抗因素，具有可靠性和准确性高等优点。

公开(公告)号：CN113673680B

公开(公告)日：2023-09-15

申请号：CN202110957915.1

申请日：2021-08-20

Applicant: 上海大学 ,  上海上大海润信息系统有限公司

Inventor： 高洪皓 ,  戴宝斌 ,  周琳 ,  施建刚 ,  陈洁

IPC: G06N3/0475 ,  G06N3/045 ,  G06N3/094 ,  G06F18/241 ,  G06F18/214

Abstract: 本发明涉及一种通过对抗网络自动生成验证性质的模型验证方法和系统，方法包括通过生成器自动获取验证性质，采用正则表达式并基于CTL语法对获取的验证性质进行语法校验后，用于进行模型验证；生成器的训练过程包括：获取采用计算树时序逻辑公式CTL描述的验证性质；将其转换成能被生成对抗网络所能识别的输入形式，作为训练数据；构建生成对抗网络，该生成对抗网络包括生成器和判别器，生成器的输入为随机噪声，判别器的输入为生成器生成的数据和训练数据，判别器输出期望奖励用于更新生成器的参数；采用对抗式训练的方法迭代地训练生成器和判别器，直至达到收敛。与现有技术相比，本发明能够实现高效且自动生成验证性质，支持提高模型验证的效率。

公开(公告)号：CN113673680A

公开(公告)日：2021-11-19

申请号：CN202110957915.1

申请日：2021-08-20

Applicant: 上海大学 ,  上海上大海润信息系统有限公司

Inventor： 高洪皓 ,  戴宝斌 ,  周琳 ,  施建刚 ,  陈洁

IPC: G06N3/04 ,  G06N3/08 ,  G06K9/62

Abstract: 本发明涉及一种通过对抗网络自动生成验证性质的模型验证方法和系统，方法包括通过生成器自动获取验证性质，采用正则表达式并基于CTL语法对获取的验证性质进行语法校验后，用于进行模型验证；生成器的训练过程包括：获取采用计算树时序逻辑公式CTL描述的验证性质；将其转换成能被生成对抗网络所能识别的输入形式，作为训练数据；构建生成对抗网络，该生成对抗网络包括生成器和判别器，生成器的输入为随机噪声，判别器的输入为生成器生成的数据和训练数据，判别器输出期望奖励用于更新生成器的参数；采用对抗式训练的方法迭代地训练生成器和判别器，直至达到收敛。与现有技术相比，本发明能够实现高效且自动生成验证性质，支持提高模型验证的效率。