Reachability solution characterization of parametric real-time systems
Resource
Theoretical Computer Science 328 (1-2): 187-201
Journal
Theoretical Computer Science
Journal Volume
328
Journal Issue
1-2
Pages
187-201
Date Issued
2004
Date
2004
Author(s)
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 paper 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. © 2004 Elsevier B.V. All rights reserved.
Type
journal article
File(s)![Thumbnail Image]()
Loading...
Name
05.pdf
Size
273.15 KB
Format
Adobe PDF
Checksum
(MD5):42e5be68679860250c18a9298f1f0c12