國立臺灣大學電機工程學系暨研究所顏嗣鈞2006-07-252018-07-062006-07-252018-07-062003-07-31http://ntur.lib.ntu.edu.tw//handle/246246/7925本研究的主要目的在探討即時系統驗證之相關問題。我們探討具有未知變數 (unknown timing parameters)之時間自動機(timed automata)的抵達解答空間 (reachability solution space)問題。一般而言，該問題為不可解的。我們定義三類 有限制之具參數時間自動機，並詳細分析其抵達解答空間問題。該三類分別為「上 限」(upper-bound)、「下限」(lower-bound)、「雙分」(bipartite) 時間自動機。我們 詳細分析以上問題的複雜度，並將結果應用至「具狀態之時間向量加法系統」 (timing parameter vector addition systems with states) 。We investigate the problem of characterizing the solution spaces for timed automata augmented by unknown timing parameters (called timing parameter automata (TPA)). The main contribution of this work is that we identify three non-trivial subclasses of TPAs, namely, upper-bound, lower-bound and bipartite TPAs, and analyze how hard it is to characterize the solution space. As it turns out, we are able to give complexity bounds for the sizes of the minimal (resp., maximal) elements which completely characterize the upward-closed (resp., downward-closed) solution spaces of upper-bound (resp., lower-bound) TPAs. For bipartite TPAs, it is shown that their solution spaces are not semilinear in general. We also extend our analysis to TPAs equipped with counters without zero-test capabilities.application/pdf125121 bytesapplication/pdfzh-TW國立臺灣大學電機工程學系暨研究所時間自動機時態邏輯即時系統驗證Timed automatatemporal logicreal-time verificationreporthttp://ntur.lib.ntu.edu.tw/bitstream/246246/7925/1/912213E002073.pdf