Skip to main content
SpringerLink
Log in
Book cover

Brazilian Symposium on Formal Methods

SBMF 2021: Formal Methods: Foundations and Applications pp 122–139Cite as

Minimization of the Number of Clocks for Timed Scenarios

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 13130))

Abstract

We present a new optimization algorithm for timed scenarios that achieves the minimal number of clocks when timed scenarios are viewed as timed automata.

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   44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   59.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

Notes

  1. 1.

    The notion of “behaviour” is equivalent to that of Alur’s “timed word” [3].

  2. 2.

    To keep the presentation compact, equality is expressed in terms of \(\le \) and \(\ge \) [12].

References

  1. Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1089–1101. Springer, Heidelberg (2005). https://doi.org/10.1007/11523468_88

    Chapter  MATH  Google Scholar 

  2. Akshay, S., Mukund, M., Kumar, K.N.: Checking coverage for infinite collections of timed scenarios. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 181–196. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_13

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  4. Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_1

    Chapter  MATH  Google Scholar 

  5. Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 75–91. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13338-6_7

    Chapter  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). https://doi.org/10.1007/978-3-642-02930-1_4

    Chapter  MATH  Google Scholar 

  7. Bollig, B., Katoen, J.-P., Kern, C., Leucker, M.: Replaying play in and play out: synthesis of design models from scenarios by learning. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 435–450. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_33

    Chapter  MATH  Google Scholar 

  8. Chandrasekaran, P., Mukund, M.: Matching scenarios with timing constraints. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 98–112. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_8

    Chapter  Google Scholar 

  9. Harel, D., Kugler, H., Pnueli, A.: Synthesis revisited: generating statechart models from scenario-based requirements. In: Kreowski, H.-J., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol. 3393, pp. 309–324. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31847-7_18

    Chapter  Google Scholar 

  10. Heitmeyer, C.L., et al.: Building high assurance human-centric decision systems. Autom. Softw. Eng. 22(2), 159–197 (2014). https://doi.org/10.1007/s10515-014-0157-z

    Article  Google Scholar 

  11. Saeedloei, N., Kluźniak, F.: From scenarios to timed automata. In: Cavalheiro, S., Fiadeiro, J. (eds.) SBMF 2017. LNCS, vol. 10623, pp. 33–51. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70848-5_4

    Chapter  Google Scholar 

  12. Saeedloei, N., Kluźniak, F.: Timed scenarios: consistency, equivalence and optimization. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 215–233. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03044-5_14

    Chapter  MATH  Google Scholar 

  13. Saeedloei, N., Kluźniak, F.: Optimization of timed scenarios. In: Carvalho, G., Stolz, V. (eds.) SBMF 2020. LNCS, vol. 12475, pp. 119–136. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-63882-5_8

    Chapter  Google Scholar 

  14. Saeedloei, N., Kluźniak, F.: Synthesizing clock-efficient timed automata. In: Dongol, B., Troubitsyna, E. (eds.) IFM 2020. LNCS, vol. 12546, pp. 276–294. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-63461-2_15

    Chapter  Google Scholar 

  15. Somé, S., Dssouli, R., Vaucher, J.: From scenarios to timed automata: building specifications from users requirements. In: Proceedings of the Second Asia Pacific Software Engineering Conference. APSEC 1995, pp. 48–57. IEEE Computer Society (1995)

    Google Scholar 

  16. Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans. Softw. Eng. 29(2), 99–115 (2003)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Towson University, Towson, USA

    Neda Saeedloei

  2. LogicBlox, Atlanta, USA

    Feliks Kluźniak

Authors
  1. Neda Saeedloei
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Feliks Kluźniak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Neda Saeedloei .

Editor information

Editors and Affiliations

  1. Departamento de Ciência da Computação, Universidade Federal de Minas Gerais, Belo Horizonte, Minas Gerais, Brazil

    Sérgio Campos

  2. College of Information and Computer Sciences, University of Massachusetts, Amherst, MA, USA

    Marius Minea

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Saeedloei, N., Kluźniak, F. (2021). Minimization of the Number of Clocks for Timed Scenarios. In: Campos, S., Minea, M. (eds) Formal Methods: Foundations and Applications. SBMF 2021. Lecture Notes in Computer Science(), vol 13130. Springer, Cham. https://doi.org/10.1007/978-3-030-92137-8_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-92137-8_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-92136-1

  • Online ISBN: 978-3-030-92137-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation