Arrow Research search

Author name cluster

Kaile Su

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

36 papers
2 author rows

Possible papers

36

AAMAS Conference 2025 Conference Paper

Automatic Verification of Linear Integer Planning Programs via Forgetting in LIAUPF

  • Liangda Fang
  • Shikang Chen
  • Xiaoman Wang
  • Xiaoyou Lin
  • Chenyi Zhang
  • Qingliang Chen
  • Quanlong Guan
  • Kaile Su

The goal of generalized planning (GP) is to find a generalized solution for a class of planning problems. One of effective means to solve GP is to transform a GP problem into an abstract planning problem, which can be easily solved. Recently, Lin et al. proposed a novel abstract model for GP, namely generalized linear integer numeric planning (GLINP), whose solution is an algorithmic-like structure called a planning program. They also developed an inductive approach to generating planning programs for GLINP. However, it has no theoretical guarantee that the generated planning program holds for infinitely many problem instances. To address this defect, we propose an automatic approach to verify whether the planning program works for infinitely many problem instances in this paper. We translate the planning program into a set of trace axioms finitely represented by linear integer arithmetic with uninterpreted predicate and function symbols (LIAUPF), and reduce the problem to the entailment problem of LIAUPF. Due to the undecidability of entailment problem in LIAUPF, we identify a class of planning programs whose trace axioms can be simplified in linear integer arithmetic (LIA), that is, a decidable fragment of LIAUPF, when reasoning about only the input and output of planning programs. As a result, the correctness verification of this class of programs becomes decidable.

PDF

ICAPS Conference 2022 Conference Paper

Generalized Linear Integer Numeric Planning

  • Xiaoyou Lin
  • Qingliang Chen
  • Liangda Fang
  • Quanlong Guan
  • Weiqi Luo 0002
  • Kaile Su

Classical planning aims to find a sequence of actions that guarantees goal achievement from an initial state. The representative framework of classical planning is based on propositional logic. Due to the weak expressiveness of propositional logic, many applications of interest cannot be formalized as a classical planning problem. Some extensions such as numeric planning and generalized planning (GP) are therefore proposed. Qualitative numeric planning (QNP) is a decidable class of numeric and generalized extensions and serves as a numeric abstraction of GP. However, QNP is still far from being perfect and needs further improvement. In this paper, we introduce another generalized version of numeric planning, namely generalized linear integer numeric planning(GLINP), which is a more suitable abstract framework of GP than QNP. In addition, we develop a general framework to synthesize solutions to GLINP problems. Finally, we evaluate our approach on a number of benchmarks, and experimental results justify the effectiveness and scalability of our proposed approach.

Details

ICAPS Conference 2018 Conference Paper

Local Search for Flowshops with Setup Times and Blocking Constraints

  • Vahid Riahi
  • M. A. Hakim Newton
  • Kaile Su
  • Abdul Sattar 0001

Permutation flowshop scheduling problem (PFSP) is a classical combinatorial optimisation problem. There exist variants of PFSP to capture different realistic scenarios, but significant modelling gaps still remain with respect to real-world industrial applications such as the cider production line. In this paper, we propose a new PFSP variant that adequately models both overlapable sequence-dependent setup times (SDST) and mixed blocking constraints. We propose a computational model for makespan minimisation of the new PFSP variant and show that the time complexity is NP Hard. We then develop a constraint-guided local search algorithm that uses a new intensifying restart technique along with variable neighbourhood descent and greedy selection. The experimental study indicates that the proposed algorithm, on a set of wellknown benchmark instances, significantly outperforms the state-of-the-art search algorithms for PFSP.

Details

IJCAI Conference 2017 Conference Paper

A Reduction based Method for Coloring Very Large Graphs

  • Jinkun Lin
  • Shaowei Cai
  • Chuan Luo
  • Kaile Su

The graph coloring problem (GCP) is one of the most studied NP hard problems and has numerous applications. Despite the practical importance of GCP, there are limited works in solving GCP for very large graphs. This paper explores techniques for solving GCP on very large real world graphs. We first propose a reduction rule for GCP, which is based on a novel concept called degree bounded independent set. The rule is iteratively executed by interleaving between lower bound computation and graph reduction. Based on this rule, we develop a novel method called FastColor, which also exploits fast clique and coloring heuristics. We carry out experiments to compare our method FastColor with two best algorithms for coloring large graphs we could find. Experiments on a broad range of real world large graphs show the superiority of our method. Additionally, our method maintains both upper bound and lower bound on the optimal solution, and thus it proves an optimal solution when the upper bound meets the lower bound. In our experiments, it proves the optimal solution for 97 out of 142 instances.

PDF Details

IJCAI Conference 2017 Conference Paper

CCEHC: An Efficient Local Search Algorithm for Weighted Partial Maximum Satisfiability (Extended Abstract)

  • Chuan Luo
  • Shaowei Cai
  • Kaile Su
  • Wenxuan Huang

Weighted partial maximum satisfiability (WPMS) is a significant generalization of maximum satisfiability (MAX-SAT), with many important applications. Recently, breakthroughs have been made on stochastic local search (SLS) for weighted MAX-SAT and (unweighted) partial MAX-SAT (PMS). However, the performance of SLS for WPMS lags far behind. In this work, we present a new SLS algorithm named CCEHC for WPMS. CCEHC is mainly based on a heuristic emphasizing hard clauses, which has three components: a variable selection mechanism focusing on configuration checking based only on hard clauses, a weighting scheme for hard clauses, and a biased random walk component. Experiments show that CCEHC significantly outperforms its state-of-the-art SLS competitors. Experiments comparing CCEHC with a state-of-the-art complete solver indicate the effectiveness of CCEHC on a number of application WPMS instances.

PDF Details

IJCAI Conference 2017 Conference Paper

Restart and Random Walk in Local Search for Maximum Vertex Weight Cliques with Evaluations in Clustering Aggregation

  • Yi Fan
  • Nan Li
  • Chengqian Li
  • Zongjie Ma
  • Longin Jan Latecki
  • Kaile Su

The Maximum Vertex Weight Clique (MVWC) problem is NP-hard and also important in real-world applications. In this paper we propose to use the restart and the random walk strategies to improve local search for MVWC. If a solution is revisited in some particular situation, the search will restart. In addition, when the local search has no other options except dropping vertices, it will use random walk. Experimental results show that our solver outperforms state-of-the-art solvers in DIMACS and finds a new best-known solution. Also it is the unique solver which is comparable with state-of-the-art methods on both BHOSLIB and large crafted graphs. Furthermore we evaluated our solver in clustering aggregation. Experimental results on a number of real data sets demonstrate that our solver outperforms the state-of-the-art for solving the derived MVWC problem and helps improve the final clustering results.

PDF Details

IJCAI Conference 2016 Conference Paper

Reconfigurability in Reactive Multiagent Systems

  • Xiaowei Huang
  • Qingliang Chen
  • Jie Meng
  • Kaile Su

Reactive agents are suitable for representing physical resources in manufacturing control systems. An important challenge of agent-based manufacturing control systems is to develop formal and structured approaches to support their specification and verification. This paper proposes a logic-based approach, by generalising that of model checking multiagent systems, for the reconfigurability of reactive multiagent systems. Two reconfigurability scenarios are studied, for the resulting system being a monolithic system or an individual module, and their computational complexity results are given.

PDF Details

AAAI Conference 2016 Conference Paper

Strengthening Agents Strategic Ability with Communication

  • Xiaowei Huang
  • Qingliang Chen
  • Kaile Su

The current frameworks of reasoning about agents’ collective strategy are either too conservative or too liberal in terms of the sharing of local information between agents. In this paper, we argue that in many cases, a suitable amount of information is required to be communicated between agents to both enforce goals and keep privacy. Several communication operators are proposed to work with an epistemic strategy logic ATLK. The complexity of model checking resulting logics is studied, and surprisingly, we found that the additional expressiveness from the communication operators comes for free.

PDF Details

SAT Conference 2015 Conference Paper

CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability

  • Shaowei Cai 0001
  • Chuan Luo 0002
  • Kaile Su

Abstract This paper presents a stochastic local search (SLS) solver for SAT named CCAnr, which is based on the configuration checking strategy and has good performance on non-random SAT instances. CCAnr switches between two modes: it flips a variable according to the CCA (configuration checking with aspiration) heuristic if any; otherwise, it flips a variable in a random unsatisfied clause (which we refer to as the focused local search mode). The main novelty of CCAnr lies on the greedy heuristic in the focused local search mode, which contributes significantly to its good performance on structured instances. Previous two-mode SLS algorithms usually utilize diversifying heuristics such as age or randomized strategies to pick a variable from the unsatisfied clause. Our experiments on combinatorial and application benchmarks from SAT Competition 2014 show that CCAnr has better performance than other state-of-the-art SLS solvers on structured instances, and its performance can be further improved by using a preprocessor CP3. Our results suggest that a greedy heuristic in the focused local search mode might be helpful to improve SLS solvers for solving structured SAT instances.

Details

LORI Conference 2015 Conference Paper

Symbolic Model Checking for Dynamic Epistemic Logic

  • Johan van Benthem
  • Jan van Eijck
  • Malvin Gattinger
  • Kaile Su

Abstract Dynamic Epistemic Logic (DEL) can model complex information scenarios in a way that appeals to logicians. However, existing DEL implementations are ad-hoc, so we do not know how the framework really performs. For this purpose, we want to hook up with the best available model-checking and SAT techniques in computational logic. We do this by first providing a bridge: a new faithful representation of DEL models as so-called knowledge structures that allow for symbolic model checking. Next, we show that we can now solve well-known benchmark problems in epistemic scenarios much faster than with existing DEL methods. Finally, we show that our method is not just a matter of implementation, but that it raises significant issues about logical representation and update.

Details

IJCAI Conference 2015 Conference Paper

The Complexity of Model Checking Succinct Multiagent Systems

  • Xiaowei Huang
  • Qingliang Chen
  • Kaile Su

This paper studies the complexity of model checking multiagent systems, in particular systems succinctly described by two practical representations: concurrent representation and symbolic representation. The logics we concern include branching time temporal logics and several variants of alternating time temporal logics.

PDF Details

AAAI Conference 2015 Conference Paper

Two Weighting Local Search for Minimum Vertex Cover

  • Shaowei Cai
  • Jinkun Lin
  • Kaile Su

Minimum Vertex Cover (MinVC) is a well known NP-hard combinatorial optimization problem, and local search has been shown to be one of the most effective approaches to this problem. State-of-the-art MinVC local search algorithms employ edge weighting techniques and prefer to select vertices with higher weighted score. These algorithms are not robust and especially have poor performance on instances with structures which defeat greedy heuristics. In this paper, we propose a vertex weighting scheme to address this shortcoming, and combine it within the current best MinVC local search algorithm NuMVC, leading to a new algorithm called TwMVC. Our experiments show that TwMVC outperforms NuMVC on the standard benchmarks namely DIMACS and BHOSLIB. To the best of our knowledge, TwMVC is the first MinVC algorithm that attains the best known solution for all instances in both benchmarks. Further, TwMVC shows superiority on a benchmark of real-world networks.

PDF Details

AAAI Conference 2014 Conference Paper

Double Configuration Checking in Stochastic Local Search for Satisfiability

  • Chuan Luo
  • Shaowei Cai
  • Wei Wu
  • Kaile Su

Stochastic local search (SLS) algorithms have shown effectiveness on satisfiable instances of the Boolean satisfiability (SAT) problem. However, their performance is still unsatisfactory on random k-SAT at the phase transition, which is of significance and is one of the empirically hardest distributions of SAT instances. In this paper, we propose a new heuristic called DCCA, which combines two configuration checking (CC) strategies with different definitions of configuration in a novel way. We use the DCCA heuristic to design an efficient SLS solver for SAT dubbed DCCASat. The experiments show that the DCCASat solver significantly outperforms a number of state-of-the-art solvers on extensive random k-SAT benchmarks at the phase transition. Moreover, DCCASat shows good performance on structured benchmarks, and a combination of DCCASat with a complete solver achieves state-of-the-art performance on structured benchmarks.

PDF Details

AAAI Conference 2014 Conference Paper

Tailoring Local Search for Partial MaxSAT

  • Shaowei Cai
  • Chuan Luo
  • John Thornton
  • Kaile Su

Partial MaxSAT (PMS) is a generalization to SAT and MaxSAT. Many real world problems can be encoded into PMS in a more natural and compact way than SAT and MaxSAT. In this paper, we propose new ideas for local search for PMS, which mainly rely on the distinction between hard and soft clauses. We use these ideas to develop a local search PMS algorithm called Dist. Experimental results on PMS benchmarks from MaxSAT Evaluation 2013 show that Dist significantly outperforms state-of-the-art PMS algorithms, including both local search algorithms and complete ones, on random and crafted benchmarks. For the industrial benchmark, Dist dramatically outperforms previous local search algorithms and is comparable with complete algorithms.

PDF Details

LORI Conference 2013 Conference Paper

A Logic for Extensive Games with Short Sight

  • Chanjuan Liu 0001
  • Fenrong Liu
  • Kaile Su

Abstract To characterize the structures and reason about strategies of extensivegames, much work has been done to provide the logical systems for such games. These logic systems focus on various perspectives of extensive games: (Harrenstein et al. , 2003) concentrated on describing equilibrium concepts and strategic reasoning. (van Benthem, 2002) used dynamic logic to describe games as well as strategies.

Details

IJCAI Conference 2013 Conference Paper

Comprehensive Score: Towards Efficient Local Search for SAT with Long Clauses

  • Shaowei Cai
  • Kaile Su

It is widely acknowledged that stochastic local search (SLS) algorithms can efficiently find models of satisfiable formulae for the Boolean Satisfiability (SAT) problem. There has been much interest in studying SLS algorithms on random k-SAT instances. Compared to random 3-SAT instances which have special statistical properties rendering them easy to solve, random k-SAT instances with long clauses are similar to structured ones and remain very difficult. This paper is devoted to efficient SLS algorithms for random k-SAT instances with long clauses. By combining a novel variable property subscore with the commonly used property score, we design a scoring function named comprehensive score, which is utilized to develop a new SLS algorithm called CScoreSAT. The experiments show that CScoreSAT outperforms state-ofthe-art SLS solvers, including the winners of recent SAT competitions, by one to two orders of magnitudes on large random 5-SAT and 7-SAT instances. In addition, CScoreSAT significantly outperforms its competitors on random k-SAT instances for each k = 4, 5, 6, 7 from SAT Challenge 2012, which indicates its robustness.

PDF Details DOI

AAAI Conference 2013 Conference Paper

Improving WalkSAT for Random k-Satisfiability Problem with k > 3

  • Shaowei Cai
  • Kaile Su
  • Chuan Luo

Stochastic local search (SLS) algorithms are well known for their ability to efficiently find models of random instances of the Boolean satisfiablity (SAT) problem. One of the most famous SLS algorithms for SAT is WalkSAT, which is an initial algorithm that has wide influence among modern SLS algorithms. Recently, there has been increasing interest in WalkSAT, due to the discovery of its great power on large random 3-SAT instances. However, the performance of WalkSAT on random k-SAT instances with k > 3 lags far behind. Indeed, there have been few works in improving SLS algorithms for such instances. This work takes a large step towards this direction. We propose a novel concept namely multilevel make. Based on this concept, we design a scoring function called linear make, which is utilized to break ties in WalkSAT, leading to a new algorithm called WalkSATlm. Our experimental results on random 5- SAT and 7-SAT instances show that WalkSATlm improves WalkSAT by orders of magnitudes. Moreover, WalkSATlm significantly outperforms state-of-the-art SLS solvers on random 5-SAT instances, while competes well on random 7-SAT ones. Additionally, WalkSATlm performs very well on random instances from SAT Challenge 2012, indicating its robustness.

PDF Details

AAAI Conference 2012 Conference Paper

Configuration Checking with Aspiration in Local Search for SAT

  • Shaowei Cai
  • Kaile Su

An interesting strategy called configuration checking (CC) was recently proposed to handle the cycling problem in local search for Minimum Vertex Cover. A natural question is whether this CC strategy also works for SAT. The direct application of CC did not result in stochastic local search (SLS) algorithms that can compete with the current best SLS algorithms for SAT. In this paper, we propose a new heuristic based on CC for SLS algorithms for SAT, which is called configuration checking with aspiration (CCA). It is used to develop a new SLS algorithm called Swcca. The experiments on random 3-SAT instances show that Swcca significantly outperforms Sparrow2011, the winner of the random satisfiable category of the SAT Competition 2011, which is considered to be the best local search solver for random 3-SAT instances. Moreover, the experiments on structured instances show that Swcca is competitive with Sattime, the best local search solver for the crafted benchmark in the SAT Competition 2011.

PDF Details

ECAI Conference 2012 Conference Paper

Improving Local Search for Random 3-SAT Using Quantitative Configuration Checking

  • Chuan Luo 0002
  • Kaile Su
  • Shaowei Cai 0001

Configuration Checking (CC) was proposed as a new diversification strategy for Stochastic Local Search (SLS) algorithm for solving Minimum Vertex Cover, and has been successfully used for solving the Boolean Satisfiability problems, leading to an SLS algorithm called Swcc. However, the CC strategy for SAT is in the early stage of study, and Swcc cannot compete with the best SLS solvers for SAT in SAT Competition 2011. This paper presents a new strategy called Quantitative Configuration Checking (QCC), which is a quantitative version of the CC strategy for SAT. QCC is based on a new definition of "configuration" and works in a different way from the CC strategy does. Specifically, while previous CC strategies work only in the greedy mode, QCC firstly works in the random mode. We use QCC to improve the Swcc algorithm, resulting in a new SLS algorithm for SAT called Swqcc. Experimental results show that the QCC strategy is more effective than the CC strategy. Furthermore, Swqcc outperforms the best local search SAT solver in SAT Competition 2011 called Sparrow2011 on random 3-SAT instances.

Details

AAAI Conference 2012 Conference Paper

Probabilistic Alternating-Time Temporal Logic of Incomplete Information and Synchronous Perfect Recall

  • Xiaowei Huang
  • Kaile Su
  • Chenyi Zhang

A probabilistic variant of ATL∗ logic is proposed to work with multi-player games of incomplete information and synchronous perfect recall. The semantics of the logic is settled over probabilistic interpreted system and partially observed probabilistic concurrent game structure. While unexpectedly, the model checking problem is in general undecidable even for singlegroup fragment, we find a fragment whose complexity is in 2-EXPTIME. The usefulness of this fragment is shown over a land search scenario.

PDF Details

AAAI Conference 2012 Conference Paper

Two New Local Search Strategies for Minimum Vertex Cover

  • Shaowei Cai
  • Kaile Su
  • Abdul Sattar

In this paper, we propose two new strategies to design efficient local search algorithms for the minimum vertex cover (MVC) problem. There are two main drawbacks in state-ofthe-art MVC local search algorithms: First, they select a pair of vertices to be exchanged simultaneously, which is time consuming; Second, although they use edge weighting techniques, they do not have a strategy to decrease the weights. To address these drawbacks, we propose two new strategies: two stage exchange and edge weighting with forgetting. The two stage exchange strategy selects two vertices to be exchanged separately and performs the exchange in two stages. The strategy of edge weighting with forgetting not only increases weights of uncovered edges, but also decreases some weights for each edge periodically. We utilize these two strategies to design a new algorithm dubbed NuMVC. The experimental results show that NuMVC significantly outperforms existing state-of-the-art heuristic algorithms on most of the hard DIMACS instances and all instances in the hard random BHOSLIB benchmark.

PDF Details

IJCAI Conference 2011 Conference Paper

Large Hinge Width on Sparse Random Hypergraphs

  • Tian Liu
  • Xiaxiang Lin
  • Chaoyi Wang
  • Kaile Su
  • Ke Xu

Consider random hypergraphs on n vertices, where each k-element subset of vertices is selected with probability p independently and randomly as a hyperedge. By sparse we mean that the total number of hyperedges is O(n) or O(n ln n). When k = 2, these are exactly the classical Erdö s-Ré nyi random graphs G(n, p). We prove that with high probability, hinge width on these sparse random hypergraphs can grow linearly with the expected number of hyperedges. Some random constraint satisfaction problems such as Model RB and Model RD have satisfiability thresholds on these sparse constraint hypergraphs, thus the large hinge width results provide some theoretical evidence for random instances around satisfiability thresholds to be hard for a standard hinge-decomposition based algorithm. We also conduct experiments on these and other kinds of random graphs with several hundreds vertices, including regular random graphs and power law random graphs. The experimental results also show that hinge width can grow linearly with the number of edges on these different random graphs. These results may be of further interests.

PDF Details DOI

AAAI Conference 2010 Conference Paper

EWLS: A New Local Search for Minimum Vertex Cover

  • Shaowei Cai
  • Kaile Su
  • Qingliang Chen

A number of algorithms have been proposed for the Minimum Vertex Cover problem. However, they are far from satisfactory, especially on hard instances. In this paper, we introduce Edge Weighting Local Search (EWLS), a new local search algorithm for the Minimum Vertex Cover problem. EWLS is based on the idea of extending a partial vertex cover into a vertex cover. A key point of EWLS is to find a vertex set that provides a tight upper bound on the size of the minimum vertex cover. To this purpose, EWLS employs an iterated local search procedure, using an edge weighting scheme which updates edge weights when stuck in local optima. Moreover, some sophisticated search strategies have been taken to improve the quality of local optima. Experimental results on the broadly used DIMACS benchmark show that EWLS is competitive with the current best heuristic algorithms, and outperforms them on hard instances. Furthermore, on a suite of difficult benchmarks, EWLS delivers the best results and sets a new record on the largest instance.

PDF Details

AAAI Conference 2008 Conference Paper

An Extended Interpreted System Model for Epistemic Logics

  • Kaile Su

The interpreted system model offers a computationally grounded model, in terms of the states of computer processes, to S5 epistemic logics. This paper extends the interpreted system model, and provides a computationally grounded one, called the interpreted perception system model, to those epistemic logics other than S5. It is usually assumed, in the interpreted system model, that those parts of the environment that are visible to an agent are correctly perceived by the agent as a whole. The essential idea of the interpreted perception system model is that an agent may have incorrect perception or observations to the visible parts of the environment and the agent may not be aware of this. The notion of knowledge can be defined so that an agent knows a statement iff the statement holds in those states that the agent can not distinguish (from the current state) by using only her correct observations. We establish a logic of knowledge and certainty, called KC logic, with a sound and complete proof system. The knowledge modality in this logic is S4 valid. It becomes S5 if we assume an agent always has correct observations; and more interestingly, it can be S4. 2 or S4. 3 under other natural constraints on agents and their sensors to the environment.

PDF Details

IJCAI Conference 2007 Conference Paper

  • Han Lin
  • Kaile Su

In this paper we present a general logical framework for (weighted) MAX-SAT problem, and study properties of inference rules for branch and bound MAX-SAT solver. Several new rules, which are not equivalent but $\Lambda$-equivalent, are proposed, and we show that $\Lambda$-equivalent rules are also sound. As an example, we show how to exploit inference rules to achieve a new lower bound function for a MAX-2-SAT solver. Our new function is admissible and consistently better than the well-known lower bound function. Based on the study of inference rules, we implement an efficient solver and the experimental results demonstrate that our solver outperforms the most efficient solver that has been implemented very recently[Heras and Larrosa, 2006], especially for large instances.

PDF Details

AAAI Conference 2005 Conference Paper

Observation-based Model for BDI-Agents

  • Kaile Su
  • Kewen Wang

We present a new computational model of BDI-agents, called the observation-based BDI-model. The key point of this BDImodel is to express agents’ beliefs, desires and intentions as a set of runs (computing paths), which is exactly a system in the interpreted system model, a well-known agent model due to Halpern and his colleagues. Our BDI-model is computationally grounded in that we are able to associate the BDIagent model with a computer program, and formulas, involving agents’ beliefs, desires (goals) and intentions, can be understood as properties of program computations. We present a sound and complete proof system with respect to our BDImodel and explore how symbolic model checking techniques can be applied to model checking BDI-agents. In order to make our BDI-model more flexible and practically realistic, we generalize it so that agents can have multiple sources of beliefs, goals and intentions.

PDF Details

AAAI Conference 2004 Conference Paper

Model Checking Temporal Logics of Knowledge in Distributed Systems

  • Kaile Su

Model checking is a promising approach to automatic verification, which has concentrated on specification expressed in temporal logic. Comparatively little attention has been given to temporal logics of knowledge, although such logics have been proven to be very useful in the specifications of protocols for distributed systems. In this paper, we address ourselves to the model checking problem for a temporal logic of knowledge (Halpern and Vardi’s logic of CKLn). Based on the semantics of interpreted systems with local propositions, we develop an approach to symbolic CKLn model checking via OBDDs. In our approach to model checking specifications involving agents’ knowledge, the knowledge modalities are eliminated via quantifiers over agents’ non-observable variables.

PDF Details

KR Conference 2004 Conference Paper

Reasoning about Knowledge by Variable Forgetting

  • Guanfeng Lv
  • Kaile Su
  • Yan Zhang

In this paper, we investigate knowledge reasoning within a simple framework called knowledge structure. We use variable forgetting as a basic operation for one agent to reason about its own or other agents’ knowledge. In our framework, two notions namely agents’ observable variables and the weakest sufficient condition play important roles in knowledge reasoning. Given a background knowledge base and a set of observable variables for an agent, we show that the notion of agent knowing a formula can be defined as a weakest sufficient condition of the formula on the set of observable variables for the agent under background knowledge base. Moreover, we show how to capture the notion of common knowledge by using a generalized notion of weakest sufficient condition. We also discuss possible applications of our framework in some interesting domains such as the automated analysis of the well-known muddy children puzzle and the verification of the revised Needham-Schroeder protocol.