Research on Automatic Verification of Finite-State Concurrent Systems

摘要: Abstract : This survey is organized as follows: Section 2 describes the syntax and semantics of temporal logics that are used in this paper. 3 states model checking problem give an efficient algorithm for simple branching-time formulas. 4 discusses issue fairness show how can be extended to include constraints. 5 demonstrates debug a mutual exclusion program. 6 some alternative approaches verifying systems finite state concurrent process. The complexity linear logic formulas analyzed techniques Pnueli Lichtenstein Vardi Wolper outlined. Additional applications circuit protocol verification discussed 7. paper concludes 8 with discussion important remaining research problems like explosion problem.