On ACTL Formulas Having Deterministic Counterexamples

. In case an ACTL formula OE fails over a labeled transition graph M , it is most useful toprovide a counterexample, i.e., a computation tree of M witnessing the failure. If there exists asingle path in M which by itself witnesses the failure of OE, then OE has a deterministic counterexample.We show that, given M and OE, where M 6j= OE, it is NP-hard to determine whether thereexists a deterministic counterexample. Moreover, it is PSPACE-hard to decide whether an ACTLformula OE always...