We present a formulation of the problem of probabilistic model checking as one of query evaluation over probabilistic logic programs. To the best of our knowledge, our formulation is the first of its kind, and it cove...
详细信息
We present a formulation of the problem of probabilistic model checking as one of query evaluation over probabilistic logic programs. To the best of our knowledge, our formulation is the first of its kind, and it covers a rich class of probabilistic models and probabilistic temporal logics. The inference algorithms of existing probabilistic logic-programming systems are well defined only for queries with a finite number of explanations. This restriction prohibits the encoding of probabilistic model checkers, where explanations correspond to executions of the system being model checked. To overcome this restriction, we propose a more general inference algorithm that uses finite generative structures (similar to automata) to represent families of explanations. The inference algorithm computes the probability of a possibly infinite set of explanations directly from the finite generative structure. We have implemented our inference algorithm in XSB Prolog, and use this implementation to encode probabilistic model checkers for a variety of temporal logics, including PCTL and GPL (which subsumes PCTL*). Our experiment results show that, despite the highly declarative nature of their encodings, the model checkers constructed in this manner are competitive with their native implementations.
Separation logic formalizes the idea of local reasoning for heap-manipulating programs via the frame rule and the separating conjunction P * Q, which describes states that can be split into separate parts, with one sa...
详细信息
ISBN:
(纸本)9783642288685;9783642288692
Separation logic formalizes the idea of local reasoning for heap-manipulating programs via the frame rule and the separating conjunction P * Q, which describes states that can be split into separate parts, with one satisfying P and the other satisfying Q. In standard separation logic, separation means physical separation. In this paper, we introduce fictional separation logic, which includes more general forms of fictional separating conjunctions P * Q, where * does not require physical separation, but may also be used in situations where the memory resources described by P and Q overlap. We demonstrate, via a range of examples, how fictional separation logic can be used to reason locally and modularly about mutable abstract data types, possibly implemented using sophisticated sharing. Fictional separation logic is defined on top of standard separation logic, and both the meta-theory and the application of the logic is much simpler than earlier related approaches.
The seaport of Gioia Tauro is the largest transshipment terminal of the Mediterranean coast. A crucial management task for the companies operating in the seaport is team-building: the problem of properly allocating th...
详细信息
The seaport of Gioia Tauro is the largest transshipment terminal of the Mediterranean coast. A crucial management task for the companies operating in the seaport is team-building: the problem of properly allocating the available personnel for serving the incoming ships. Teams have to be carefully arranged in order to meet several constraints, such as allocation of employees with appropriate skills, fair distribution of the working load, and turnover of the heavy/dangerous roles. This makes team-building a hard and expensive task requiring several hours of manual preparation per day. In this paper we present a system based on Answer Set programming for the automatic generation of the teams of employees in the seaport of Gioia Tauro. The system is currently exploited in the Gioia Tauro seaport by ICO BLG, a company specialized in automobile logistics.
Abstract The module theorem by Janhunen et al. demonstrates how to provide a modular structure in answer set programming, where each module has a well-defined input/output interface which can be used to establish the ...
详细信息
Abstract In prior work, we showed that logicprogramming compilation can be given a proof-theoretic justification for generic abstract logicprogramming languages, and demonstrated this technique in the case of heredi...
详细信息
Probabilistic logicprogramming (PLP), exemplified by Sato and Kameya's PRISM, Poole's ICL, Raedt et al.'s ProbLog and Vennekens et al.'s LPAD, is aimed at combining statistical and logical knowledge r...
详细信息
Probabilistic logicprogramming (PLP), exemplified by Sato and Kameya's PRISM, Poole's ICL, Raedt et al.'s ProbLog and Vennekens et al.'s LPAD, is aimed at combining statistical and logical knowledge representation and inference. However, the inference techniques used in these works rely on enumerating sets of explanations for a query answer. Consequently, these languages permit very limited use of random variables with continuous distributions. In this paper, we present a symbolic inference procedure that uses constraints and represents sets of explanations without enumeration. This permits us to reason over PLPs with Gaussian or Gamma-distributed random variables (in addition to discrete-valued random variables) and linear equality constraints over reals. We develop the inference procedure in the context of PRISM;however the procedure's core ideas can be easily applied to other PLP languages as well. An interesting aspect of our inference procedure is that PRISM's query evaluation process becomes a special case in the absence of any continuous random variables in the program. The symbolic inference procedure enables us to reason over complex probabilistic models such as Kalman filters and a large subclass of Hybrid Bayesian networks that were hitherto not possible in PLP frameworks.
We present and evaluate a compiler from Prolog (and extensions) to JavaScript which makes it possible to use (constraint) logicprogramming to develop the client side of web applications while being compliant with cur...
详细信息
We present and evaluate a compiler from Prolog (and extensions) to JavaScript which makes it possible to use (constraint) logicprogramming to develop the client side of web applications while being compliant with current industry standards. Targeting JavaScript makes (C) LP programs executable in virtually every modern computing device with no additional software requirements from the point of view of the user. In turn, the use of a very high-level language facilitates the development of high-quality, complex software. The compiler is a back end of the Ciao system and supports most of its features, including its module system and its rich language extension mechanism based on packages. We present an overview of the compilation process and a detailed description of the run-time system, including the support for modular compilation into separate JavaScript code. We demonstrate the maturity of the compiler by testing it with complex code such as a CLP(FD) library written in Prolog with attributed variables. Finally, we validate our proposal by measuring the performance of some LP and CLP(FD) benchmarks running on top of major JavaScript engines.
Traditional approaches to automatic AND-parallelization of logic programs rely on some static analysis to identify independent goals that can be safely and efficiently run in parallel in any possible execution. In thi...
详细信息
Traditional approaches to automatic AND-parallelization of logic programs rely on some static analysis to identify independent goals that can be safely and efficiently run in parallel in any possible execution. In this paper, we present a novel technique for generating annotations for independent AND-parallelism that is based on partial evaluation. Basically, we augment a simple partial evaluation procedure with (run-time) groundness and variable sharing information so that parallel conjunctions are added to the residual clauses when the conditions for independence are met. In contrast to previous approaches, our partial evaluator is able to transform the source program in order to expose more opportunities for parallelism. To the best of our knowledge, we present the first approach to a parallelizing partial evaluator.
Answer Set programming (ASP) is a well-known problem solving approach based on nonmonotonic logic programs and efficient solvers. To enable access to external information, HEX-programs extend programs with external at...
详细信息
Answer Set programming (ASP) is a well-known problem solving approach based on nonmonotonic logic programs and efficient solvers. To enable access to external information, HEX-programs extend programs with external atoms, which allow for a bidirectional communication between the logic program and external sources of computation (e. g., description logic reasoners and Web resources). Current solvers evaluate HEX-programs by a translation to ASP itself, in which values of external atoms are guessed and verified after the ordinary answer set computation. This elegant approach does not scale with the number of external accesses in general, in particular in presence of nondeterminism (which is instrumental for ASP). In this paper, we present a novel, native algorithm for evaluating HEX-programs which uses learning techniques. In particular, we extend conflict-driven ASP solving techniques, which prevent the solver from running into the same conflict again, from ordinary to HEX-programs. We show how to gain additional knowledge from external source evaluations and how to use it in a conflict-driven algorithm. We first target the uninformed case, i.e., when we have no extra information on external sources, and then extend our approach to the case where additional meta-information is available. Experiments show that learning from external sources can significantly decrease both the runtime and the number of considered candidate compatible sets.
In this work, we propose Answer-Set programming (ASP) as a tool for rapid prototyping of dynamic programming algorithms based on tree decompositions. In fact, many such algorithms have been designed, but only a few of...
详细信息
In this work, we propose Answer-Set programming (ASP) as a tool for rapid prototyping of dynamic programming algorithms based on tree decompositions. In fact, many such algorithms have been designed, but only a few of them found their way into implementation. The main obstacle is the lack of easy-to-use systems which (i) take care of building a tree decomposition and (ii) provide an interface for declarative specifications of dynamic programming algorithms. In this paper, we present D-FLAT, a novel tool that relieves the user of having to handle all the technical details concerned with parsing, tree decomposition, the handling of data structures, etc. Instead, it is only the dynamic programming algorithm itself which has to be specified in the ASP language. D-FLAT employs an ASP solver in order to compute the local solutions in the dynamic programming algorithm. In the paper, we give a few examples illustrating the use of D-FLAT and describe the main features of the system. Moreover, we report experiments which show that ASP-based D-FLAT encodings for some problems outperform monolithic ASP encodings on instances of small treewidth.
暂无评论