ACTL strong negation and its application to hybrid systems verification

Model checking procedures for verifying properties of hybrid dynamic systems are based on the construction of finite-state abstractions. If the property is not satisfied by the abstraction, the verification is inconclusive and the abstraction needs to be refined so that a less conservative model can be checked. If the hybrid system does not satisfy the property, this verify–refine procedure usually will not terminate. This paper introduces the concept of strong negation for ACTL formulas as an auxiliary condition that can be verified to obtain a conclusive negative verification result from a finite-state abstraction in certain cases. The concepts are illustrated with an example from automotive powertrain control.