無限狀態系統之自動驗證(1/3)
Date Issued
2003-07-31
Date
2003-07-31
Author(s)
DOI
912213E002073
Abstract
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.
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.
Subjects
Timed automata
temporal logic
real-time verification
Publisher
臺北市:國立臺灣大學電機工程學系暨研究所
Type
report
File(s)![Thumbnail Image]()
Loading...
Name
912213E002073.pdf
Size
122.19 KB
Format
Adobe PDF
Checksum
(MD5):d4bfcb1002e552d1f19df6360d0a5b1f