國立臺灣大學電機工程學系暨研究所顏嗣鈞2006-07-252018-07-062006-07-252018-07-062004-07-31http://ntur.lib.ntu.edu.tw//handle/246246/7976本年度之研究計畫中、我們研究參數 時間自動機 (timing parameter automata, TPA)之解答空間問題 (the solution space problem) 。 一般而 言，此問題為不可解。我們探討三類 可解之情形: upper-bound TPA 、 lower-bound TPA 、 bipartite TPA 。 我們並發展新的驗證技術來解決以上 三類參數時間自動機之解答空間問 題，並分析其複雜度。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 spaces. 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/pdf37567 bytesapplication/pdfzh-TW國立臺灣大學電機工程學系暨研究所時間自動機時間參數timed automatatiming parameterreporthttp://ntur.lib.ntu.edu.tw/bitstream/246246/7976/1/922213E002018.pdf