时态逻辑及其在决策系统中的应用

时态逻辑及其在决策系统中的应用第一页，共二十五页，编辑于2023年，星期三

断言推理1目录

时态逻辑

2

SIDSS系统描述

3

系统实现4

总结

5第二页，共二十五页，编辑于2023年，星期三

断言推理1Pre→Post由这样的断言推理为核心组织的产生式系统在决策支持系统、专家系统中使用得最多，也是最为成熟的解决方案但是语义是静态的当遇到诸如动态的、实时的、并发的或具有其他时态特性的推理时，这种静态的推理方式则有很大的缺陷时态逻辑断言推理则可有效地弥补这方面出现的难题。第三页，共二十五页，编辑于2023年，星期三

时态逻辑2时态逻辑（tenselogic）是非经典逻辑的分支学科其研究对象是:

把含有时态动词的语句形式化

把含有这种语句的推理系统化引入以下常见的时态逻辑操作符：

Next:

ΟA,IfAandBareformulaethenΟA

Always:

□A,AlwaysinthefutureA

Sometimes:

A,SometimesinthefutureA

Until:

AUB,AuntilB

Since:

ASB,AsinceB

After:

AΠB,BafterA第四页，共二十五页，编辑于2023年，星期三

系统描述3智能工资决策支持系统（SIDSS）是由刘冬宁、汤庸等人自主开发的一个典型的时态信息系统目前已有6000多家机关事业单位用户针对我国机关事业单位工资政策复杂性、地域性和时间性等主要特点应用时态数据和知识处理技术解决了根据机关事业单位工作人员随时间变化影响工资变动的信息（时态性数据），依据相应时期的工资政策（时态知识库）自动确定工资的问题第五页，共二十五页，编辑于2023年，星期三3.1SIDSS中的时态特征根据我国国情，工资政策繁杂，随时间变动大在复杂的规则、高时态信息变动的条件下如何确保工资确定的正确性成了SIDSS中的重点和难点涉及到了大量的断言推理与时态信息处理

系统描述3第六页，共二十五页，编辑于2023年，星期三简单地以工资政策中“两年优秀晋升”的政策为例该政策在1999年以前的描述是这样的：

如果人员连续两年考核优秀，或某年考核优秀有“一年优”标志，工资档次允许晋升一档，考核结果有效年份从下年算起，但连续两次晋升之间必须相隔两年以上。在1999年以后的描述则改为：

其他与之前相同，但连续两次晋升之间必须相隔四年以上。举例说明：

人员A从1995年到2000年的考核均为优秀，则他可以分别在1997年和1999年执行一次工资档次晋升，而不允许在2001年执行档次晋升，正是由于1999年以后的工资政策规定，2001年与1999年之间并未相隔4年以上，因此不能进行晋升

系统描述3第七页，共二十五页，编辑于2023年，星期三表1人员A工资晋升随时间的变化年份考核结果执行操作政策依据1995优秀

1999年以前的“两年优晋升”相隔必须两年以上1996优秀1997年允许晋升一档1997优秀

1998优秀1999年允许晋升一档1999优秀

1999年以后的“两年优晋升”相隔必须四年以上2000优秀2001年不允许晋升一档

系统描述3第八页，共二十五页，编辑于2023年，星期三3.2规则描述在“人员越级晋升”的过程中，会遇到的各种规则本文中仅以1999年更改政策一项规则变更为基准其规则、条件、动作的相关表如下：

系统描述3第九页，共二十五页，编辑于2023年，星期三规则规则名规则说明起始条件表达式规则生命周期R1越级晋升用于处理1999年以前考核结果引起的越级晋升C1[1993/10,1998/12]R2越级晋升用于处理1999年以后考核结果引起的越级晋升C2[1999/1,NOW]表2越级晋升规则表

系统描述3第十页，共二十五页，编辑于2023年，星期三表3越级晋升条件表条件条件THENELSEC1连续两年考核结果优秀C3NULLC2连续两年考核结果优秀C4NULLC3当前年份—上次越级晋升年份>=2或以前从未越级晋升A1NULLC4当前年份—上次越级晋升年份>=4或以前从未越级晋升A1NULL

系统描述3第十一页，共二十五页，编辑于2023年，星期三表4越级晋升动作表动作动作NEXTA1人员工资档次加一档NULL表2~4中，是关于“越级晋升”这一事件涉及到的规则、条件和动作。从表中可以看到这样的规则、条件、动作具有断言推理的特征，而其中在规则表中，定义的生命周期，更体现了时态变更性的特点，同时这一系列的判断推理都具有强时序性，鉴于对推理的正确性应引入时态逻辑断言推理。

系统描述3第十二页，共二十五页，编辑于2023年，星期三4.1时态逻辑断言规则的设计根据表2~4，设计执行规则如下：（S1）WhenReceivePromotingApplication

Then_DoTimeVerificationAnd_ThenCondictionChecking（S2）WhenCondictionChecking

Then_DoPromotionExecuting在执行规则中体现出了较强的时间序列性（1）接到越级晋升的请求后，先判断系统时间，根据规则的生命周期挑出该使用的条件序列判断；（2）完成匹配条件序列判断嵌套；（3）执行动作。

系统实现4第十三页，共二十五页，编辑于2023年，星期三进一步细化这些执行序列：（S3）WhenCondictionChecking

IfInvalidCondiction

Then_DoNext_CondictionChecking

UntilEndofLayer_CondictionChecking在条件判断嵌套过程中，当前条件得不到匹配时，则轮转到下一条件进行匹配，直到该层所有条件判断完毕即判断嵌套完成

系统实现4第十四页，共二十五页，编辑于2023年，星期三（S4）WhenCondictionChecking

IfEndofLayer_CondictionChecking

Then_DoRejectPromotingApplication在条件判断嵌套过程中，当前条件得不到匹配和该层所有条件又判断完毕时，则表示不符合越级晋升的条件，不通过该处理（S5）WhenNotInvalidCondiction

Then_DoNextLayer_CondictionCheckingUntilEndofAll_CondictionCheckingAnd_ThenPromotionExecute在条件判断嵌套中，当前条件匹配成功则递进到下一层条件判断，如所有条件没有判断完毕则继续进行判断嵌套直到嵌套完毕，如嵌套完毕而条件匹配又成功则执行晋升动作

系统实现4第十五页，共二十五页，编辑于2023年，星期三4.2对断言规则的逻辑描述对（S1）、（S2）逻辑描述如下：（S6）receive(SIDSS,Promoting_Application)=>verify(SIDSS,System_Time)Πcheck(SIDSS,Condiction)其中“Π”表示After，AΠB，意为BafterA。（S7）check(SIDSS,Condiction)=>act(SIDSS,Promotion)

系统实现4第十六页，共二十五页，编辑于2023年，星期三对（S3）-（S5）逻辑描述如下：（S8）check(SIDSS,Condiction)∧┑match(SIDSS,Condiction)=>samelayer_check(SIDSS,Condiction)Uend_check(Condiction,Layer)其中“U”在这里代表Until。（S9）┑match(SIDSS,Condiction)Πend_check(Condiction,Layer)=>reject(SIDSS,Promoting_Application)（S10）match(SIDSS,Condiction)=>(nextlayer_check(SIDSS,Condiction)Uend_check(Condiction,All))Πact(SIDSS,Promotion)

系统实现4第十七页，共二十五页，编辑于2023年，星期三4.3对规则生命周期的时态逻辑表示不仅可以对推理规则进行时态逻辑断言设计以及逻辑推理，还可对规则的生命周期也用时态逻辑进行扩展。引入时态因子Ti时态因子状态T1表示时间T2表示时间表5时态因子表

系统实现4第十八页，共二十五页，编辑于2023年，星期三因此对规则R1和R2的表示分别为：（1）AlwaysR1SinceT1UntilT2（2）AlwaysR2SinceT2用时态逻辑运算符表示为：（1）□((R1ST1)UT2)（2）□(R2ST1)

系统实现4第十九页，共二十五页，编辑于2023年，星期三4.4Java实现根据上述时态逻辑断言，可以在代码中实现上述规则断言。调用TimeRoverInc.的TemporalRover工具它是一种用于处理Java程序中时态逻辑断言并根据断言生成有效Java代码的工具，并可以配备数据库表的工具DBRover同时使用。

系统实现4第二十页，共二十五页，编辑于2023年，星期三给出断言规则（S6）-（S7）的Java伪代码如下所示：S6:receivePromoting_Applicationimplies{Next{{checkCondiction}Until{verifySystemTime}}};S7:Always{{matchCondiction}implies{Next{actPromotion}}};

系统实现4第二十一页，共二十五页，编辑于2023年，星期三给出断言规则（S8）~（S10）的Java伪代码如下所示：S8:If!{matchCondiction}implies{Next{{checkNext_Condiction}UntilEmpty{CondictionofthisLayer}}};S9:IfEmpty{CondictionofthisLayer}implies{Next!{actPromotion}};S10:If{matchCondiction}implies{Next{{{checkNextLayor_Condiction}UntilEmpty{AllCondictions}}implies{Next{actPromotion}}};

系统实现4第二十二页，共二十五页，编辑于2023年，星期三对时态规则生命周期：（1）□((R1ST1)UT2)（2）□(R2ST1)给出Java伪代码如下所示：（1）Always{{

R1SinceT1

}UntilT2

};（2）Always{

R2SinceT1

};