江西师范大学学报(自然科学版)2024,Vol.48Issue(3) :294-300,310.DOI:10.16357/j.cnki.issn1000-5862.2024.03.10

基于最大半环的DP问题函数式建模与验证

The Functional Modeling and Verification of Dynamic Programming Problems Based on Max_Semiring

王唱唱 游珍 孙欢 王昌晶
江西师范大学学报(自然科学版)2024,Vol.48Issue(3) :294-300,310.DOI:10.16357/j.cnki.issn1000-5862.2024.03.10

基于最大半环的DP问题函数式建模与验证

The Functional Modeling and Verification of Dynamic Programming Problems Based on Max_Semiring

王唱唱 1游珍 2孙欢 1王昌晶3
扫码查看

作者信息

  • 1. 江西师范大学数字产业学院,江西上饶 334000
  • 2. 江西师范大学计算机信息工程学院,江西南昌 330022;江西师范大学网络化支撑软件国家科技合作基地,江西南昌 330022
  • 3. 江西师范大学数字产业学院,江西上饶 334000;江西师范大学计算机信息工程学院,江西南昌 330022
  • 折叠

摘要

针对在DP问题算法的设计和推导中缺乏对DP问题函数式建模算法与验证的细致研究,该文首先通过深入分析最大半环与DP类问题递推关系式的对应关系,找到满足最大半环性质的一类DP问题,使用最大半环对该类DP问题进行函数式建模;然后将实现的基于最大半环的函数式建模算法与Wimmer定义的递归函数结果进行等价性验证,从而保证了函数式建模算法的正确性;最后通过对lcs问题案例分析,验证了该方法的可行性和有效性.

Abstract

Functional modeling algorithms and verification frameworks for DP issues are not thoroughly studied in the literature,which mostly concentrates on the design and derivation of algorithms for DP problems.Firstly,the re-lationship between the maximum half-loop and the recursive equation of DP issues is examined,a class of DP prob-lems that have the maximal half-loop property are identified,and then this class of DP problems using the maximal half-loop are functionally described.Secondly,in order to confirm that the functional modeling algorithm used in this study is valid,the output of Wimmer's recursive function with the maximum half-loop-based functional mode-ling technique are made equivalence checking.Finally,case examples of lcs difficulties illustrate the method's via-bility and efficacy.

关键词

DP问题/最大半环/函数式建模/验证

Key words

DP problems/max_semiring/functional modeling/formal verification

引用本文复制引用

基金项目

江西省主要学科学术与技术带头人培养项目(20232BCJ22013)

江西省自然科学基金面上项目(20212BAB202018)

江西省教育厅科技重点项目(GJJ2200302)

江西省研究生创新基金(YJS2022064)

出版年

2024
江西师范大学学报(自然科学版)
江西师范大学

江西师范大学学报(自然科学版)

CSTPCD北大核心
影响因子:0.538
ISSN:1000-5862
参考文献量3
段落导航相关论文