Opacity for Linear Constraint Markov Chains - Sorbonne Université Access content directly
Reports (Research Report) Year : 2016

Opacity for Linear Constraint Markov Chains


On a partially observed system, a secret ϕ is opaque if an observer cannot ascertain that its trace belongs to ϕ. We consider specifications given as Constraint Markov Chains (CMC), which are underspec-ified Markov chains where probabilities on edges are required to belong to some set. The nondeterminism is resolved by a scheduler, and opacity on this model is defined as a worst case measure over all implementations obtained by scheduling. This measures the information obtained by a passive observer when the system is controlled by the smartest sched-uler in coalition with the observer. When restricting to the subclass of Linear CMC, we compute (or approximate) this measure and prove that refinement of a specification can only improve opacity.
Fichier principal
Vignette du fichier
bkms-hal.pdf (434.1 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01384153 , version 1 (19-10-2016)


  • HAL Id : hal-01384153 , version 1


Béatrice Bérard, Olga Kouchnarenko, John Mullins, Mathieu Sassolas. Opacity for Linear Constraint Markov Chains. [Research Report] LIP6 UMR 7606 UPMC Sorbonne Universités, France; Univ. de Franche-Comté; Ecole Polytechnique de Montréal; LACL, Université Paris-Est. 2016. ⟨hal-01384153⟩
257 View
282 Download


Gmail Facebook Twitter LinkedIn More