Model checking is a promising technology, which has been applied for verification of many hardware and software systems. In this paper, we introduce the concept of model update towards the development of an automatic system modification tool that extends model checking functions. We define primitive update operations on the models of Computation Tree Logic (CTL) and formalize the principle of minimal change for CTL model update. These primitive update operations, together with the underlying minimal change principle, serve as the foundation for CTL model update. Essential semantic and computational characterizations are provided for our CTL model update approach. We then describe a formal algorithm that implements this approach. We also illustrate two case studies of CTL model updates for the well-known microwave oven example and the Andrew File System 1, from which we further propose a method to optimize the update results in complex system modifications.

Goal recognition is the task of inferring users’ goals from sequences of observed actions. By enabling player-adaptive digital games to dynamically adjust their behavior in concert with players’ changing goals, goal recognition can inform adaptive decision making for a broad range of entertainment, training, and education applications. This paper presents a goal recognition framework based on Markov logic networks (MLN). The model’s parameters are directly learned from a corpus of actions that was collected through player interactions with a non-linear educational game. An empirical evaluation demonstrates that the MLN goal recognition framework accurately predicts players’ goals in a game environment with multiple solution paths.

We study the performance of different message passing algorithms in the two dimensional Edwards Anderson model. We show that the standard Belief Propagation (BP) algorithm converges only at high temperature to a paramagnetic solution. Then, we test a Generalized Belief Propagation (GBP) algorithm, derived from a Cluster Variational Method (CVM) at the plaquette level. We compare its performance with BP and with other algorithms derived under the same approximation: Double Loop (DL) and a two-ways message passing algorithm (HAK). The plaquette-CVM approximation improves BP in at least three ways: the quality of the paramagnetic solution at high temperatures, a better estimate (lower) for the critical temperature, and the fact that the GBP message passing algorithm converges also to non paramagnetic solutions. The lack of convergence of the standard GBP message passing algorithm at low temperatures seems to be related to the implementation details and not to the appearance of long range order. In fact, we prove that a gauge invariance of the constrained CVM free energy can be exploited to derive a new message passing algorithm which converges at even lower temperatures. In all its region of convergence this new algorithm is faster than HAK and DL by some orders of magnitude.

Standard belief change assumes an underlying logic containing full classical propositional logic. However, there are good reasons for considering belief change in less expressive logics as well. In this paper we build on recent investigations by Delgrande on contraction for Horn logic. We show that the standard basic form of contraction, partial meet, is too strong in the Horn case. This result stands in contrast to Delgrandes conjecture that orderly maxichoice is the appropriate form of contraction for Horn logic. We then define a more appropriate notion of basic contraction for the Horn case, influenced by the convexity property holding for full propositional logic and which we refer to as infra contraction. The main contribution of this work is a result which shows that the construction method for Horn contraction for belief sets based on our infra remainder sets corresponds exactly to Hanssons classical kernel contraction for belief sets, when restricted to Horn logic. This result is obtained via a detour through contraction for belief bases. We prove that kernel contraction for belief bases produces precisely the same results as the belief base version of infra contraction. The use of belief bases to obtain this result provides evidence for the conjecture that Horn belief change is best viewed as a 'hybrid' version of belief set change and belief base change. One of the consequences of the link with base contraction is the provision of a representation result for Horn contraction for belief sets in which a version of the Core-retainment postulate features.

This paper extends the framework of partially observable Markov decision processes (POMDPs) to multi-agent settings by incorporating the notion of agent models into the state space. Agents maintain beliefs over physical states of the environment and over models of other agents, and they use Bayesian updates to maintain their beliefs over time. The solutions map belief states to actions. Models of other agents may include their belief states and are related to agent types considered in games of incomplete information. We express the agents autonomy by postulating that their models are not directly manipulable or observable by other agents. We show that important properties of POMDPs, such as convergence of value iteration, the rate of convergence, and piece-wise linearity and convexity of the value functions carry over to our framework. Our approach complements a more traditional approach to interactive settings which uses Nash equilibria as a solution paradigm. We seek to avoid some of the drawbacks of equilibria which may be non-unique and do not capture off-equilibrium behaviors. We do so at the cost of having to represent, process and continuously revise models of other agents. Since the agents beliefs may be arbitrarily nested, the optimal solutions to decision making problems are only asymptotically computable. However, approximate belief updates and approximately optimal plans are computable. We illustrate our framework using a simple application domain, and we show examples of belief updates and value functions.

We analyze the patterns of autistic reasoning while performing planning tasks. The formalism of non-monotonic logic of defaults is used to simulate the autistic decision-making while adjusting an action to a context. Our current main finding is that while people with autism may be able to process single default rules, they have a characteristic difficulty in cases where multiple default rules conflict. Even though default reasoning was intended to simulate the reasoning of typical human subjects, it turns out that following the operational semantics of default reasoning in a literal way leads to the peculiarities of autistic behavior observed in the literature.

We consider the general problem of finding the minimum weight $\bm$-matching on arbitrary graphs. We prove that, whenever the linear programming (LP) relaxation of the problem has no fractional solutions, then the belief propagation (BP) algorithm converges to the correct solution. We also show that when the LP relaxation has a fractional solution then the BP algorithm can be used to solve the LP relaxation. Our proof is based on the notion of graph covers and extends the analysis of (Bayati-Shah-Sharma 2005 and Huang-Jebara 2007}. These results are notable in the following regards: (1) It is one of a very small number of proofs showing correctness of BP without any constraint on the graph structure. (2) Variants of the proof work for both synchronous and asynchronous BP; it is the first proof of convergence and correctness of an asynchronous BP algorithm for a combinatorial optimization problem.

This work proposes new approaches to contingent planning using alternative belief state representations extended from those in conformant planning and a new AND/OR forward search algorithm, called PrAO, for contingent solutions. Each representation was implemented in a new contingent planner. The important role of belief state representation has been confirmed by the fact that our planners all outperform other stateof- the-art planners on most benchmarks and the comparison of their performances varies across all the benchmarks even using the same search algorithm PrAO and same unsophisticated heuristic scheme. The work identifies the properties of each representation method that affect the performance.

Model-based diagnosis (MBD) uses an abstraction of system to diagnose possible faulty functions of an underlying system. To improve the solution efficiency for multi-fault diagnosis problems, especially for large scale systems, this paper proposes a method to induce reasonable diagnosis solutions, under coarse diagnosis, by using the relationships between system outputs and components. Compared to existing diagnosis methods, the proposed framework only needs to consider associations between outputs and components by using an assumption-based truth maintenance system (ATMS) [de Kleer 1986] to obtain correlation components for every output node. As a result, our method significantly reduces the number of variables required for model diagnosis, which makes it suitable for large scale circuit systems.

This paper compares in depth the effectiveness of two conjunctive belief state representations in contingent planning: prime implicates and minimal CNF, a compact form of CNF formulae, which were initially proposed in conformant planning research (To et al. 2010a; 2010b). Similar to the development of the contingent planner CNFct for minimal CNF (To et al. 2011b), the present paper extends the progression function for the prime implicate representation in (To et al. 2010b) for computing successor belief states in the presence of incomplete information to handle non-deterministic and sensing actions required in contingent planning. The idea was instantiated in a new contingent planner, called PIct, using the same AND/OR search algorithm and heuristic function as those for CNFct. The experiments show that, like CNFct, PIct performs very well in a wide range of benchmarks. The study investigates the advantages and disadvantages of the two planners and identifies the properties of each representation method that affect the performance.