A Two-phase Approximation for Model Checking Probabilistic Systems

Date: 
Monday, October 4, 2010 - 9:43am

UCSB COMPUTER SCIENCE DEPARTMENT PRESENTS:

Monday, October 25, 2010
11:00 AM – 12:00 PM
Computer Science Conference Room, Harold Frank Hall Rm. 1132

HOST: Tevfik Bultan

SPEAKER: Samik Basu
Computer Science Department, Iowa State University

Title: A Two-phase Approximation for Model Checking Probabilistic Systems

Abstract:

A large variety of systems from different domains exhibit probabilistic behavior; examples include distributed and consensus algorithms that rely on coin-tossing to break ties; protocols where messages are exchanged via lossy channels and/or where computations are undone due to unreliability. Such system behaviors are captured using probabilistic models. The process of verifying the correctness of these models in a probabilistic sense is called probabilistic model checking. I will discuss probabilistic model checking of systems modeled as Discrete Time Markov Chains (DTMC). While several techniques are available for model checking of DTMC, these techniques become un-usable and/or inefficient when the model under consideration is prohibitively large. In these situations we deploy approximate techniques, which do not rely on exploring all possible model behavior. These techniques are based on (a) obtaining sample simulations to estimate probability with which a model satisfies certain property and (b) applying statistical bounds to control the error in the estimates. In this talk, I will present a new technique for approximate probabilistic model checking and discuss its advantages over the existing techniques.

Bio:

Samik Basu is Associate Professor in the Department of Computer Science at Iowa State University. He received BE in Computer Science and Engineering from Jadavpur University, India, and earned MS and PhD from the State University of New York at Stony Brook. His primary area of research is model checking. He is also involved in projects on application of formal methods in Web services, intrusion detection and software product-line verification.