無限狀態系統之自動驗證(2/3)
Date Issued
2004-07-31
Date
2004-07-31
Author(s)
DOI
922213E002018
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 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.
Subjects
timed automata
timing
parameter
parameter
Publisher
臺北市：國立臺灣大學電機工程學系暨研究所
Type
report
File(s)![Thumbnail Image]()
Loading...
Name
922213E002018.pdf
Size
36.69 KB
Format
Adobe PDF
Checksum
(MD5):333d68028df3c88668a0b35c04a50f2e