Title :
Extracting Unsatisfiable Cores for LTL via Temporal Resolution
Author :
Schuppan, Viktor
Abstract :
Unsatisfiable cores (UCs) are a well established means for debugging in a declarative setting. Still, tools that perform automated extraction of UCs for LTL are scarce. Using resolution graphs to extract UCs is common in many domains. In this paper we construct and optimize resolution graphs for temporal resolution as implemented in the temporal resolution-based solver TRP++ and we use them to extract UCs for propositional LTL. We implement our method in TRP++, and we experimentally evaluate it. Source code of our tool is available.
Keywords :
program debugging; temporal logic; TRP++; debugging; declarative setting; propositional LTL; resolution graphs; temporal resolution-based solver; unsatisfiable core extraction; Boolean functions; Business; Cognition; Data structures; Debugging; Partitioning algorithms; Production; LTL; temporal resolution; unsatisfiable cores; vacuity;
Conference_Titel :
Temporal Representation and Reasoning (TIME), 2013 20th International Symposium on
Conference_Location :
Pensacola, FL
Print_ISBN :
978-1-4799-2240-6
DOI :
10.1109/TIME.2013.15
