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 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, D. L. Dill. Model-Checking in Dense Real-Time, Information and Computation 104(1), 2–34, 1990.
R. Alur, D. L. Dill, D. Automata for Modeling Real-Time Systems, in in Proc. 17th ICALP, LNCS 443, pp. 332–335, 1990.
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.
R. Alur, T.A. Henzinger, M.Y. Vardi. Parametric Real-Time Reasoning, in Proc. 25th ACM STOC, pp. 592–601, 1993.
B. Berard. Untiming Timed Languages, Inform. Proc. Lett., 55:129–135,1995.
G. Delzanno, J.-F. Raskin. Symbolic Representation of Upward-closed Sets, in Proc. TACAS 2000, LNCS 1785, pp. 426–440, 2000.
E.A. Emerson, R. Trefler. Parametric Quantitative Temporal Reasoning, in Proc. IEEE LICS, pp. 336–343, July 1999.
T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic Model Checking for Real-Time Systems, Information and Computation, 111, 193–244, 1994.
J. Hopcroft, J. Pansiot. On the Reachability Problem for 5-Dimensional Vector Addition Systems, Theoretical Computer Science, 8, 135–159, 1979.
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.
C. Rackoff. The Covering and Boundedness Problems for Vector Addition Systems, Theoretical Computer Science, 6, 223–231, 1978.
L. Rosier, H. Yen. A Multiparameter Analysis of the Boundedness Problem for Vector Addition Systems, J. Comput. System Sci., 32, 105–135, 1986.
R. Valk, M. Jantzen. The Residue of Vector Sets with Applications to Decidability in Petri Nets, Acta Informatica, 21, 643–674, 1985.
F. Wang. Parametric Timing Analysis for Real-Time Systems, Information and Computation, 130(2), 131–150, 1996. Also in Proc. 10th IEEE LICS, 1995.
F. Wang. Parametric Analysis of Computer Systems, Formal Methods in System Design, 17, 39–60, 2000.
F. Wang, P.-A. Hsiung. Parametric Analysis of Computer Systems, Australia, Dec. 1997, in Proc. AMAST’97, LNCS 1349, pp. 539–553.
F. Wang, H.-C. Yen. Parametric Optimization of Open Real-Time Systems, Paris, July 2001, in Proc. SAS 2001, LNCS 2126, pp. 299–318.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, F., Yen, HC. (2003). Timing Parameter Characterization of Real-Time Systems. In: Ibarra, O.H., Dang, Z. (eds) Implementation and Application of Automata. CIAA 2003. Lecture Notes in Computer Science, vol 2759. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45089-0_4
Download citation
DOI: https://doi.org/10.1007/3-540-45089-0_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40561-0
Online ISBN: 978-3-540-45089-4
eBook Packages: Springer Book Archive