Model-checking bisimulation-based information flow properties for pushdown systems

Deepak D'Souza, K.R.Raghavendra

Abstract: Bisimulation-based information flow properties were intro- duced by Focardi and Gorrieri in 2005 as a way of specifying security properties for transition system models. These properties were shown to be decidable for finite-state systems. In this paper, we study the problem of verifying these properties for some well-known classes of infinite state systems. We show that all the properties are undecidable for each of these classes of systems.