Probabilistic opacity for Markov decision processes

DOI10.1016/J.IPL.2014.09.001zbMATH Open1366.68213arXiv1407.4225OpenAlexW2090930915MaRDI QIDQ458386FDOQ458386

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

Publication date: 7 October 2014

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

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.

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

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

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)

Cites Work

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

Cited In (14)

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

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)