Efficient Stochastic Model Checking
Background. Stochastic processes are used in hardware and software analysis to model the uncertainly or randomness involved in the systems. These randomness/uncertainty arises from the the inputs of the model, and based on these uncertainty different outcomes of the model are predicted. Different safety properties, security and privacy policies, or performance and dependability measures can be expressed as properties defined on stochastic processes. Among different probabilistic models, we make extensive use of discrete-time Markov chains (DTMCs) and continuous-time Markov chains (CTMCs) in our work. Probabilistic model checking takes a stochastic model represented as a DTMC or CTMC and a property represented in a probabilistic temporal logic, and uses numerical or analytical methods to compute the likelihood of different events thus, to verify the property. The specification language used for DTMCs is called probabilistic computation tree logic (PCTL), a probabilistic extension of the logic CTL, while the specification language used for CTMCs is called continuous stochastic logic (CSL), a probabilistic extension of the logic CTL.
Completed work. Probabilistic hyperproperties describe system properties involving probability measures over independent runs and have applications in many areas, for example information-flow security. We develop efficient model checking algorithm to verify HyperPCTL properties (HyperPCTL is the extension of PCTL to hyerproperties). This is needed in practice because the poor scalability of existing HyperPCTL model checking algorithms limits its use to small models. Our algorithm reduces the dimensionality of the matrices that need to be computed, first by exploiting the semantics and position of the variable quantifiers in the HyperPCTL formula, then by applying probabilistic decomposition arguments. Experimentally, we show that our algorithm significantly outperforms both a SAT-solver symbolic approach and the original approach based on brute-force self-composition.
Work in progress #1. We are exploring new operators for the logics PCTL and CSL that increase their expressiveness. We plan to develop efficient numerical algorithms to evaluate these operators. Work in progress #2. We plan to define HyperCSL, the extension of logic CSL to express and verify hyperproperties and investigate efficient numerical algorithms analogous to those for HyperPCTL.
Both works in progress were initially motivated by discussions about CRNs with Prof. Jim Lathrop and Prof. Titus Klinge, and we expect this to be one of the applications we will explore.
Committee: Gianfranco Ciardo (co-major professor), Borzoo Bonakdarpour (co-major professor), Samik Basu, Jack Lutz, Andrew Miner, and Farzad Sabzikar.
Join on Zoom: Please click this URL to start or join. https://iastate.zoom.us/j/91896203257 or, go to https://iastate.zoom.us/join and enter meeting ID: 918 9620 3257