Repeated Lipton Reduction in Trace Abstraction Refinement

Project Goal

Integrate Petri net-based Trace Abstraction Refinement with a form of Partial Order Reduction, namely Lipton reduction. We want to evaluate how this affects verification runtime. We extend the one-time up-front Lipton reduction previously implemented in Ultimate (see this project) in order to apply it also to refined Petri nets. We hope to benefit from the reduced degree of concurrency in the refined net, as well as from usage of conditional POR.

Current Tasks

• Revise & complete proposal (Target: Sunday, Feb 07)
• Research & start registration process
• Document results on generalized Lipton sequence rule (from email) in a project report
• Begin implementation:
  • branch wip/dk/repeated-lipton
  • create new CEGAR loop (derived from CegarLoopForPetriNet)
  • extend Lipton reduction implementation to handle structure of refined nets, including using transitions in CoenabledRelation
• [future] Consider conditional independence
  • determine possible usage of conditions (predicates)
  • extend implementation