Automata-Driven Partial Order Reduction and Guided Search for LTL Model CheckingRemote
In LTL model checking, a system model is synchronized using the product construction with Buchi automaton representing all runs that invalidate a given LTL formula. An existence of a run with infinitely many occurrences of an accepting state in the product automaton then provides a counter-example to the validity of the LTL formula. Classical partial order reduction methods for LTL model checking allow to considerably prune the searchable state space, however, the majority of published approaches do not use the information about the current Buchi state in the product automaton. We demonstrate that this additional information can be used to significantly improve the performance of existing techniques. In particular, we present a novel partial order method based on stubborn sets and a heuristically guided search, both driven by the information of the current state in the Buchi automaton. We implement these techniques in the model checker TAPAAL and an extensive benchmarking on the dataset of Petri net models and LTL formulae from the 2021 Model Checking Contest documents that the combination of the automata-driven stubborn set reduction and heuristic search improves the state-of-the-art techniques by a significant margin.
Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 11:50 | |||
10:20 30mPaper | Automata-Driven Partial Order Reduction and Guided Search for LTL Model CheckingRemote VMCAI Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba Aalborg University, Nikolaj Jensen Ulrik Aalborg University, Simon Mejlby Virenfeldt Aalborg University | ||
10:50 30mPaper | Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not TerminateRemote VMCAI Rahmadi Trimananda University of California at Irvine, USA, Weiyu Luo University of California, Irvine, Brian Demsky University of California at Irvine, Harry Xu University of California, Los Angeles (UCLA) Link to publication DOI Pre-print Media Attached File Attached | ||
11:20 30mPaper | Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsInPerson VMCAI |