License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.AUTOMATA.2021.12
URN: urn:nbn:de:0030-drops-140217
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14021/
Go to the corresponding OASIcs Volume Portal

Zhang, Kuize

State-Based Opacity of Real-Time Automata

pdf-format:
OASIcs-AUTOMATA-2021-12.pdf (0.6 MB)

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.

BibTeX - Entry

@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/opus/volltexte/2021/14021},
  URN =		{urn:nbn:de:0030-drops-140217},
  doi =		{10.4230/OASIcs.AUTOMATA.2021.12},
  annote =	{Keywords: real-time automaton, state-based opacity, observer, verification}
}

Keywords: real-time automaton, state-based opacity, observer, verification
Collection: 27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems (AUTOMATA 2021)
Issue Date: 2021
Date of publication: 28.06.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI