Partial information decompositions (PIDs), which quantify information interactions between three or more variables in terms of uniqueness, redundancy and synergy, are gaining traction in many application domains. However, our understanding of the operational interpretations of PIDs is still incomplete for many popular PID definitions. In this paper, we discuss the operational interpretations of unique information through the lens of two well-known PID definitions. We reexamine an interpretation from statistical decision theory showing how unique information upper bounds the risk in a decision problem. We then explore a new connection between the two PIDs, which allows us to develop an informal but appealing interpretation, and generalize the PID definitions using a common Lagrangian formulation. Finally, we provide a new PID definition that is able to capture the information that is unique. We also show that it has a straightforward interpretation and examine its properties.The full version of this paper is available online [1].

Linear Temporal Logic (LTL) is arguably the most popular specification language for formal verification of safety-critical systems. However, LTL formulas can be unintuitive and error- prone for human practitioners to specify and validate. Meanwhile, drawing timelines remains one of the most popular methods for specifying and validating requirements for indus-trial system designs, such as in aerospace operational concepts. Therefore, we provide a new timeline tool for visualizing LTL specifications as timelines, providing provably-correct, intuitive equivalents between these two specification formats. Our tool generates timeline visualizations by translating LTL formulas to intermediate representations as Buchi automata and then regular expressions, and finally simplifying and visualizing the expressions. We provide an algorithm for this visualization, a theoretical soundness analysis” and an implementation.