Skip to main content
SpringerLink
Log in

Decidability of the Initial-State Opacity of Real-Time Automata

  • Chapter
  • First Online:
Symposium on Real-Time and Hybrid Systems

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

Abstract

In this paper, we investigate the initial-state opacity of real-time automata. A system is called initial-state opaque if an intruder with partial observability is unable to determine whether or not the execution starts from a secret state. In order to prove that the initial-state opacity problem is decidable, we first calculate the lapse of time between each pair of observable events. Two real-time automata are constructed which accept the projection of languages from secret initial states and non-secret ones, respectively. Then, the two real-time automata are further transformed into trace-equivalent finite-state automata. Subsequently, we adapt complement and product on the finite-state automata, and check accepting language of the finally-obtained automaton. The system is initial-state opaque if it accepts nothing or only empty trace, and not initial-state opaque otherwise.

This work is funded partly by NSFC under grant No. 61625206 and 61732001, by “973 Program” under grant No. 2014CB340701, and by the CAS/SAFEA International Partnership Program for Creative Research Teams.

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

Access this chapter

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

Institutional subscriptions

References

  1. Saboori, A., Hadjicostis, C.N.: Verification of initial-state opacity in security applications of discrete event systems. Inf. Sci. 246, 115–132 (2013)

    Article  MathSciNet  Google Scholar 

  2. Bryans, J.W., Kounty, M., Ryan, P.Y.: Modelling opacity using petri nets. Electron. Notes Theor. Comput. Sci. 121, 101–115 (2005). Proceedings of the 2nd International Workshop on Security Issues with Petri Nets and other Computational Models (WISP 2004)

    Article  Google Scholar 

  3. Tong, Y., Li, Z., Seatzu, C., Giua, A.: Verification of state-based opacity using Petri nets. IEEE Trans. Autom. Control. 62(6), 2823–2837 (2017)

    Article  MathSciNet  Google Scholar 

  4. Bryans, J.W., Kounty, M., Mazaré, L., Ryan, P.Y.A.: Opacity generalised to transition systems. Int. J. Inf. Secur. 7(6), 421–435 (2008)

    Article  Google Scholar 

  5. Saboori, A., Hadjicostis, C.N.: Verification of k-step opacity and analysis of its complexity. In: Proceedings of the 48th IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference, pp. 205–210 (2009)

    Google Scholar 

  6. Saboori, A., Hadjicostis, C.N.: Opacity-enforcing supervisory strategies via state estimator constructions. IEEE Trans. Autom. Control. 57(5), 1155–1165 (2012)

    Article  MathSciNet  Google Scholar 

  7. Saboori, A., Hadjicostis, C.N.: Verification of infinite-step opacity and complexity considerations. IEEE Trans. Autom. Control. 57(5), 1265–1269 (2012)

    Article  MathSciNet  Google Scholar 

  8. Keroglou, C., Hadjicostis, C.N.: Initial state opacity in stochastic des. In: 2013 IEEE 18th Conference on Emerging Technologies & Factory Automation (ETFA), pp. 1–8 (2013)

    Google Scholar 

  9. Bérard, B., Chatterjee, K., Sznajder, N.: Probabilistic opacity for Markov decision processes. Inf. Process. Lett. 115(1), 52–59 (2015)

    Article  MathSciNet  Google Scholar 

  10. Bérard, B., Mullins, J., Sassolas, M.: Quantifying opacity. In: 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pp. 263–272 (2010)

    Google Scholar 

  11. Ibrahim, M., Chen, J., Kumar, R.: Secrecy in stochastic discrete event systems. In: Proceedings of the 11th IEEE International Conference on Networking, Sensing and Control, pp. 48–53 (2014)

    Google Scholar 

  12. Cassez, F.: The dark side of timed opacity. In: Park, J.H., Chen, H.-H., Atiquzzaman, M., Lee, C., Kim, T., Yeo, S.-S. (eds.) ISA 2009. LNCS, vol. 5576, pp. 21–30. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02617-1_3

    Chapter  Google Scholar 

  13. Dima, C.: Real-time automata. J. Autom. Lang. Comb. 6(1), 3–24 (2001)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. State Key Lab. of Comp. Sci., Institute of Software, Chinese Academy of Sciences, Beijing, China

    Lingtai Wang & Naijun Zhan

  2. University of Chinese Academy of Sciences, Beijing, China

    Lingtai Wang & Naijun Zhan

Authors
  1. Lingtai Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Naijun Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Naijun Zhan .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle, UK

    Cliff Jones

  2. National University of Defense Technology, Changsha, China

    Ji Wang

  3. Institute of Software, CAS, Beijing, China

    Naijun Zhan

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Wang, L., Zhan, N. (2018). Decidability of the Initial-State Opacity of Real-Time Automata. In: Jones, C., Wang, J., Zhan, N. (eds) Symposium on Real-Time and Hybrid Systems. Lecture Notes in Computer Science(), vol 11180. Springer, Cham. https://doi.org/10.1007/978-3-030-01461-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-01461-2_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-01460-5

  • Online ISBN: 978-3-030-01461-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation