Providing fundamental theories and techniques for analyzing/verifying infinite-state systems is of great interest in many areas of computer science, such as embedded/hybrid systems, security protocol analysis, software verification, and even emerging areas like membrane and DNA computing. The traditional model-checking techniques are limited to finite-state systems, though most real-world systems (such as software designs) are inherently infinite-state. This research will investigate the use of automata-theoretic and related techniques (such as nonlinear Diophantine equations) in analyzing many forms of restricted infinite-state systems.
Specifically, the project will address the following issues: The first is to build a new automata theory for analyzing systems with dense counters and other unbounded discrete structures. The second issue is to develop a new verification technique based on nonlinear Diophantine equation theory. The third issue is to establish a new automata theory for nonuniversal membrane computing systems and study automata-theoretic approaches to DNA computing. The fourth issue is to use structural information on a transition system to improve the efficiency of verification algorithms and use complexity theory to obtain tight lower bounds for some of the algorithms. This project will significantly advance the state of the art of model-checking theories as well as automata theories. In the long term, this research will eventually provide practitioners with new verification techniques that will help engineers build current and future computing systems that are faster, better, and verifiable.
