Title

Reachability and Safety in Infinite-State Systems

Speaker

• Dr. Oscar H. Ibarra
• Department of Computer Science, University of California, Santa Barbara, USA

Time and Place

• Monday, September 25, 2000
• at 14.15
• Lecture Room A414 (4th floor), Department of Computer Science

Abstract

In the first part of the talk, we look at a model of a queue system that consists of the following components:

1. Two nondeterministic finite-state machines W and R, each augmented with finitely many counters with the property that each counter can be incremented or decremented by 1 and tested for zero, but the number of alternations between nondecreasing mode and nonincreasing mode is bounded by a constant.
2. One unrestricted (unbounded) queue that can be used to send messages from W (the "writer") to R (the "reader").

W and R operate at the same clock rate, i.e., each transition takes one time unit. There is no central control. We show that verification problems such as (binary, forward, and backward) reachability and safety for these systems are solvable. We also consider some reachability questions concerning machines operating in parallel.

In the second part of the talk, we describe a general automata-theoretic approach for analyzing the verification problems for discrete timed automata augmented with various data structures. We give examples of such structures and exhibit some new properties of discrete timed automata that can be verified.

Biography

Oscar H. Ibarra received the B.S. degree in Electrical Engineering from the University of the Philippines in 1962 and the M.S. and Ph.D. degrees, also in Electrical Engineering, from the University of California, Berkeley, in 1965 and 1967, respectively. He is currently a Professor of Computer Science at the University of California, Santa Barbara, where he served as Department Chair from 1997-1999. He was previously with the faculties of UC Berkeley (1967-1969) and the University of Minnesota (1969-1990).

Dr. Ibarra's research interests include the design and analysis of algorithms, the theory of computation, computational complexity, and parallel computing. He is a Fellow of the Association for Computing Machinery (ACM), a Fellow of the Institute of Electrical and Electronics Engineers (IEEE), a Fellow of the American Association for the Advancement of Science (AAAS), and a Fellow of the Minnesota Supercomputer Institute. He is a recipient of a John Simon Guggenheim Fellowship.

Dr. Ibarra is the Editor-in-Chief of the International Journal of Foundations of Computer Science. He is on the editorial boards of Theoretical Computer Science, Journal of Parallel and Distributed Computing, and Journal of Computing and Information. He has also served on the editorial boards of the IEEE Transactions on Computers, IEEE Transactions on Parallel and Distributed Systems, and Journal of VLSI Signal Processing. He is on the advisory board of the IEEE Technical Committee on Parallel Processing.

Dr. Oscar H. Ibarra