On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach

• URL: http://arxiv.org/abs/2003.06492v3
• Date: Fri, 3 Jul 2020 13:44:36 GMT
• Title: On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach
• Authors: Renyan Feng, Erman Acar, Stefan Schlobach, Yisong Wang, Wanwei Liu
• Abstract summary: We introduce a forgetting-based approach in Computation Tree Logic (CTL) We show that it can be used to compute the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a property under a given model and over a given signature. We also study its theoretical properties and show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting.
• Score: 3.9461038686072847
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Computation Tree Logic (CTL) is one of the central formalisms in formal verification. As a specification language, it is used to express a property that the system at hand is expected to satisfy. From both the verification and the system design points of view, some information content of such property might become irrelevant for the system due to various reasons, e.g., it might become obsolete by time, or perhaps infeasible due to practical difficulties. Then, the problem arises on how to subtract such piece of information without altering the relevant system behaviour or violating the existing specifications over a given signature. Moreover, in such a scenario, two crucial notions are informative: the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a given property. To address such a scenario in a principled way, we introduce a forgetting-based approach in CTL and show that it can be used to compute SNC and WSC of a property under a given model and over a given signature. We study its theoretical properties and also show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting. Furthermore, we analyse the computational complexity of some basic reasoning tasks for the fragment CTL_AF in particular.

Related papers

• The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
  Tokenization is a critical step in the NLP pipeline. Despite its recognized importance as a standard representation method in NLP, the theoretical underpinnings of tokenization are not yet fully understood. The present paper contributes to addressing this theoretical gap by proposing a unified formal framework for representing and analyzing tokenizer models.
  arXiv  Detail & Related papers  (2024-07-16T11:12:28Z)
• Identifiable Causal Representation Learning: Unsupervised, Multi-View, and Multi-Environment [10.814585613336778]
  Causal representation learning aims to combine the core strengths of machine learning and causality. This thesis investigates what is possible for CRL without direct supervision, and thus contributes to its theoretical foundations.
  arXiv  Detail & Related papers  (2024-06-19T09:14:40Z)
• Retrieval-Augmented Mining of Temporal Logic Specifications from Data [0.46040036610482665]
  This work addresses the task of learning STL requirements from observed behaviors in a data-driven manner. We present a novel framework that combines Bayesian Optimization (BO) and Information Retrieval (IR) techniques to simultaneously learn both the structure and the parameters of STL formulae.
  arXiv  Detail & Related papers  (2024-05-23T09:29:00Z)
• Neuro-Symbolic Causal Reasoning Meets Signaling Game for Emergent Semantic Communications [71.63189900803623]
  A novel emergent SC system framework is proposed and is composed of a signaling game for emergent language design and a neuro-symbolic (NeSy) artificial intelligence (AI) approach for causal reasoning. The ESC system is designed to enhance the novel metrics of semantic information, reliability, distortion and similarity.
  arXiv  Detail & Related papers  (2022-10-21T15:33:37Z)
• On the Complexity of Rational Verification [5.230352342979224]
  Rational verification refers to the problem of checking which temporal logic properties hold of a concurrent multiagent system. We show that the complexity of rational verification can be greatly reduced by specifications. We provide improved results for rational verification when considering players' goals given by mean-payoff utility functions.
  arXiv  Detail & Related papers  (2022-07-06T12:56:22Z)
• Efficient Knowledge Compilation Beyond Weighted Model Counting [7.828647825246474]
  We introduce Second Level Algebraic Model Counting (2AMC) as a generic framework for these kinds of problems. First level techniques based on Knowledge Compilation (KC) have been adapted for specific 2AMC instances by imposing variable order constraints. We show that we can exploit the logical structure of a 2AMC problem to omit parts of these constraints, thus limiting the negative effect.
  arXiv  Detail & Related papers  (2022-05-16T08:10:40Z)
• The Causal Neural Connection: Expressiveness, Learnability, and Inference [125.57815987218756]
  An object called structural causal model (SCM) represents a collection of mechanisms and sources of random variation of the system under investigation. In this paper, we show that the causal hierarchy theorem (Thm. 1, Bareinboim et al., 2020) still holds for neural models. We introduce a special type of SCM called a neural causal model (NCM), and formalize a new type of inductive bias to encode structural constraints necessary for performing causal inferences.
  arXiv  Detail & Related papers  (2021-07-02T01:55:18Z)
• Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming [8.677108656718824]
  Event Calculus (EC) is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains. We show how EC scenarios can be naturally and directly encoded in s(CASP) and how it enables deductive and abductive reasoning tasks.
  arXiv  Detail & Related papers  (2021-06-28T10:43:25Z)
• Structural Causal Models Are (Solvable by) Credal Networks [70.45873402967297]
  Causal inferences can be obtained by standard algorithms for the updating of credal nets. This contribution should be regarded as a systematic approach to represent structural causal models by credal networks. Experiments show that approximate algorithms for credal networks can immediately be used to do causal inference in real-size problems.
  arXiv  Detail & Related papers  (2020-08-02T11:19:36Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  We present a novel approach to formulate different notions of causal reasoning, over binary acyclic models, as optimization problems. We show that both notions are efficiently automated. Using models with more than $8000$ variables, checking is computed in a matter of seconds, with MaxSAT outperforming ILP in many cases.
  arXiv  Detail & Related papers  (2020-06-05T10:56:52Z)
• CSNE: Conditional Signed Network Embedding [77.54225346953069]
  Signed networks encode positive and negative relations between entities such as friend/foe or trust/distrust. Existing embedding methods for sign prediction generally enforce different notions of status or balance theories in their optimization function. We introduce conditional signed network embedding (CSNE) Our probabilistic approach models structural information about the signs in the network separately from fine-grained detail.
  arXiv  Detail & Related papers  (2020-05-19T19:14:52Z)

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.