Guest lecture by
Dr. Oscar H. Ibarra
|
Title
Reachability and Safety in Infinite-State Systems
Speaker
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:
- 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.
- 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.
![](pic/ibarra.jpg)
Dr. Oscar H. Ibarra
|