Temporal logics are useful for describing dynamic system behavior, and have been successfully used as a language for goal definitions during task planning. Prior works on inferring temporal logic specifications have focused on "summarizing" the input dataset -- i.e., finding specifications that are satisfied by all plan traces belonging to the given set. In this paper, we examine the problem of inferring specifications that describe temporal differences between two sets of plan traces. We formalize the concept of providing such contrastive explanations, then present a Bayesian probabilistic model for inferring contrastive explanations as linear temporal logic specifications. We demonstrate the efficacy, scalability, and robustness of our model for inferring correct specifications across various benchmark planning domains and for a simulated air combat mission. In a meeting where multiple plan options are under deliberation by a team, it would be helpful for that team's resolution process if someone could intuitively explain how the plans under consideration differ from one another. Also, given a need to identify differences in execution behavior between distinct groups of users (e.g., a group of users who successfully completed a task using a particular system versus those who did not), explanations that identify distinguishing patterns between group behaviors can yield valuable analytics and insights toward iterative system refinement.In this paper, we seek to generate explanations for how two sets of divergent plans differ. We focus on generating such contrastive explanations by discovering specifications satisfied by one set of plans, but not the other. Prior works on plan explanations include those related to plan recognition for inferring latent goals through observations BID25 BID35 , works on system diagnosis and excuse generation in order to explain plan failures BID29 BID10 , and those focused on synthesizing "explicable" plans -i.e., plans that are self-explanatory with respect to a human's mental model BID16 . The aforementioned works, however, only involve the explanation or generation of a single plan; we instead focus on explaining differences between multiple plans, which can be helpful in various applications, such as the analysis of competing systems and compliance models, and detecting anomalous behaviour of users.A specification language should be used in order to achieve clear and effective plan explanations. Prior works have considered surface-level metrics such as plan cost and action (or causal link) similarity measures to describe plan differences BID23 BID3 . In this work, we leverage linear temporal logic (LTL) BID24 which is an expressive language for capturing temporal relations of state variables. We use a plan's individual satisfaction (or dissatisfaction) of LTL specifications to describe their differences.LTL specifications have been widely used in both industrial systems and planning algorithms to compactly describe temporal properties BID32 . They are human interpretable when expressed as compositions of predefined templates; inversely, they can be constructed from natural language descriptions BID7 ) and serve as natural patterns when encoding high-level human strategies for planning constraints BID14 .Although a suite of LTL miners have been developed for software engineering and verification purposes BID32 BID17 BID28 , they primarily focus on mining properties that summarize the overall behavior on a single set of plan traces. Recently , BID22 presented SAT-based algorithms to construct a LTL specification that asserts contrast between two sets of traces. The algorithms , however, are designed to output only a single explanation, and are susceptible to failure when the input contains imperfect traces. Similar to Neider and Gavran, our problem focuses on mining contrastive explanations between two sets of traces, but we adopt a probabilistic approach -we present a Bayesian inference model that can generate multiple explanations while demonstrating robustness to noisy input. The model also permits scalability when searching in large hypothesis spaces and allows for flexibility in incorporating various forms of prior knowledge and system designer preferences. We demonstrate the efficacy of our model for extracting correct explanations on plan traces across various benchmark planning domains and for a simulated air combat mission.Plan explanations are becoming increasingly important as automated planners and humans collaborate. This first involves humans making sense of the planner's output (e.g., PDDL plans), where prior work has focused on developing user-friendly interfaces that provide graphical visualizations to describe the causal links and temporal relations of plan steps BID1 BID26 BID21 . The outputs of these systems , however, require an expert for interpretation and do not provide a direct explanation as to why the planner made certain decisions to realize the outputted plan.Automatic generation of explanations has been studied in goal recognition settings, where the objective is to infer the latent goal state that best explains the incomplete sequence of observations BID25 BID30 . Works on explicable planning emphasize the generation of plans that are deemed selfexplanatory, defined in terms of optimizing plan costs for a human's mental model of the world BID16 . Mixed-initiative planners iteratively revise their plan generation based on user input (e.g. action modifications), indirectly promoting an understanding of differences across newly generated plans through continual user interaction BID27 BID3 . All aforementioned works deal with explainability with respect to a single planning problem specification, whereas our model deals with explaining differences in specifications governing two distinct sets of plans given as input.Works on model reconciliation focus on producing explanations for planning models (i.e. predicates, preconditions and effects), instead of the realized plans . Explanations are specified in the form of model updates , iteratively bringing an incomplete model to a more complete world model. The term, "contrastive explanation," is used in these works to identify the relevant differences between the input pair of models. Our work is similar in spirit but focuses on producing a specification of differences in the constraints satisfied among realized plans. Our approach takes sets of observed plans as input rather than planning models.While model updates are an important modality for providing plan explanations, there are certain limitations. We note that an optimal plan generated with respect to a complete environment/world model is not always explicable or self-explanatory. The space of optimal plans may be large, and the underlying preference or constraint that drives the generation of a particular plan may be difficult to pre-specify and incorporate within the planning model representation. We focus on explanations stemming directly from the realized plans themselves. Environment/world models (e.g. PDDL domain files) can be helpful in providing additional context, but are not necessary for our approach.Our work leverages LTL as an explanation language. Temporal patterns can offer greater expressivity and explanatory power in describing why a set of plans occurred and how they differ, and may reveal hidden plan dynamics that cannot be captured by the use of surface-level metrics like plan cost or action similarities. Our work on using LTL for contrastive explanations directly contributes to exploring how we can answer the following roadmap questions for XAIP BID9 : "why did you do that? why didn't you do something else (that I would have done)?" Prior research into mining LTL specifications has focused on generating a "summary" explanation of the observed traces. BID12 explored mining globally persistent specifications from demonstrated action traces for a finite state Markov decision process. BID17 introduced Texada, a system for mining all possible instances of a given LTL template from an output log where each unique string is represented as a new proposition. BID28 proposed a template-based probabilistic model to infer task specifications given a set of demonstrations. However, all of these approaches focus on inferring a specification that all the demonstrated traces satisfy.For contrastive explanations, Neider and Gavran (2018) presented SAT-based algorithms to infer a LTL specification that delineates between the positive and negative sets of traces. Unlike existing LTL miners, the algorithms construct an arbitrary, minimal LTL specification without requiring predefined templates. However, they are designed to output only a single specification, and can fail when the sets contain imperfect traces (i.e., if there exists no specification consistent with every single input trace.). We present a probabilistic model for the same problem and generate multiple contrastive explanations while offering robustness to noisy input.Some works have proposed algorithms to infer contrastive explanations for continuous valued time-series data based on restricted signal temporal logic (STL) grammar BID33 BID15 . However, the continuous space semantics of STL and a restricted subset of temporal operators make the grammar unsuitable for use with planning domain problems. To the best of our knowledge, our proposed model is the first probabilistic model to infer contrastive LTL specifications for sets of traces in domains defined by PDDL. The runtime for our model and the delimited enumeration baseline with 2,000 samples ranged between 1.2-4.7 seconds (increase in |V | only had marginal effect on the runtime). The SAT-based miner by Neider and Gavran often failed to generate a solution within a five minute cutoff (see the number of its timeout cases in the last column of TAB2 ). The prior work can only output a single ϕ * , which frequently took on a form of Fp i . It did not scale well to problems that required more complex ϕ as solutions. This is because increasing the "depth" of ϕ (the number of temporal / Boolean operators and propositions) exponentially increased the size of the compiled SAT problem. In our experiments, the prior work timed out for problems requiring solutions with depth ≥ 3 (note that Fp i has depth of 2). Robustness to Noisy Input In order to test robustness, we perturbed the input X by randomly swapping traces between π A and π B . For example, a noise rate of 0.2 would swap 20% of the traces, where the accuracy of ϕ ground on the perturbed data, X = ( π A , π B ), would evaluate to 0.8 (note that it may be possible to discover other ϕ that achieve better accuracy on X). The MAP estimates inferred from X, { ϕ * }, were evaluated on the original input X to assess any loss of ability to provide contrast. Figure 3 shows the average accuracy of { ϕ * }, evaluated on both X and X, across varying noise rate. Even at a moderate noise rate of 0.25, the inferred ϕ * s were able to maintain an average accuracy greater than 0.9 on X. Such a threshold is promising for real-world applications. The robustness did start to sharply decline as noise rate increased past 0.4. For all test cases, the Neider and Gavran miner failed to generate a solution for anything with a noise rate ≥ 0.1. We have presented a probabilistic Bayesian model to infer contrastive LTL specifications describing how two sets of plan traces differ. Our model generates multiple contrastive explanations more efficiently than the state-of-the-art and demonstrates robustness to noisy input. It also provides a principled approach to incorporate various forms of prior knowledge or preferences during search. It can serve as a strong foundation that can be naturally extended to multiple input sets by repeating the algorithm for all pairwise or one-vs.-rest comparisons.Interesting avenues for future work include gauging the saliency of propositions, as well as deriving a minimal set of contrastive explanations. Furthermore , we seek to test the model in human-in-the-loop settings, with the goal of understanding the relationship between different planning heuristics for the saliency of propositions (e.g. landmarks and causal links) to their actual explicability when the explanation is communicated to a human.
We present a Bayesian inference model to infer contrastive explanations (as LTL specifications) describing how two sets of plan traces differ.
{"src": "scitldr-AIC_train", "paper_id": "rkg2m6hXcE"}