Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Reachability Problems

RP 2017: Reachability Problems pp 9–25Cite as

Adding Dense-Timed Stack to Integer Reset Timed Automata

  • Conference paper
  • First Online:

  • 312 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10506))

Abstract

Integer reset timed automata (IRTA) are known to be a determinizable subclass of timed automata, but it is not known whether they are input-determined, i.e., the clock values are completely determined by an input timed word. We first define a syntactic subclass of IRTA called strict IRTA and show that strict IRTA is equivalent to IRTA. We show that the class of strict IRTA is indeed input-determined. Visibly pushdown automata is another input-determined class of automata with a stack that is also closed under boolean operations and admits a logical characterization. We propose dtIRVPA as a class of timed automata with a dense-timed stack. Similar to strict IRTA, we define strict dtIRVPA and show that strict dtIRVPA is input-determined where both – stack operations and the values of the integer reset clocks – are determined by the input word, and this helps us to get the monadic second-order (MSO) logical characterization of dtIRVPA. We prove the closure properties of dtIRVPA under union, intersection, complementation, and determinization. Further, we show that reachability of dtIRVPA is PSPACE-complete, i.e. the complexity is no more than that of timed automata.

S. Guha—Supported by FP7/2007-2013, ERC grant no 278410.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: LICS, pp. 35–44 (2012)

    Google Scholar 

  2. Aceto, L., Laroussinie, F.: Is your model checker on time? on the complexity of model checking for timed modal logics. J. Log. Algebr. Program. 52–53, 7–51 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  3. Akshay, S., Gastin, P., Krishna, S.N.: Analyzing timed systems using tree automata. In: CONCUR, pp. 27:1–27:14 (2016)

    Google Scholar 

  4. Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC, pp. 202–211 (2004)

    Google Scholar 

  6. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 43–54. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02930-1_4

    Chapter  Google Scholar 

  7. Bhave, D., Dave, V., Krishna, S.N., Phawade, R., Trivedi, A.: A logical characterization for dense-time visibly pushdown automata. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 89–101. Springer, Cham (2016). doi:10.1007/978-3-319-30000-9_7

    Chapter  Google Scholar 

  8. Bhave, D., Dave, V., Krishna, S.N., Phawade, R., Trivedi, A.: A perfect class of context-sensitive timed languages. In: Brlek, S., Reutenauer, C. (eds.) DLT 2016. LNCS, vol. 9840, pp. 38–50. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53132-7_4

    Chapter  Google Scholar 

  9. Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. Hybrid Syst. II, 64–85 (1995)

    MathSciNet  Google Scholar 

  10. Clemente, L., Lasota, S.: Timed pushdown automata revisited. In: LICS, pp. 738–749 (2015)

    Google Scholar 

  11. Dang, Z.: Binary reachability analysis of pushdown timed automata with dense clocks. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 506–517. Springer, Heidelberg (2001). doi:10.1007/3-540-44585-4_48

    Chapter  Google Scholar 

  12. Droste, M., Perevoshchikov, V.: A logical characterization of timed pushdown languages. In: Beklemishev, L.D., Musatov, D.V. (eds.) CSR 2015. LNCS, vol. 9139, pp. 189–203. Springer, Cham (2015). doi:10.1007/978-3-319-20297-6_13

    Google Scholar 

  13. D’Souza, D., Tabareau, N.: On timed automata with input-determined guards. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 68–83. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_7

    Chapter  Google Scholar 

  14. Henzinger, T.A., Majumdar, R., Prabhu, V.S.: Quantifying similarities between timed systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 226–241. Springer, Heidelberg (2005). doi:10.1007/11603009_18

    Chapter  Google Scholar 

  15. Lautemann, C., Schwentick, T., Thérien, D.: Logics for context-free languages. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 205–216. Springer, Heidelberg (1995). doi:10.1007/BFb0022257

    Chapter  Google Scholar 

  16. Li, G., Cai, X., Ogawa, M., Yuen, S.: Nested timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 168–182. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40229-6_12

    Chapter  Google Scholar 

  17. Li, G., Ogawa, M., Yuen, S.: Nested timed automata with frozen clocks. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 189–205. Springer, Cham (2015). doi:10.1007/978-3-319-22975-1_13

    Chapter  Google Scholar 

  18. Manasa, L., Krishna, S.N.: Integer reset timed automata: clock reduction and determinizability. CoRR, abs/1001.1215 (2010)

    Google Scholar 

  19. Mohalik, A., Rajeev, C., Dixit, M.G., Ramesh, S., Suman, P.V., Pandya, P.K., Jiang, S.: Model checking based analysis of end-to-end latency in embedded, real-time systems with clock drifts. In: DAC (2008)

    Google Scholar 

  20. Suman, P.V., Pandya, P.K., Krishna, S.N., Manasa, L.: Timed automata with integer resets: language inclusion and expressiveness. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 78–92. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85778-5_7

    Chapter  Google Scholar 

  21. Trivedi, A., Wojtczak, D.: Recursive timed automata. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 306–324. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15643-4_23

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Indian Institute of Technology Bombay, Mumbai, India

    Devendra Bhave

  2. The Hebrew University of Jerusalem, Jerusalem, Israel

    Shibashis Guha

Authors
  1. Devendra Bhave
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shibashis Guha
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Devendra Bhave .

Editor information

Editors and Affiliations

  1. Royal Holloway University of London, London, United Kingdom

    Matthew Hague

  2. University of Liverpool, Liverpool, United Kingdom

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bhave, D., Guha, S. (2017). Adding Dense-Timed Stack to Integer Reset Timed Automata. In: Hague, M., Potapov, I. (eds) Reachability Problems. RP 2017. Lecture Notes in Computer Science(), vol 10506. Springer, Cham. https://doi.org/10.1007/978-3-319-67089-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67089-8_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67088-1

  • Online ISBN: 978-3-319-67089-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation