CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)

Roberto Pettinau, Christoph Matheja

We study model checking algorithms for infinite families of finite-state labeled transition systems against temporal properties written in CTL*. Such families arise, for example, a…