Research

Overview

Broadly speaking, I am interested in techniques for analyzing large discrete-state systems. Examples of such systems include computer communication networks, multi-threaded software, network protocols, and tile assembly systems. I work in the areas of model checking and performance evaluation and have interests in developing software tools.

Model checking

Model checking is the process of determining if a system, described as a (usually nondeterministic) model, satisfies some properties. These properties are expressed using an appropriate logic, such as the temporal logics LTL or CTL. If the system model describes a finite state machine, then the model checking problem is decidable. In practice, however, the finite state machines can be extremely large. Researchers use a variety of techniques to overcome this; I am mainly interested in using a data structure called decision diagrams.  Much of my work involves developing new variations of decision diagrams, and improving algorithms to construct or manipulate decision diagrams.

Performance evaluation

If a system is described using a stochastic model, rather than a nondeterministic model, then the model ultimately generates a stochastic process. Properties of the system can then either be queried (e.g., "What is the probability that a packet is lost") or expressed using a stochastic logic such as pCTL or CSL (e.g., "The probability of a lost packet is less than 0.000001"). In either case, these properties are determined by analyzing the underlying stochastic process, which is typically a Markov chain. 

Past grants