Advertisement

Timing Parameter Characterization of Real-Time Systems

  • Farn Wang
  • Hsu-Chun Yen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2759)

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.

Keywords

Solution Space Minimal Element Region Graph Partial Interpretation Inequality Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    R. Alur, C. Courcoubetis, D. L. Dill. Model-Checking in Dense Real-Time, Information and Computation 104(1), 2–34, 1990.CrossRefMathSciNetGoogle Scholar
  2. [2]
    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
  3. [3]
    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
  4. [4]
    R. Alur, T.A. Henzinger, M.Y. Vardi. Parametric Real-Time Reasoning, in Proc. 25th ACM STOC, pp. 592–601, 1993.Google Scholar
  5. [5]
    B. Berard. Untiming Timed Languages, Inform. Proc. Lett., 55:129–135,1995.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    G. Delzanno, J.-F. Raskin. Symbolic Representation of Upward-closed Sets, in Proc. TACAS 2000, LNCS 1785, pp. 426–440, 2000.Google Scholar
  7. [7]
    E.A. Emerson, R. Trefler. Parametric Quantitative Temporal Reasoning, in Proc. IEEE LICS, pp. 336–343, July 1999.Google Scholar
  8. [8]
    T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic Model Checking for Real-Time Systems, Information and Computation, 111, 193–244, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  9. [9]
    J. Hopcroft, J. Pansiot. On the Reachability Problem for 5-Dimensional Vector Addition Systems, Theoretical Computer Science, 8, 135–159, 1979.zbMATHCrossRefMathSciNetGoogle Scholar
  10. [10]
    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
  11. [11]
    C. Rackoff. The Covering and Boundedness Problems for Vector Addition Systems, Theoretical Computer Science, 6, 223–231, 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  12. [12]
    L. Rosier, H. Yen. A Multiparameter Analysis of the Boundedness Problem for Vector Addition Systems, J. Comput. System Sci., 32, 105–135, 1986.zbMATHCrossRefMathSciNetGoogle Scholar
  13. [13]
    R. Valk, M. Jantzen. The Residue of Vector Sets with Applications to Decidability in Petri Nets, Acta Informatica, 21, 643–674, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  14. [14]
    F. Wang. Parametric Timing Analysis for Real-Time Systems, Information and Computation, 130(2), 131–150, 1996. Also in Proc. 10th IEEE LICS, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  15. [15]
    F. Wang. Parametric Analysis of Computer Systems, Formal Methods in System Design, 17, 39–60, 2000.CrossRefGoogle Scholar
  16. [16]
    F. Wang, P.-A. Hsiung. Parametric Analysis of Computer Systems, Australia, Dec. 1997, in Proc. AMAST’97, LNCS 1349, pp. 539–553.Google Scholar
  17. [17]
    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

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Farn Wang
    • 1
  • Hsu-Chun Yen
    • 1
  1. 1.Dept. of Electrical EngineeringNational Taiwan UniversityTaipeiTaiwan, Republic of China

Personalised recommendations