The paper presents an efficient algorithm 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 global state graph of the concurrent system. The authors also discuss how to adapt the approach to handle fairness conditions, which are essential for verifying systems with fair execution sequences. They argue that their technique can provide a practical alternative to manual proof construction or the use of mechanical theorem provers for verifying many finite-state concurrent systems. Experimental results show that the algorithm can check state machines with several hundred states in seconds. The paper includes a detailed description of the specification language, the model checking algorithm, and its extension to handle fairness. It also provides an example of using the extended model checker to verify the correctness of the Alternating Bit Protocol. Finally, the paper discusses more expressive logics and their complexity, concluding with a discussion of related work and open problems.The paper presents an efficient algorithm 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 global state graph of the concurrent system. The authors also discuss how to adapt the approach to handle fairness conditions, which are essential for verifying systems with fair execution sequences. They argue that their technique can provide a practical alternative to manual proof construction or the use of mechanical theorem provers for verifying many finite-state concurrent systems. Experimental results show that the algorithm can check state machines with several hundred states in seconds. The paper includes a detailed description of the specification language, the model checking algorithm, and its extension to handle fairness. It also provides an example of using the extended model checker to verify the correctness of the Alternating Bit Protocol. Finally, the paper discusses more expressive logics and their complexity, concluding with a discussion of related work and open problems.