In social recommenders, the inherent nonlinearity and opacity of synergistic effects across multiple social networks hinders users from understanding how diverse information is leveraged for recommendations, consequently diminishing explainability. However, existing explainers can only identify the topological information in social networks that significantly influences recommendations, failing to further explain the synergistic effects among this information. Inspired by existing findings that synergistic effects enhance mutual information between inputs and predictions to generate information gain, we extend this discovery to graph data. We quantify graph information gain to identify subgraphs embodying synergistic effects. Based on the theoretical insights, we propose SemExplainer, which explains synergistic effects by identifying subgraphs that embody them. SemExplainer first extracts explanatory subgraphs from multi-view social networks to generate preliminary importance explanations for recommendations. A conditional entropy optimization strategy to maximize information gain is developed, thereby further identifying subgraphs that embody synergistic effects from explanatory subgraphs. Finally, SemExplainer searches for paths from users to recommended items within the synergistic subgraphs to generate explanations for the recommendations. Extensive experiments on three datasets demonstrate the superiority of SemExplainer over baseline methods, providing superior explanations of synergistic effects. The implementation is available at https://github.com/yushuowiki/SemExplainer.

Comprehensible neural network explanations are foundations for a better understanding of decisions, especially when the input data are infused with malicious perturbations. Existing solutions generally mitigate the impact of perturbations through adversarial training, yet they fail to generate comprehensible explanations under unknown perturbations. To address this challenge, we propose AGAIN, a factor graph-based interpretable neural network, which is capable of generating comprehensible explanations under unknown perturbations. Instead of retraining like previous solutions, the proposed AGAIN directly integrates logical rules by which logical errors in explanations are identified and rectified during inference. Specifically, we construct the factor graph to express logical rules between explanations and categories. By treating logical rules as exogenous knowledge, AGAIN can identify incomprehensible explanations that violate real-world logic. Furthermore, we propose an interactive intervention switch strategy rectifying explanations based on the logical guidance from the factor graph without learning perturbations, which overcomes the inherent limitation of adversarial training-based methods in defending only against known perturbations. Additionally, we theoretically demonstrate the effectiveness of employing factor graph by proving that the comprehensibility of explanations is strongly correlated with factor graph. Extensive experiments are conducted on three datasets and experimental results illustrate the superior performance of AGAIN compared to state-of-the-art baselines.

The real-time interaction between embedded software and its external environment is conducted through the interrupt mechanism. Since the interrupt request is random and responds according to priority, the execution of embedded software is non-sequential, which leads to the non-deterministic software behaviors. If these non-deterministic behaviors can be quantitatively pre-analyzed during the software design phase, the reliability of embedded software can be improved effectively. In this paper, we first provide an embedded software behavior model based on extended deterministic and stochastic Petri nets (EDSPN). Through EDSPN, the interrupt behavior of embedded software can be effectively modeled. Then we put forward a probabilistic model checking method of Continuous Stochastic Logic (CSL) for EDSPN to analyze embedded software behavior. For alleviating the state explosion problem, the above method uses the bounded model checking (BMC) technique. We present the model checking methods and the probability metric calculation methods for CSL operators under bounded semantics. Finally, by analyzing the EDSPN model of embedded software with multiple interrupts, we compare the analytical capabilities of BMC method and non-BMC method. The experiment shows that when the state space of EDSPN is large and is hard to calculate, the bounded checking algorithm can be used to approximate the software behavior. The conclusions obtained are helpful to understand the properties to be verified.