This paper presents an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a propositional, branching-time temporal logic. The algorithm has linear complexity in both the size of the specification and the size of the global state graph for the concurrent system. The approach is adapted to handle fairness by modifying the semantics of the logic to consider only fair paths. The algorithm, called a model checker, is similar to global flow analysis algorithms used in compiler optimization and has linear complexity in both the size of the structure and the specification. Experimental results show that state machines with several hundred states can be checked in a matter of seconds. The paper discusses the use of temporal logic for specifying concurrent systems, the extension of the model checking algorithm to handle fairness, and the application of the algorithm to verify the correctness of the Alternating Bit Protocol. The paper also considers extended logics that are more expressive than CTL and investigates their usefulness for automatic verification of finite-state concurrent programs. The model checking problem for CTL* is shown to be PSPACE-complete, and the model checking problem for BT* and CTL+ is shown to be both NP-hard and co-NP-hard and is in Δ₂^P. The paper concludes with a discussion of related work and remaining open problems.This paper presents an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a propositional, branching-time temporal logic. The algorithm has linear complexity in both the size of the specification and the size of the global state graph for the concurrent system. The approach is adapted to handle fairness by modifying the semantics of the logic to consider only fair paths. The algorithm, called a model checker, is similar to global flow analysis algorithms used in compiler optimization and has linear complexity in both the size of the structure and the specification. Experimental results show that state machines with several hundred states can be checked in a matter of seconds. The paper discusses the use of temporal logic for specifying concurrent systems, the extension of the model checking algorithm to handle fairness, and the application of the algorithm to verify the correctness of the Alternating Bit Protocol. The paper also considers extended logics that are more expressive than CTL and investigates their usefulness for automatic verification of finite-state concurrent programs. The model checking problem for CTL* is shown to be PSPACE-complete, and the model checking problem for BT* and CTL+ is shown to be both NP-hard and co-NP-hard and is in Δ₂^P. The paper concludes with a discussion of related work and remaining open problems.