Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic

• URL: http://arxiv.org/abs/2307.05067v1
• Date: Tue, 11 Jul 2023 07:13:09 GMT
• Title: Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic
• Authors: Daniel Miedema (Bernoulli Institute, University of Groningen), Malvin Gattinger (ILLC, University of Amsterdam)
• Abstract summary: We use ZDDs to symbolically encode Kripke models used in Dynamic Epistemic Logic. We show that replacing BDDs with the right variant of ZDDs can significantly reduce memory usage. This suggests that ZDDs are a useful tool for model checking multi-agent systems.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Binary decision diagrams (BDDs) are widely used to mitigate the state-explosion problem in model checking. A variation of BDDs are Zero-suppressed Decision Diagrams (ZDDs) which omit variables that must be false, instead of omitting variables that do not matter. We use ZDDs to symbolically encode Kripke models used in Dynamic Epistemic Logic, a framework to reason about knowledge and information dynamics in multi-agent systems. We compare the memory usage of different ZDD variants for three well-known examples from the literature: the Muddy Children, the Sum and Product puzzle and the Dining Cryptographers. Our implementation is based on the existing model checker SMCDEL and the CUDD library. Our results show that replacing BDDs with the right variant of ZDDs can significantly reduce memory usage. This suggests that ZDDs are a useful tool for model checking multi-agent systems.

Related papers

• Breaking Determinism: Fuzzy Modeling of Sequential Recommendation Using Discrete State Space Diffusion Model [66.91323540178739]
  Sequential recommendation (SR) aims to predict items that users may be interested in based on their historical behavior. We revisit SR from a novel information-theoretic perspective and find that sequential modeling methods fail to adequately capture randomness and unpredictability of user behavior. Inspired by fuzzy information processing theory, this paper introduces the fuzzy sets of interaction sequences to overcome the limitations and better capture the evolution of users' real interests.
  arXiv  Detail & Related papers  (2024-10-31T14:52:01Z)
• ZeroDDI: A Zero-Shot Drug-Drug Interaction Event Prediction Method with Semantic Enhanced Learning and Dual-Modal Uniform Alignment [11.290096354280111]
  Previously unobserved/unseen DDIEs have been emerging, posing a new classification task when unseen classes have no labelled instances in the training stage. Existing computational methods are not directly applicable to ZS-DDIE, which has two primary challenges: obtaining suitable DDIE representations and handling the class imbalance issue. We propose a novel method named ZeroDDI for the ZS-DDIE task, which emphasizes the key biological semantics and distills discriminative molecular substructure-related semantics for DDIE representation learning.
  arXiv  Detail & Related papers  (2024-07-01T01:28:14Z)
• Long-Tailed Anomaly Detection with Learnable Class Names [64.79139468331807]
  We introduce several datasets with different levels of class imbalance and metrics for performance evaluation. We then propose a novel method, LTAD, to detect defects from multiple and long-tailed classes, without relying on dataset class names. LTAD substantially outperforms the state-of-the-art methods for most forms of dataset imbalance.
  arXiv  Detail & Related papers  (2024-03-29T15:26:44Z)
• Variants of Tagged Sentential Decision Diagrams [6.891570850234007]
  A recently proposed canonical form of Boolean functions, namely tagged sentential decision diagrams (TSDDs), exploits both the standard and zero-suppressed trimming rules. In this paper, we present a variant of TSDDs which we call standard TSDDs (STSDDs) by reversing the order of trimming rules. We then prove the canonicity of STSDDs and present the algorithms for binary operations on TSDDs.
  arXiv  Detail & Related papers  (2023-11-16T12:29:25Z)
• Interpretability at Scale: Identifying Causal Mechanisms in Alpaca [62.65877150123775]
  We use Boundless DAS to efficiently search for interpretable causal structure in large language models while they follow instructions. Our findings mark a first step toward faithfully understanding the inner-workings of our ever-growing and most widely deployed language models.
  arXiv  Detail & Related papers  (2023-05-15T17:15:40Z)
• Optimizing Binary Decision Diagrams with MaxSAT for classification [3.2894524838755608]
  A growing interest in explainable artificial intelligence motivates the need for interpretable machine learning (ML) models. Recently, several exact methods for computing such models are proposed to overcome weaknesses of traditional methods. In this paper, we first propose SAT-based models for learning optimal Binary decision diagrams (BDDs) Then, we lift the encoding to a MaxSAT model to learn optimal BDDs in limited depths. Finally, we tackle the fragmentation problem by introducing a method to merge compatible subtrees for the BDDs found via the MaxSAT model.
  arXiv  Detail & Related papers  (2022-03-21T23:17:37Z)
• Belief Revision in Sentential Decision Diagrams [126.94029917018733]
  We develop a general revision algorithm for SDDs based on a syntactic characterisation of Dalal revision. Preliminary experiments performed with randomly generated knowledge bases show the advantages of directly perform revision within SDD formalism.
  arXiv  Detail & Related papers  (2022-01-20T11:01:41Z)
• Discriminative-Generative Dual Memory Video Anomaly Detection [81.09977516403411]
  Recently, people tried to use a few anomalies for video anomaly detection (VAD) instead of only normal data during the training process. We propose a DiscRiminative-gEnerative duAl Memory (DREAM) anomaly detection model to take advantage of a few anomalies and solve data imbalance.
  arXiv  Detail & Related papers  (2021-04-29T15:49:01Z)
• Variable Shift SDD: A More Succinct Sentential Decision Diagram [10.91026094237478]
  Sentential Decision Diagram (SDD) is a tractable representation of Boolean functions. We propose a more succinct variant of SDD named Variable Shift SDD (VS-SDD) We show that VS-SDDs are never larger than SDDs and there are cases in which the size of a VS-SDD is exponentially smaller than that of an SDD.
  arXiv  Detail & Related papers  (2020-04-06T09:18:19Z)
• Ordered Functional Decision Diagrams: A Functional Semantics For Binary Decision Diagrams [0.0]
  We introduce a novel framework, termed $lambda$DD, that revisits Binary Decision Diagrams from a purely functional point of view. We enumerate, in a principled way, all the models of this class and isolate its most expressive model.
  arXiv  Detail & Related papers  (2020-03-20T15:46:48Z)
• Simple and Effective Prevention of Mode Collapse in Deep One-Class Classification [93.2334223970488]
  We propose two regularizers to prevent hypersphere collapse in deep SVDD. The first regularizer is based on injecting random noise via the standard cross-entropy loss. The second regularizer penalizes the minibatch variance when it becomes too small.
  arXiv  Detail & Related papers  (2020-01-24T03:44:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.