程序綜合是一種通過系統(tǒng)行為規(guī)范來自動設(shè)計生成交互式系統(tǒng)模型的技術(shù)。目前主流的行為規(guī)范語言叫做線性時態(tài)邏輯LTL。然而LTL程序綜合問題是一個復(fù)雜的難題,在實踐中難以應(yīng)用。因此基于實踐角度考慮,研究者們將更多的關(guān)注點放在了LTL子集上的程序綜合問題,希望可以有針對性的技術(shù)來獲得更好的求解方案。本文主要關(guān)注一種新的邏輯語言,叫做有限線性時態(tài)邏輯LTL_f。LTL_f對LTL的語法進行了重定義,是一種解析在有限序列上的語言。在這種解析方式下,程序執(zhí)行序列可以是任意有限長度,也因此令LTL_f更加適用于計算機和人工智能領(lǐng)域中的有限域問題。這也就引出了本文的研究課題,LTL_f程序綜合。本文主要工作和貢獻點有以下四個方面:·提出了符號化LTL_f程序綜合框架。傳統(tǒng)的LTL_f程序綜合方法無法避免空間爆炸問題,于是本文首先提出了符號化DFA的概念,并以此為基礎(chǔ)提出了基于BDD和不動點計算的符號化LTL_f程序綜合框架。實驗表明本文提出的新方法在所有已知相關(guān)方法... 

【文章來源】：華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：148 頁

【學(xué)位級別】：博士

【文章目錄】：
摘要
abstract
主要命名中英對照表
主要符號索引
第一章 緒論
    1.1 有限線性時態(tài)邏輯
        1.1.1 線性時態(tài)邏輯的提出和發(fā)展
        1.1.2 有限線性時態(tài)邏輯的提出和發(fā)展
        1.1.3 有限線性時態(tài)邏輯的應(yīng)用場景
    1.2 程序綜合在計算機領(lǐng)域的重要性
        1.2.1 程序綜合問題的提出
        1.2.2 程序綜合問題的研究現(xiàn)狀
        1.2.3 程序綜合競賽
    1.3 本文的選題與主要工作
第二章 基礎(chǔ)知識
f">    2.1 有限線性時態(tài)邏輯LTLf

    2.2 LTL_f到FOL
f程序綜合">    2.3 LTL_f程序綜合
    2.4 二元決策圖
    2.5 布爾程序綜合
f程序綜合">第三章 符號化LTL_f程序綜合
    3.1 背景介紹
f公式到DFA的轉(zhuǎn)化">    3.2 LTL_f公式到DFA的轉(zhuǎn)化
        3.2.1 DFA構(gòu)造
    3.3 DFA構(gòu)造比較實驗
f程序綜合框架">    3.4 符號化LTL_f程序綜合框架
        3.4.1 符號化DFA博弈求解
f綜合">        3.4.2 通過LTL綜合來實現(xiàn)LTL_f綜合
    3.5 工具實現(xiàn)
        3.5.1 預(yù)處理MONA返回的DFA
        3.5.2 程序綜合方法的實現(xiàn)
    3.6 比較實驗
        3.6.1 符號化vs.具體化
        3.6.2 Syft與 LTL綜合工具的比較
        3.6.3 實驗討論
    3.7 本章小結(jié)
f到自動機的多編碼研究">第四章 LTL_f到自動機的多編碼研究
    4.1 背景介紹
    4.2 MSO編碼
    4.3 緊湊MSO編碼
f到PLTL_f">        4.3.1 LTL_f到PLTL_f

        4.3.2 PLTL_f到DFA
        4.3.3 用二階邏輯來反轉(zhuǎn)DFA
    4.4 實驗評估
        4.4.1 二階邏輯編碼優(yōu)化
        4.4.2 實驗結(jié)果
    4.5 本章小結(jié)
第五章 自動機最小化對程序綜合的影響研究
    5.1 背景介紹
    5.2 離線DFA構(gòu)造
f到DFA轉(zhuǎn)化的復(fù)雜度">        5.2.1 LTL_f到DFA轉(zhuǎn)化的復(fù)雜度
f到SS-NFA的構(gòu)造">        5.2.2 LTL_f到SS-NFA的構(gòu)造
        5.2.3 符號化自動機確定化方法
        5.2.4 實驗比較
f程序綜合">    5.3 動態(tài)LTL_f程序綜合
        5.3.1 SS-NFA上的程序綜合
        5.3.2 實驗評估
    5.4 本章小結(jié)
f程序綜合">第六章 公平假設(shè)下的LTL_f程序綜合
    6.1 背景介紹
f綜合">    6.2 公平LTL_f綜合
        6.2.1 復(fù)雜DFA博弈歸約
        6.2.2 穩(wěn)定-可達博弈求解
        6.2.3 獲勝策略抽取
    6.3 歸約到LTL程序綜合
    6.4 比較實驗
        6.4.1 實驗策略
        6.4.2 實驗結(jié)果
    6.5 本章小結(jié)
第七章 總結(jié)與展望
    7.1 全文小結(jié)
    7.2 未來工作展望
參考文獻
致謝
攻讀博士學(xué)位期間發(fā)表論文和科研情況



本文編號：3067033

boshi