多区间上非线性程序的终止性判定

您当前的位置：

首页 >

文章列表页 >

多区间上非线性程序的终止性判定

信息工程 | 更新时间：2023-11-14

- 多区间上非线性程序的终止性判定
- Termination of Non-linear Programs over the Set of Intervals
- 工程科学与技术 2011年43卷第3期页码：76-80
- 作者机构：
- 作者简介：
- 基金信息：
  
  国家重点基础研究发展计划资助项目(2004CB318003)
- DOI：
  中图分类号：
- 纸质出版日期：2011，
  
  网络出版日期：2010-7-16，
扫描看全文
牟琳,李轶,李玲娜,刘栋.多区间上非线性程序的终止性判定[J].工程科学与技术,2011,43(3):76-80.

Termination of Non-linear Programs over the Set of Intervals[J]. Advanced Engineering Sciences, 2011,43(3):76-80.
牟琳,李轶,李玲娜,刘栋.多区间上非线性程序的终止性判定[J].工程科学与技术,2011,43(3):76-80. DOI：

Termination of Non-linear Programs over the Set of Intervals[J]. Advanced Engineering Sciences, 2011,43(3):76-80. DOI：

摘要

中文摘要: 主要解决了如下形式的程序的终止性判定的问题：while(x∈Ω) do {x:=f(x)} end

其中

x为程序变元，Ω(Ω=(a1

b1‖∪‖a2

b2‖∪…∪‖an

bn)，其中

‖∈{(

)

［

］}，n∈N*)是间段并集，f是一个多项式函数。证明了：当φ(b1)φ(a2)>0

…

φ(bn－1)φ(an)>0(其中

φ(x)=f(x)－x)时，这类区间上的非线性程序不终止的必要条件是：在Ω内部或者边界上存在不动点。如果不动点仅仅在Ω内部，则上述结果是充要条件。通过添加一定的约束条件，对于仅区间边界有不动点的情况，也给出了判定的方法。对一类多项式函数的终止性给出了完备性的算法（TNPSI）。

Abstract

Abstract:The solution of the following programs:while(x∈Ω) do {x:〖KG-*3〗=f(x)} end

which was called as Non linear Programs over intervals

was presented

where x was a program variable

Ω(Ω=(a1

b1‖∪‖a2

b2‖∪…∪‖an

bn)，while ‖∈{(

)

［

］}，n∈N*) was a set of intervals

and f was a polynomial function.It was proved that

when φ(b1)φ(a2)>0

…

φ(bn－1)φ(an)>0（φ(x)=f(x)－x）

the necessary condition for non-termination of the above program was that there existed fixed point within Ω or on the boundaries of Ω.Furthermore

if there were fixed points within Ω

the above condition was not only necessary but also sufficient.When all fixed points were on the boundaries of Ω

the corresponding necessary and sufficient condition of nontermination was established by introducing more constraints

and a decision algorithm for continuous polynomial function was presented.

关键词

程序验证计算机代数非线性程序不动点

Keywords

program verificationcomputer algebranonlinear programfixed point

references

Cousot P,Proving program invariance and termination by parametric abstraction,lagrangian relaxation and semidefinite programming,2005.

Yang L;Hou X R;Xia B C.A complete algorithm for automated discovering of a class of inequality type theorems[J].Sci China:Ser F,2001(1)

杨路;夏时洪.一类构造性几何不等式的机器证明[J].计算机学报,2003(7)

Xia B C;Yang L;Zhan N J,Symbolic decision procedure for termination of linear programs,Formal Aspects of Computing

李轶,程序终止性判定的代数算法研究,北京:中国科学院,2009.

Braveman M,Termination of integer linear programs,2006.

Tiwari A,Termination of linear programs,2004.

Hoare C A R,An axiomatic basis for computer programming,Communications of the ACM

Floyd R W,Assinging meanings to programs,Symphoxia in Applied Mathematics,1967.

Dijkstra E W,A discipline of programming,Prentice-Hall,Inc,1976.

姚勇.区间上非线性程序的终止性判定[J].软件学报,2010(12)doi:10.3724/SP.J.1001.2010.03722

李骏;李轶;冯勇.一类循环条件非线性的程序终止性[J].四川大学学报(工程科学版),2009(1)

Chen Y H;Xia B C;Yang L,Discovering nonlinear ranking function by solving semi-algebraic systems,2007.

Bradley A R;Manna Z;Sipma H B,Termination of polynomial prograrms,2005.

杨路;夏壁灿,不等式机器证明与自动发现,北京:科学出版社,2008.

Yang L;Zhang J Z,A practical program of automated proving for a class of geometric inequalities,2001.

Yang L;Zhou C C;Zhan N J.Recent advances in program verification through computer algebra[J].Frohtiers of Computer Science in China,2010(1)doi:10.1007/s11704-009-0074-7

更多指标>

浏览量

下载量

CNKI被引量

文章被引用时，请邮件提醒。

提交

工具集

关联资源

一类循环条件非线性的程序终止性

线性程序的Ranking函数自动合成