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

• Research & start registration process
• Document results on generalized Lipton sequence rule (from emails) in a project report
• Begin implementation:
  • branch wip/dk/repeated-lipton
  • extend Lipton reduction implementation to handle structure of refined nets, including using transitions in CoenabledRelation
• Collect example programs that show benefit of repeated POR
• [future] Consider conditional independence
  • determine possible usage of conditions (predicates)
  • extend implementation