What is the form of a counterexample for a ACTL* formula?

141 Views Asked by At

Given a Kripke structure $K$ and an $ACTL$ formula $\phi$ you can attest that it's false by finding a counterexample, more precisely a path, eventually followed by a loop.

Is there an equivalent concept of counterexample for an $ACTL^*$ formula? If it exists, what form does it have? Is it a path, a tree, or what else?

Does something change if the structure $K$ is finite?