@inproceedings{56796209b69e4b279ea167d972e3932b,
title = "Dynamic observers for the synthesis of opaque systems",
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.",
author = "Franck Cassez and J{\'e}r{\'e}my Dubreil and Herv{\'e} Marchand",
year = "2009",
doi = "10.1007/978-3-642-04761-9_26",
language = "English",
isbn = "3642047602",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer, Springer Nature",
pages = "352--367",
editor = "Zhiming Liu and Ravn, {Anders P.}",
booktitle = "Automated technology for verification and analysis",
address = "United States",
note = "7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009 ; Conference date: 14-10-2009 Through 16-10-2009",
}