@inproceedings{DBLP:conf/atva/CassezDM09,
  author    = {Franck Cassez and
               J{\'{e}}r{\'{e}}my Dubreil and
               Herv{\'{e}} Marchand},
                 editor    = {Zhiming Liu and
               Anders P. Ravn},
  title     = {Dynamic Observers for the Synthesis of Opaque Systems},
  booktitle = {Automated Technology for Verification and Analysis, 7th International
               Symposium, {ATVA} 2009, Macao, China, October 14-16, 2009. Proceedings},
  pages     = {352--367},
  year      = {2009},
    series    = {Lecture Notes in Computer Science},
  volume    = {5799},
  publisher = {Springer},
  url       = {http://dx.doi.org/10.1007/978-3-642-04761-9_26},
  doi       = {10.1007/978-3-642-04761-9_26},
    urlpaper = {papers/atva-09.pdf},
  urlslides = {papers/slides-atva-09.pdf},
        Type = {B - International Conferences},

  ABSTRACT = {   In this paper, we address the problem of synthesizing \emph{opaque}
  systems by selecting the set of observable
  events.
  We first investigate the case of \emph{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 \emph{dynamic} partial observability where the
  set of observable events
  can
  change over time.
  We show how to check that a system is opaque \wrt 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.},
}

{"_id":"uHMQt3BA7YGSd5ZNi","bibbaseid":"cassez-dubreil-marchand-dynamicobserversforthesynthesisofopaquesystems-2009","author_short":["Cassez, F.","Dubreil, J.","Marchand, H."],"bibdata":{"bibtype":"inproceedings","type":"B - International Conferences","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Jérémy"],"propositions":[],"lastnames":["Dubreil"],"suffixes":[]},{"firstnames":["Hervé"],"propositions":[],"lastnames":["Marchand"],"suffixes":[]}],"editor":[{"firstnames":["Zhiming"],"propositions":[],"lastnames":["Liu"],"suffixes":[]},{"firstnames":["Anders","P."],"propositions":[],"lastnames":["Ravn"],"suffixes":[]}],"title":"Dynamic Observers for the Synthesis of Opaque Systems","booktitle":"Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings","pages":"352–367","year":"2009","series":"Lecture Notes in Computer Science","volume":"5799","publisher":"Springer","url":"http://dx.doi.org/10.1007/978-3-642-04761-9_26","doi":"10.1007/978-3-642-04761-9_26","urlpaper":"papers/atva-09.pdf","urlslides":"papers/slides-atva-09.pdf","abstract":"In this paper, we address the problem of synthesizing \\emphopaque systems by selecting the set of observable events. We first investigate the case of \\emphstatic 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 \\emphdynamic partial observability where the set of observable events can change over time. We show how to check that a system is opaque ≀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.","bibtex":"@inproceedings{DBLP:conf/atva/CassezDM09,\n author = {Franck Cassez and\n J{\\'{e}}r{\\'{e}}my Dubreil and\n Herv{\\'{e}} Marchand},\n editor = {Zhiming Liu and\n Anders P. Ravn},\n title = {Dynamic Observers for the Synthesis of Opaque Systems},\n booktitle = {Automated Technology for Verification and Analysis, 7th International\n Symposium, {ATVA} 2009, Macao, China, October 14-16, 2009. Proceedings},\n pages = {352--367},\n year = {2009},\n series = {Lecture Notes in Computer Science},\n volume = {5799},\n publisher = {Springer},\n url = {http://dx.doi.org/10.1007/978-3-642-04761-9_26},\n doi = {10.1007/978-3-642-04761-9_26},\n urlpaper = {papers/atva-09.pdf},\n urlslides = {papers/slides-atva-09.pdf},\n Type = {B - International Conferences},\n\n ABSTRACT = { In this paper, we address the problem of synthesizing \\emph{opaque}\n systems by selecting the set of observable\n events.\n We first investigate the case of \\emph{static} observability\n where the set of observable events\n is fixed a priori. In this context, we show that checking whether a\n system is opaque and computing an optimal static observer ensuring\n opacity are both PSPACE-complete problems.\n Next, we introduce \\emph{dynamic} partial observability where the\n set of observable events\n can\n change over time.\n We show how to check that a system is opaque \\wrt a dynamic observer\n and also address the corresponding synthesis problem: given a system\n $G$ and secret states $S$, compute the set of dynamic observers\n under which $S$ is opaque. Our main result is that the synthesis\n problem can be solved in EXPTIME.},\n}\n\n\n","author_short":["Cassez, F.","Dubreil, J.","Marchand, H."],"editor_short":["Liu, Z.","Ravn, A. P."],"key":"DBLP:conf/atva/CassezDM09","id":"DBLP:conf/atva/CassezDM09","bibbaseid":"cassez-dubreil-marchand-dynamicobserversforthesynthesisofopaquesystems-2009","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/atva-09.pdf","Slides":"http://science.mq.edu.au/~fcassez/bib/papers/slides-atva-09.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":[],"search_terms":["dynamic","observers","synthesis","opaque","systems","cassez","dubreil","marchand"],"title":"Dynamic Observers for the Synthesis of Opaque Systems","year":2009}