線性時序邏輯在失業(yè)保險審計中的應用研究.pdf

1、在社會保險審計的過程中，理解被審計地區(qū)的法規(guī)和業(yè)務流程是非常重要的環(huán)節(jié)。各地的法規(guī)政策是開展業(yè)務的基礎，根據(jù)法規(guī)政策來構建當?shù)氐臉I(yè)務模型也是理解業(yè)務的有效手段。目前，模型檢測的方法很多，線性時序邏輯已經受到廣泛的關注，并且已經應用到模型檢測中。
　　 本文根據(jù)法規(guī)政策的文本描述，構建當?shù)氐臉I(yè)務工作流程。依據(jù)時間序列上業(yè)務事件發(fā)生的時間不同，對構建的業(yè)務模型進行化簡、完備失業(yè)保險業(yè)務處理流程模型等操作。基于有限狀態(tài)自動機的失業(yè)保險

2、業(yè)務處理流程模型構建完畢后，應用線性時序邏輯對模型的時序性質加以描述，針對該時序描述，應用線性時序邏輯語言編寫程序，程序作為模型檢測輸入的一部分。本文提取失業(yè)保險法規(guī)政策的約束條件，作為失業(yè)保險業(yè)務模型檢測的標準，再將法規(guī)的線性時序邏輯語言描述轉換成線性時序邏輯程序，這部分程序作為模型檢測輸入的約束條件。以上兩部分程序作為輸入條件來檢測失業(yè)保險業(yè)務模型的正確性。
　　 本文利用線性時序邏輯來描述失業(yè)保險業(yè)務處理流程模型的時序性質