Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Infinite-step opacity of nondeterministic finite transition systems: A bisimulation relation approach
KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
2017 (English)In: 2017 IEEE 56TH ANNUAL CONFERENCE ON DECISION AND CONTROL (CDC), IEEE , 2017Conference paper, Published paper (Refereed)
Abstract [en]

It is known that the problem of verifying the infinite-step opacity of nondeterministic finite transition systems (NFTSs)is PSPACE-hard. In this paper, we investigate whether it is possible to use classical bisimulation relation to come up with abstract NFTSs and verify the infinite-step opacity of original NFTSs over their abstractions. First, we show that generally bisimulation relation does not preserve infinitestep opacity. Second, by adding some additional conditions to bisimulation relation, we prove that a stronger version of bisimulation relation, called here opacity-preserving bisimulation relation, preserves infinite-step opacity. Therefore, if one can find an abstract NFTS for a large NFTS under an opacity-preserving bisimulation relation, then the infinite-step opacity of the original NFTS can be verified by investigating that over the abstract NFTS. Finally, we show that under some mild assumptions, the quotient relation between an NFTS and its quotient system becomes opacity-preserving bisimulation relation which provides a scheme for constructing opacity-preserving abstractions of large- scale NFTSs. We show the effectiveness of the results using several examples throughout the paper.

Place, publisher, year, edition, pages
IEEE , 2017.
Series
IEEE Conference on Decision and Control, ISSN 0743-1546
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:kth:diva-223879ISI: 000424696905064ISBN: 978-1-5090-2873-3 OAI: oai:DiVA.org:kth-223879DiVA, id: diva2:1187508
Conference
IEEE 56th Annual Conference on Decision and Control (CDC), DEC 12-15, 2017, Melbourne, AUSTRALIA
Note

QC 20180305

Available from: 2018-03-05 Created: 2018-03-05 Last updated: 2018-03-05Bibliographically approved

Open Access in DiVA

No full text in DiVA

Search in DiVA

By author/editor
Zhang, Kuize
By organisation
ACCESS Linnaeus Centre
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 15 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf