On-the-fly Unfolding with Optimal Exploration for Linear Temporal Logic Model Checking of Concurrent Software and Systems

Shuo Li, Liao Zheng, Ru Yang +1

Context: Linear temporal logic (LTL) model checking faces a significant challenge known as the state-explosion problem. The on-the-fly method is a solution that constructs and chec…