DISJUNCTIVE TRANSITION RELATION DECOMPOSITION BASED VERIFICATION

摘要

A method and system for building disjunctive transition relation decompositions of a system and obtaining reachable states from manipulation of the transition relation. Properties of the system may be verified by analyzing reachable states obtained with respect to a target specification of the system.