Compositional Automata Reduction with Non-critical Path Slicing

Model checking is a formal verification method that automatically checks whether a system satisfies its property or not. The system behavior can be modeled by a system state graph, and the model checker will explore the entire system state graph to verify design correctness. However, model checking is limited by the state space explosion problem. Model reduction techniques alleviate this limitation by reducing the model size and preserve sufficient information to verify the system against a given property. In this Thesis, we present a compositional reduction method that reduces the automata model before the system state graph is generated. Reduction is based on the semantics for temporal logic properties of the forms EG(f1) and E(f1 U f2), where f1 and f2 are propositional logics. Non-critical paths which do that affect the property are sliced out through the elimination of property independent transitions. We theoretically justified our reduction method and provided experimental results on several case studies.