時(shí)間自動(dòng)機(jī)及其應(yīng)用研究.pdf

1、實(shí)時(shí)系統(tǒng)在軍事和民用領(lǐng)域都有著廣泛的應(yīng)用，如何保證這類(lèi)系統(tǒng)的安全性和可靠性是研究人員廣泛關(guān)注的問(wèn)題。模型檢測(cè)方法是分析和驗(yàn)證實(shí)時(shí)系統(tǒng)的一種形式化驗(yàn)證方法，而時(shí)間自動(dòng)機(jī)是模型檢測(cè)方法的一個(gè)有效工具。時(shí)間自動(dòng)機(jī)是對(duì)自動(dòng)機(jī)理論的擴(kuò)展，提供了形式化的方法來(lái)建立和分析實(shí)時(shí)系統(tǒng)的行為，在模型檢測(cè)方面有著重要的應(yīng)用。時(shí)間自動(dòng)機(jī)已經(jīng)成為計(jì)算機(jī)科學(xué)理論研究的一個(gè)熱點(diǎn)。 帶自動(dòng)機(jī)是經(jīng)典時(shí)間自動(dòng)機(jī)的一種有窮狀態(tài)構(gòu)造，它的狀態(tài)是由時(shí)鐘帶和位置構(gòu)成的偶對(duì)

2、，因此如何有效的表示和操作時(shí)鐘帶是實(shí)現(xiàn)帶自動(dòng)機(jī)的一個(gè)關(guān)鍵問(wèn)題。目前已經(jīng)提出了幾種有效的表示方法并應(yīng)用于實(shí)踐，如DBM、CDD等，DBM是應(yīng)用比較廣泛的一種數(shù)據(jù)結(jié)構(gòu)。本文研究時(shí)間自動(dòng)機(jī)理論及時(shí)鐘帶的表示和范式化，主要工作如下： 首先，系統(tǒng)的分析時(shí)間自動(dòng)機(jī)理論及其相關(guān)性質(zhì)，介紹區(qū)域自動(dòng)機(jī)和帶自動(dòng)機(jī)。 其次，通過(guò)對(duì)時(shí)鐘帶DBM表示方式的分析，本文分離出一類(lèi)時(shí)鐘帶，針對(duì)這類(lèi)時(shí)鐘帶的特點(diǎn)，提出一種DBM的范式化算法。這種范式化算法