### 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*.

### 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

- CAREER: Composition approaches for the analysis of complex systems, National Science Foundation. Andrew Miner (PI). 2006-2011.
- Software verification using plug and play components, National Science Foundation. Andrew Miner (PI), Samik Basu (Co-PI). 2005-2006.