DROPS

Document

DOI: 10.4230/OASIcs.AUTOMATA.2021.12

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.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}
}

Search Results

Documents authored by Zhang, Kuize

State-Based Opacity of Real-Time Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message