On ACTL formulas having linear counterexamples

In case an ACTL formula phi fails over a transition graph M, it is most use ful 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 t he failure of phi, then phi has a linear counterexample. We show that, give n M and phi, where M does not satisfy phi, it is NP-hard to determine wheth er there exists a linear counterexample. Moreover, it is PSPACE-hard to dec ide 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 tem plates of ACTL formulas, i.e., skeletons of modal formulas whose atoms are disregarded. We identify the (unique) maximal set LIN of templates whose in stances (obtained by replacing atoms with arbitrary pure state formulas) al ways 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 wi tnessing the failure by itself can be computed in polynomial time. (C) 2001 Academic Press.