Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Infinite-step opacity of nondeterministic finite transition systems: A bisimulation relation approach
KTH, Skolan för elektro- och systemteknik (EES), Centra, ACCESS Linnaeus Centre.
2017 (engelsk)Inngår i: 2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017, IEEE , 2017, s. 5615-5619Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
IEEE , 2017. s. 5615-5619
Serie
IEEE Conference on Decision and Control, ISSN 0743-1546
HSV kategori
Identifikatorer
URN: urn:nbn:se:kth:diva-223879DOI: 10.1109/CDC.2017.8264506ISI: 000424696905064Scopus ID: 2-s2.0-85046271363ISBN: 978-1-5090-2873-3 (tryckt)OAI: oai:DiVA.org:kth-223879DiVA, id: diva2:1187508
Konferanse
IEEE 56th Annual Conference on Decision and Control (CDC), DEC 12-15, 2017, Melbourne, AUSTRALIA
Merknad

QC 20180305

Tilgjengelig fra: 2018-03-05 Laget: 2018-03-05 Sist oppdatert: 2024-03-18bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Person

Zhang, Kuize

Søk i DiVA

Av forfatter/redaktør
Zhang, Kuize
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 22 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf