Model checking differentially private properties

DOI10.1016/J.TCS.2022.10.002MaRDI QIDQ2680992zbMATH OpenOpenAlexFDO

Authors Depeng Liu, Bow-Yaw Wang, Chen Fu, Lijun Zhang

Publication date 5 January 2023

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2022.10.002

zbMATH Keywords

model checkingdifferential privacytemporal logic

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Model checking differentially private properties
• Probabilistic relational reasoning for differential privacy
• Deciding differential privacy for programs with finite inputs and outputs
• Differential privacy in probabilistic systems
• The algorithmic foundations of differential privacy

Cites work

• scientific article; zbMATH DE number 5685899 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3371972 (Why is no real title available?)
• A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata
• A logic for reasoning about time and reliability
• An optimal automata approach to LTL model checking of probabilistic systems
• Bisimilarity distances for approximate differential privacy
• Deciding differential privacy for programs with finite inputs and outputs
• Differential Privacy
• Differential privacy under continual observation
• Distance makes the types grow stronger: a calculus for differential privacy
• Formal verification of differential privacy for interactive systems (extended abstract)
• Generalized Bisimulation Metrics
• Higher-order approximate relational refinement types for mechanism design and differential privacy
• LightDP: towards automating differential privacy proofs
• Linear dependent types for differential privacy
• Markov chains and unambiguous Büchi automata
• Model checking differentially private properties
• Model checking of probabilistic and nondeterministic systems
• Preserving differential privacy under finite-precision semantics
• Probabilistic automata
• Probabilistic relational reasoning for differential privacy
• Proving differential privacy via probabilistic couplings
• The algorithmic foundations of differential privacy
• The big-O problem for labelled Markov chains and weighted automata
• The complexity of probabilistic verification
• Theory of Cryptography
• Universally utility-maximizing privacy mechanisms
• Universally utility-maximizing privacy mechanisms
• Verifying Pufferfish privacy in hidden Markov models

Cited in

(2)

• Deciding differential privacy for programs with finite inputs and outputs
• Model checking differentially private properties

Describes a project that uses

Uses Software

• iscasMc
• LightDP
• PrivateLR
• PRISM

This page was built for publication: Model checking differentially private properties

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