時(shí)間自動(dòng)機(jī)可達(dá)性檢測方法研究.pdf

1、時(shí)間自動(dòng)機(jī)是具有時(shí)間約束的有限狀態(tài)轉(zhuǎn)換系統(tǒng)，在實(shí)時(shí)系統(tǒng)進(jìn)行形式化證明的過程中，先用它建模，然后再檢驗(yàn)?zāi)承┎话踩珷顟B(tài)是否可達(dá)。所以研究時(shí)間自動(dòng)機(jī)及其驗(yàn)證技術(shù)，主要研究它的狀態(tài)可達(dá)性問題。然而由于在它的語義描述中時(shí)間自動(dòng)機(jī)的狀態(tài)是無窮的，因而計(jì)算它的狀態(tài)可達(dá)性關(guān)系顯得尤為復(fù)雜。 時(shí)間自動(dòng)機(jī)中各時(shí)鐘的值可以取連續(xù)的正實(shí)數(shù)值，為狀態(tài)可達(dá)性關(guān)系的計(jì)算帶來了許多不便，所以本文在R.Alur和D.L.Dill提出的時(shí)間轉(zhuǎn)換系統(tǒng)等價(jià)轉(zhuǎn)化的基礎(chǔ)上

2、給出了在時(shí)間自動(dòng)機(jī)中可以通過等價(jià)轉(zhuǎn)化將所有的時(shí)鐘約束轉(zhuǎn)化為僅含有整數(shù)值約束常量的約束，并且分析了這種轉(zhuǎn)化對(duì)時(shí)間自動(dòng)機(jī)兩類轉(zhuǎn)換的影響及其等價(jià)性證明。 求解時(shí)間自動(dòng)機(jī)狀態(tài)可達(dá)性關(guān)系的關(guān)鍵問題在于對(duì)各個(gè)時(shí)鐘的時(shí)間約束關(guān)系的處理。R.Alur和D.L.Dill提出的域自動(dòng)機(jī)構(gòu)造方法通過對(duì)狀態(tài)空間進(jìn)行等價(jià)劃分構(gòu)造有限自動(dòng)機(jī)，然后通過對(duì)有限自動(dòng)機(jī)的分析求解狀態(tài)可達(dá)性關(guān)系。JohanBengtsson提出了含有形如x-y～n(其中，～∈{<，

3、>，=，≤，≥})的時(shí)間自動(dòng)機(jī)狀態(tài)可達(dá)性關(guān)系的計(jì)算方法。。Felice Balarin提出的近似計(jì)算方法實(shí)際上計(jì)算出的只是可達(dá)狀態(tài)集的超集，這種超集有時(shí)候會(huì)證明一個(gè)正確的系統(tǒng)是不正確的，但是它不會(huì)使得一個(gè)不正確的系統(tǒng)被證明是正確的。Catalin Dima將復(fù)位點(diǎn)語義應(yīng)用于時(shí)間自動(dòng)機(jī)，通過對(duì)原子關(guān)系的合成、并和自反傳遞閉包進(jìn)行運(yùn)算求解可達(dá)狀態(tài)集。 本文研究分析了上述幾種求解方法。然后針對(duì)符號(hào)化的時(shí)間自動(dòng)機(jī)語義在對(duì)所有大于時(shí)鐘約束