Decidability of Model Checking for Infinite-State Concurrent Systems

Javier Esparza

Abstract: We study the decidability of the model checking problem for linear and branching time logics, and two models of concurrent computation, namely Petri nets and Basic Parallel Processes.

LFCS report ECS-LFCS-94-302, August 1994.

Javier Esparza is now at the Department of Computer Science, Technische Universität München, where his email address is esparza@informatik.tu-muenchen.de.

Previous | Index | Next