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

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

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

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