Utilizing the structure of safety properties to aid in the verification of hybrid controllers

Identifying hazardous states in a system and ensuring they are not reachable is an ongoing problem in any large system safety analysis. An exhaustive search of most complex process-control systems encounters the problem of state explosion. The use of predicate abstraction has been studied and employed to great effect. However, in this paper, we outline a novel approach, which utilizes the structure of the safety property to be verified to mitigate state explosion. The state explosion problem is minimized by creating an abstraction that partitions the state space into equivalence classes based on the predicates of the safety property. An ordering on these predicates, based on the number of continuous variables inherent to each term, is used to develop the set of equivalence classes that minimizes the number of continuous variables that must be computed in order to determine if a transition between classes occurs. This acts to minimize the computational complexity of calculating reachability sets by limiting the number of continuous variables that need to be explicitly calculated. The work is then put in the context of an air traffic conflict detection example problem, and conclusions regarding scalability are drawn.