Probabilistic opacity for Markov decision processes

DOI10.1016/J.IPL.2014.09.001MaRDI QIDQ458386zbMATHOpenAlexFDO

Authors Béatrice Bérard, Krishnendu Chatterjee, Nathalie Sznajder

Publication date 7 October 2014

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1407.4225

zbMATH Keywords

decidabilityformal methodsMarkov decision processesopacityperfect and partial informationsecurity properties

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Markov and semi-Markov decision processes (90C40)

Abstract: Opacity is a generic security property, that has been defined on (non probabilistic) transition systems and later on Markov chains with labels. For a secret predicate, given as a subset of runs, and a function describing the view of an external observer, the value of interest for opacity is a measure of the set of runs disclosing the secret. We extend this definition to the richer framework of Markov decision processes, where non deterministic choice is combined with probabilistic transitions, and we study related decidability problems with partial or complete observation hypotheses for the schedulers. We prove that all questions are decidable with complete observation and $omega$-regular secrets. With partial observation, we prove that all quantitative questions are undecidable but the question whether a system is almost surely non opaque becomes decidable for a restricted class of $omega$-regular secrets, as well as for all $omega$-regular secrets under finite-memory schedulers.

Recommendations

• Opacity for linear constraint Markov chains
• Probabilistic system opacity in discrete event systems
• Generalizing Markov decision processes to imprecise probabilities
• Markov Decision Processes with Imprecise Transition Probabilities
• Partially observable Markov decision processes with imprecise parameters
• Markov decision processes under ambiguity
• Probabilistic Hyperproperties of Markov Decision Processes
• On the complexity of partially observed Markov decision processes
• Current-State Opacity Formulations in Probabilistic Finite Automata
• Optimality conditions for partially observable Markov decision processes

Cites work

• scientific article; zbMATH DE number 941396 (Why is no real title available?)
• scientific article; zbMATH DE number 765034 (Why is no real title available?)
• scientific article; zbMATH DE number 3371972 (Why is no real title available?)
• Algorithms for Omega-Regular Games with Imperfect Information
• Alternating finite automata on \(\omega\)-words
• Asymptotic information leakage under one-try attacks
• Current-State Opacity Formulations in Probabilistic Finite Automata
• Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification
• Opacity issues in games with imperfect information
• Probabilistic automata
• Probabilistic automata on finite words: decidable and undecidable problems
• Probabilistic ω-automata
• Qualitative analysis of partially-observable Markov decision processes
• Quantifying opacity
• Quantitative stochastic parity games
• Randomness for free
• Supervisory Control for Opacity
• Synthesis of opaque systems with static and dynamic masks
• The complexity of probabilistic verification
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Time-bounded reachability for monotonic hybrid automata: complexity and fixed points
• Verification of Infinite-Step Opacity and Complexity Considerations
• What is decidable about partially observable Markov decision processes with omega-regular objectives

Cited in

(14)

• Process opacity for timed process algebra
• Accurate approximate diagnosis of (controllable) stochastic systems
• Quantifying opacity
• The complexity of synchronous notions of information flow security
• Dynamics security policies and process opacity for timed process algebras
• Opacity for linear constraint Markov chains
• Information control in networked discrete event systems and its application to battery management systems
• Probabilistic disclosure: maximisation vs. minimisation
• Infinite-step opacity and \(K\)-step opacity of stochastic discrete-event systems
• A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
• Enforcement of opacity by public and private insertion functions
• Enforcing opacity of regular predicates on modal transition systems
• Opacity issues in games with imperfect information
• Game current-state opacity formulation in probabilistic resource automata

This page was built for publication: Probabilistic opacity for Markov decision processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q458386)