On ACTL Formulas Having Deterministic Counterexemplas

In case an ACTL formula φ 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 φ, then φ has a linear counterexample. We show that, given M and φ, where M |≠ φ, it is NP-hard to determine whether there exists a linear counterexample. Moreover, it is PSPACE-hard to decide whether an ACTL formula φ 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 φ which is an instance of a template γ* ε LIN, and for each Kripke structure M such that M |≠φ, a single path of M witnessing the failure by itself can be computed in polynomial time.