Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Statistical relational models combine aspects of first-order logic and probabilistic graphical models, enabling them to model complex logical and probabilistic interactions between large numbers of objects. This level of expressivity comes at the cost of increased complexity of inference, motivating a new line of research in lifted probabilistic inference. By exploiting symmetries of the relational structure in the model, and reasoning about groups of objects as a whole, lifted algorithms dramatically improve the run time of inference and learning.The thesis has five main contributions. First, we propose a new method for logical inference, calledfirst-order knowledge compilation. We show that by compiling relational models into a new circuit language, hard inference problems become tractable to solve. Furthermore, we present an algorithm that compiles relational models into our circuit language. Second, we show how to use first-order knowledge compilation for statistical relational models, leading to a new state-of-the-art lifted probabilistic inference algorithm. Third, we develop a formal framework for exact lifted inference, including a definition in terms of its complexity w.r.t. the number of objects in the world. From this follows a first completeness result, showing that the two-variable class of statistical relational models always supports lifted inference. Fourth, we present an algorithm for approximate lifted inference by performing exact lifted inference in a relaxed, approximate model. Statistical relational models are receiving a lot of attention today because of their expressive power for learning. Fifth, we propose to harness the full power of relational representations for that task, by using lifted parameter learning. The techniques presented in this thesis are evaluated empirically on statistical relational models of thousands of interacting objects and millions of random variables.

681.3 <043> --- academic collection --- Computerwetenschap--Dissertaties --- Theses

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

681.3 <043> --- academic collection --- Computerwetenschap--Dissertaties --- Theses

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

One of the main advantages of logic programs is that it allows to write declarative programs that very understandable. However, such a declarati ve program can be a very inefficient or even a non-terminating specifica tion of a problem. Therefore, one of the main concerns in program verifi cation of a logic proram, is proving that it terminates. If such a proof fails, non-termination analysis identifies the loop in the program. In this PhD, we prove non-termination based on symbolic derivation trees . These symbolic trees show (a part of) the derivations of all queries i n a certain class of queries. We implemented these symbolic trees and in troduced a new non-termination condition based on these trees. In the remainder of the PhD, these trees will be extended to use non-fai lure information. This allows to prove non-termination of more classes o f programs. Furthermore, we will investigate which non-logical features of Prolog can be incorporated in order to analyse more realistic Prolog programs.

681.3 <043> --- academic collection --- Computerwetenschap--Dissertaties --- Theses

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Representing, learning, and reasoning about knowledge are central to artificial intelligence (AI). A long standing goal of AI is unifying logic and probability, to benefit from the strengths of both formalisms. Probability theory allows us to represent and reason in uncertain domains, while first-order logic allows us to represent and reason about structured, relational domains. Many real-world problems exhibit both uncertainty and structure, and thus can be more naturally represented with a combination of probabilistic and logical knowledge. This observation has led to the development of probabilistic logical models (PLMs), which combine probabilistic models with elements of first-order logic, to succinctly capture uncertainty in structured, relational domains, e.g., social networks, citation graphs, etc. While PLMs provide expressive representation formalisms, efficient inference is still a major challenge in these models, as they typically involve a large number of objects and interactions among them. Among the various efforts to address this problem, a promising line of work is lifted probabilistic inference. Lifting attempts to improve the efficiency of inference by exploiting the symmetries in the model. The basic principle of lifting is to perform an inference operation once for a whole group of interchangeable objects, instead of once per individual in the group. Researchers have proposed lifted versions of various (propositional) probabilistic inference algorithms, and shown large speedups achieved by the lifted algorithms over their propositional counterparts. In this dissertation, we make a number of novel contributions to lifted inference, mainly focusing on lifted variable elimination (LVE). First, we focus on constraint processing, which is an integral part of lifted inference. Lifted inference algorithms are commonly tightly coupled to a specific constraint language. We bring more insight in LVE, by decoupling the operators from the used constraint language. We define lifted inference operations so that they operate on the semantic level rather than on the syntactic level, making them language independent. Further, we show how this flexibility allows us to improve the efficiency of inference, by enhancing LVE with a more powerful constraint representation. Second, we generalize the `lifting' tools used by LVE, by introducing a number of novel lifted operators in this algorithm. We show how these operations allow LVE to exploit a broader range of symmetries, and thus expand the range of problems it can solve in a lifted way. Third, we advance our theoretical understanding of lifted inference by providing the first completeness result for LVE. We prove that LVE is complete---always has a lifted solution---for the fragment of 2-logvar models, a model class that can represent many useful relations in PLMs, such as (anti-)symmetry and homophily. This result also shows the importance of our contributions to LVE, as we prove they are sufficient and necessary for LVE to achieve completeness. Fourth, we propose the structure of first-order decomposition trees (FO-dtrees), as a tool for symbolically analyzing lifted inference solutions. We show how FO-dtrees can be used to characterize an LVE solution, in terms of a sequence of lifted operations. We further make a theoretical analysis of the complexity of lifted inference based on a corresponding FO-dtree, which is valuable for finding and selecting among different lifted solutions. Finally, we present a pre-processing method for speeding up (lifted) inference. Our goal with this method is to speed up inference in PLMs by restricting the computations to the requisite part of the model. For this, we build on the Bayes-ball algorithm that identifies the requisite variables in a ground Bayesian network. We present a lifted version of Bayes-ball, which works with first-order Bayesian networks, and show how it applies to lifted inference.

681.3 <043> --- academic collection --- Computerwetenschap--Dissertaties --- Theses

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

The importance of security and reliability of software systems makes formal methods of paramount significance for guaranteeing that a system satisfies a particular specification. Hyperproperties can be seen as an abstract formalization of security policies. Because of this, it is desirable to establish a generic verification methodology for at least the class of security-relevant hyperproperties. Unfortunately, such a generic verification methodology is lacking. This is the main motivation of this dissertation.We observe that most interesting hyperproperties that are relevant in practice come from a class of security-relevant policies, specified using universal and possibly existential quantification on traces, as well as relations on those traces. We formalize such definitions and call them holistic hyperproperties. Then our goal becomes to find a methodology for the verification of holistic hyperproperties. To that end, we explore an incremental, coalgebraic perspective on systems and specifications and as a result we arrive at a different, but related kind of specifications: incremental hyperproperties (essentially coinductive predicates). Given some holistic hyperproperty H, the respective incremental version is called H&#8242; and its definition naturally gives the notion of an H&#8242;-simulation relation. Such relations enable verification of holistic hyperproperties: finding an H&#8242;-simulation relation on a candidate system implies that the incremental hyperproperty H&#8242; holds and thus the high-level, holistic hyperproperty H holds for the candidate system. We also introduce techniques that are often helpful in translating holistic hyperproperties into incremental ones.To show that incremental hyperproperties are important in practice, we explore their connection with the most closely related verification technique — via unwinding. To achieve this, we propose a framework for coinductive unwinding of security relevant hyperproperties based on Mantel’s MAKS framework and our work on holistic and incremental hyperproperties. Mantel’s MAKS framework cannot be used directly as it is geared towards reasoning about finite behavior and is thus not suitable to reason about holistic hyperproperties in general. However, our framework has a similar structure to MAKS: coinductive unwinding relations compose (or imply) coinductive Basic Security Predicates, which in turn compose a number of security-relevant, holistic hyperproperties. It turns out that the coinductive unwinding relations we introduce are instances of H&#8242;-simulation relations. More importantly, incremental hyperproperties can be expressed in well-behaved logics and this opens the door to their verification.Finally, we propose a generic verification approach for incremental hyperproperties via game-based model checking. To achieve this, we first show how to interpret incremental hyperproperty checking as games. Although one might do regular model checking of incremental hyperproperties on a transformed system, model checking games are advantageous as they do not only produce a yes-no answer, but also give more intuition about the security policy and what can potentially go wrong, by producing a concrete winning strategy. In order to show that the theory developed here is practical, we present and illustrate methods of using several off-the-shelf tools for verification of incremental hyperproperties expressed in the polyadic modal mu-calculus

681.3 <043> --- academic collection --- Computerwetenschap--Dissertaties --- Theses