A novel abstraction-guided simulation approach using posterior probabilities for verification

This paper presents a novel abstraction-guided simulation approach for multiple target states which uses posterior probabilities of the states from the abstract model, instead of abstract distances used by former abstraction-guided approaches, as the guidance of simulation. The posterior probabilities carry more precise information of the abstract model, being able to offer more effective guidance as well as allow the simulation to deal with multiple target states at a time. Experimental results show that the simulation using posterior probabilities as guidance is much more efficient than that using the abstract distances, and the multiple target states simulation framework reduces the simulation cycles effectively.