1 Search Results for "Zhang, Kuize"


Document
State-Based Opacity of Real-Time Automata

Authors: Kuize Zhang

Published in: OASIcs, Volume 90, 27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems (AUTOMATA 2021)


Abstract
State-based opacity is a special type of opacity as a confidentiality property, which describes whether an external intruder cannot make for sure whether secret states of a system have been visited by observing generated outputs, given that the intruder knows complete knowledge of the system’s structure but can only see generated outputs. When the time of visiting secret states is specified as the initial time, the current time, any past time, and at most K steps prior to the current time, the notions of state-based opacity can be formulated as initial-state opacity, current-state opacity, infinite-step opacity, and K-step opacity, respectively. In this paper, we formulate the four versions of opacity for real-time automata which are a widely-used model of real-time systems, and give 2-EXPTIME verification algorithms for the four notions by defining appropriate notions of observer and reverse observer for real-time automata that are computable in 2-EXPTIME.

Cite as

Kuize Zhang. State-Based Opacity of Real-Time Automata. In 27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems (AUTOMATA 2021). Open Access Series in Informatics (OASIcs), Volume 90, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{zhang:OASIcs.AUTOMATA.2021.12,
  author =	{Zhang, Kuize},
  title =	{{State-Based Opacity of Real-Time Automata}},
  booktitle =	{27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems (AUTOMATA 2021)},
  pages =	{12:1--12:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-189-4},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{90},
  editor =	{Castillo-Ramirez, Alonso and Guillon, Pierre and Perrot, K\'{e}vin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.AUTOMATA.2021.12},
  URN =		{urn:nbn:de:0030-drops-140217},
  doi =		{10.4230/OASIcs.AUTOMATA.2021.12},
  annote =	{Keywords: real-time automaton, state-based opacity, observer, verification}
}
  • Refine by Author
  • 1 Zhang, Kuize

  • Refine by Classification
  • 1 Security and privacy → Formal security models
  • 1 Theory of computation → Timed and hybrid models

  • Refine by Keyword
  • 1 observer
  • 1 real-time automaton
  • 1 state-based opacity
  • 1 verification

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail