On ACTL formulas having linear counterexamples

In case an ACTL formula phi fails over a transition graph M, it is most useful to provide a counterexample, i.e., a computation tree of M, witnessing the failure. If there exists a single path in M which by itself witnesses the failure of phi, then phi has a linear counterexample. We show that, given M and phi, where M does not satisfy phi, it is NP-hard to determine whether there exists a linear counterexample. Moreover, it is PSPACE-hard to decide whether an ACTL formula phi always admits a linear counterexample if it fails. This means that there exists no simple characterization of the ACTL formulas that guarantee linear counterexamples. Consequently, we study templates of ACTL formulas, i.e., skeletons of modal formulas whose atoms are disregarded. We identify the (unique) maximal set LIN of templates whose instances (obtained by replacing atoms with arbitrary pure state formulas) always guarantee linear counterexamples. We show that For each ACTL formula g which is an instance of a template gamma (star)* epsilon LIN, and for each Kripke structure M such that M does not satisfy phi, a single path of M witnessing the failure by itself can be computed in polynomial time. (C) 2001 Academic Press.