This thesis focuses on two verification problems, both handling infinite-state systems. The first is model checking of sequential infinite-state systems. We present an algorithm for model-checking linear-time properties of pushdown and prefix-recognizable systems. We then show that model-checking pushdown systems with regular labeling is equivalent to model-checking prefix-recognizable systems. We extend the automata-theoretic approach to infinite-state systems to handle global model checking for both linear-time and branching-time properties. We then use the methods developed for reasoning about infinite-state sequential systems to offer a solution to the emptiness problem of pushdown nondeterministic parity tree automata. Using this new solution, we consider model checking of non-regular specifications with respect to finite-state systems. We show that model checking this type of specifications with respect to pushdown systems is undecidable. We introduce the class of micro-macro stack graphs, which extends the class of prefix-recognizable graphs, and give elementary algorithms for model-checking linear-time and branching-time specifications with respect to micro-macro stack graphs.
The second problem is uniform verification of parameterized systems. We suggest a heuristic that enables proving the correctness of liveness properties for a large class of parameterized systems. We start with systems in which the connection between the processes is relatively simple and show how to extend the method to systems in which moves of processes may depend on the state of neighboring processes and even on all other processes. We exhibit the usefulness of our approach by proving liveness for a few protocols for mutual exclusion.
The thesis is organized in the form of an edited collection of the extended versions of six published articles. The first four chapters are associated with systems with pushdown store and the last chapter is associated with parameterized systems.