Timing Parameter Characterization of Real-Time Systems
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 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.
KeywordsSolution Space Minimal Element Region Graph Partial Interpretation Inequality Operator
Unable to display preview. Download preview PDF.
- R. Alur, D. L. Dill, D. Automata for Modeling Real-Time Systems, in in Proc. 17th ICALP, LNCS 443, pp. 332–335, 1990.Google Scholar
- R. Alur, K. Etessami, S. La Torre, D. Peled. Parametric Temporal Logic for Model Measuring, in Proc. 26th ICALP, LNCS 1644, pp. 169–178, 1999.Google Scholar
- R. Alur, T.A. Henzinger, M.Y. Vardi. Parametric Real-Time Reasoning, in Proc. 25th ACM STOC, pp. 592–601, 1993.Google Scholar
- G. Delzanno, J.-F. Raskin. Symbolic Representation of Upward-closed Sets, in Proc. TACAS 2000, LNCS 1785, pp. 426–440, 2000.Google Scholar
- E.A. Emerson, R. Trefler. Parametric Quantitative Temporal Reasoning, in Proc. IEEE LICS, pp. 336–343, July 1999.Google Scholar
- T. Hune, J. Romijn, M. Stoekinga, F. Vaandrager. Linear Parametric Model Checking of Timed Automata, in Proc. TACAS 2001, Italy, April, 2001, LNCS 2031, pp. 189–203.Google Scholar
- F. Wang, P.-A. Hsiung. Parametric Analysis of Computer Systems, Australia, Dec. 1997, in Proc. AMAST’97, LNCS 1349, pp. 539–553.Google Scholar
- F. Wang, H.-C. Yen. Parametric Optimization of Open Real-Time Systems, Paris, July 2001, in Proc. SAS 2001, LNCS 2126, pp. 299–318.Google Scholar