In this paper we propose an extension named AHyperPCTL to additionally introduce asynchronicity between the observed executions by quantifying over stutter-schedulers, which may randomly decide to delay scheduler decisions by idling. We show that AHyperPCTL can express interesting information-flow security policies, and propose a model checking algorithm for a decidable fragment.
The model checking problem for hyperproperties is challenging due to its inherent complexity of verifying properties across sets of traces and suffers from scalability issues. We have attempted to combine these two concepts to propose a tractable solution to model checking of hyperproperties expressed as HyperLTL on models involving nondeterminism. We have implemented our approach in PLASMA and experimented with a range of case studies to showcase its effectiveness.
We allow expression of the concept of rewards in probabilistic hyperproperties. We describe how it can be undefined in cases and suggest algorithms using which we can derive a defined answer from partial definedness. We additionally elaborate few interesting case studies for application and provide experimental results of the same.
We present a overview of our tool, HyperProb, which aims to verify probabilistic hyperproperties on Markov Decision Processes.
We prove that the model checking problem for verification of probabilistic hyperproperties on Markov Decision Processes is undecidable. We further provide a NP complex solution for a fragment of the same problem and provide experimental results of the same.
We solve the problem of synthesis of parameters in DTMCs given probabilistic hyperproperties that hold for the system.
We study the problem of formalizing and checking probabilistic hyperproperties for Markov decision processes (MDPs). We introduce the temporal logic HyperPCTL that allows explicit and simultaneous quantification over schedulers as well as probabilistic computation trees. We show that the logic can express important quantitative requirements in various fields. We show that HyperPCTL model checking over MDPs is in general undecidable, but restricting the domain of scheduler quantification to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language.
We proposed a method to find the extract tumor-affected region from brain MRI scans using rough k-means segmentation.
We proposed a method to find the best set of features that can help us distinguish between brain MRI scans with and without tumors. The segmentation method used here was rough k-means clustering
We proposed a method to find the best set of features that can help us distinguish between brain MRI scans with and without tumors. We used a fuzzy c-means clustering method.