Dynamic observers for the synthesis of opaque systems

Franck Cassez*, Jérémy Dubreil, Hervé Marchand

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

29 Citations (Scopus)

Abstract

In this paper, we address the problem of synthesizing opaque systems by selecting the set of observable events. We first investigate the case of static observability where the set of observable events is fixed a priori. In this context, we show that checking whether a system is opaque and computing an optimal static observer ensuring opacity are both PSPACE-complete problems. Next, we introduce dynamic partial observability where the set of observable events can change over time. We show how to check that a system is opaque w.r.t. a dynamic observer and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic observers under which S is opaque. Our main result is that the synthesis problem can be solved in EXPTIME.

Original languageEnglish
Title of host publicationAutomated technology for verification and analysis
Subtitle of host publication7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009, proceedings
EditorsZhiming Liu, Anders P. Ravn
Place of PublicationBerlin
PublisherSpringer, Springer Nature
Pages352-367
Number of pages16
ISBN (Print)3642047602, 9783642047602
DOIs
Publication statusPublished - 2009
Externally publishedYes
Event7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009 - Macao, China
Duration: 14 Oct 200916 Oct 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5799 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009
CountryChina
CityMacao
Period14/10/0916/10/09

Fingerprint Dive into the research topics of 'Dynamic observers for the synthesis of opaque systems'. Together they form a unique fingerprint.

Cite this