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

- SI2 - SSE: A Next-Generation Decision Diagram Library, National Science Foundation. Andrew Miner (PI), Gianfranco Ciardo. 2017-2019.
- 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.