Decidability of Parameterized Probabilistic Information Flow

In this paper, we consider the decidability of two problems related to information flow in a system with respect to some property. A flow occurs in a system if the conditional probability of the property under some partial observation differs from the a priori probability of that property. For systems modelled as finite Markov chains we prove that the two following problems are decidable: does a system has information flow for a given regular property? is it true that the system has no information flow for any (sequential) property?

• Type: Conference
• Year: 2007
• Where: CSR
• Authors: Danièle Beauquier, Marie Duflot, Yury Lifshits
• Keywords: CSR 2007, Information flow, Partial Observation Differs, finite Markov Chains