Fundamenta Informaticae

Aggregation functions are widely used in answer set programming (ASP) for representing and reasoning on knowledge involving sets of objects collectively. These sets may also depend recursively on the results of the aggregation functions, even if so far the support for such recursive aggregations was quite limited in ASP systems. In fact, recursion over aggregates was restricted to convex aggregates, i.e., aggregates that may have only one transition from false to true, and one from true to false, in this specific order. Recently, such a restriction has been overcome, so that the user can finally use non-convex recursive aggregates in ASP programs. An evaluation of ASP programs with non-convex recursive aggregates is reported in this paper, also testing a recently proposed extension of the concept of the positive extension graph to the case of programs with aggregates. Moreover, as an additional contribution, new rewritings for EVEN and ODD are presented: EVEN maps to true aggregation sets containing an even number of true literals, and ODD maps to true aggregation sets containing an odd number of true literals. Both aggregates are non-convex, and previously replaced by a conjunction of non-convex sums, whose size is quadratic with respect to the number of literals in the aggregation set. A different rewriting is presented in this paper, whose size is linear with respect to the number of literals in the aggregation set.

Logic programming provides a declarative framework for modeling and solving many combinatorial problems. Until recently, it was not competitive with state-of-the-art planning techniques partly due to search capabilities limited to backtracking. Recent development brought more advanced search techniques to logic programming such as tabling that simplifies implementation and exploitation of more sophisticated search algorithms. Together with rich modeling capabilities this progress brings tabled logic programing on a par with current best planners.

This paper describes the planner module of the tabled logic programming language Picat, its modeling capabilities, and core search procedures behind the planner. The major contribution is an experimental comparison of the influence of various modeling techniques, namely factored vs. structured representations of states, control knowledge, and heuristics on the performance of two search procedures – iterative deepening and branch and bound – behind the planner. The paper also compares the Picat planner with winning automated planners both domain dependent and domain independent to demonstrate that the presented techniques are competitive with state-ofthe- art.

We define a new protocol rule, Now or Never (NoN), for bilateral negotiation processes which allows self-motivated competitive agents to efficiently carry out multi-variable negotiations with remote untrusted parties, where privacy is a major concern and agents know nothing about their opponent. By building on the geometric concepts of convexity and convex hull, NoN ensures a continuous progress of the negotiation, thus neutralising malicious or inefficient opponents. In particular, NoN allows an agent to derive in a finite number of steps, and independently of the behaviour of the opponent, that there is no hope to find an agreement. To be able to make such an inference, the interested agent may rely on herself only, still keeping the highest freedom in the choice of her strategy.

We also propose an actual NoN-compliant strategy for an automated agent and evaluate the computational feasibility of the overall approach on both random negotiation scenarios and case studies of practical size.

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variations in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment.

In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to (Hardware In the Loop Simulation based) System Level Formal Verification.

SyLVaaS takes as input a finite state automaton defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion (i.e., with no communication among the parallel processes) on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS Web site.

As the actual simulation is carried out at the user premises (e.g., on a private cluster), SyLVaaS allows full Intellectual Property protection of the SUV model as well as of the user verification flow.

The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity.

We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on case studies consisting of input operational environments entailing up to 35 641 501 scenarios related to the system level verification of models from the Simulink distribution (namely, Inverted Pendulum on a Cart and Fuel Control System).

Twelve years have elapsed since the first Quantified Boolean Formulas (QBFs) evaluation was held as an event linked to SAT conferences. During this period, researchers have striven to propose new algorithms and tools to solve challenging formulas, with evaluations periodically trying to assess the current state of the art. In this paper, we present an experimental account of solvers and formulas with the aim to understand the progress in the QBF arena across these years. Unlike typical evaluations, the analysis is not confined to the snapshot of submitted solvers and formulas, but rather we consider several tools that were proposed over the last decade, and we run them on different formulas from previous QBF evaluations. The main contributions of our analysis, which are also the messages we would like to pass along to the research community, are: (i) many formulas that turned out to be difficult to solve in past evaluations, remain still challenging after twelve years, (ii) there is no single solver which can significantly outperform all the others, unless specific categories of formulas are considered, and (iii) effectiveness of preprocessing depends both on the coupled solver and the structure of the formula.

We study abduction in First Order Horn logic theories where all atoms can be abduced and we are looking for preferred solutions with respect to three objective functions: cardinality minimality, coherence, and weighted abduction. We represent this reasoning problem in Answer Set Programming (ASP), in order to obtain a flexible framework for experimenting with global constraints and objective functions, and to test the boundaries of what is possible with ASP. Realizing this problem in ASP is challenging as it requires value invention and equivalence between certain constants, because the Unique Names Assumption does not hold in general. To permit reasoning in cyclic theories, we formally describe fine-grained variations of limiting Skolemization. We identify term equivalence as a main instantiation bottleneck, and improve the efficiency of our approach with on-demand constraints that were used to eliminate the same bottleneck in state-ofthe- art solvers. We evaluate our approach experimentally on the ACCEL benchmark for plan recognition in Natural Language Understanding. Our encodings are publicly available, modular, and our approach is more efficient than state-of-the-art solvers on the ACCEL benchmark.

Case-based planning can fruitfully exploit knowledge gained by solving a large number of problems, storing the corresponding solutions in a plan library and reusing them for solving similar planning problems in the future. Case-based planning is very effective when similar reuse candidates can be efficiently and effectively chosen.

In this paper, we study an innovative technique based on planning problem features for efficiently retrieving solved planning problems (and relative plans) from large plan libraries. A problem feature is a characteristic –usually provided under the form of a number– of the instance that can be automatically derived from the problem specification, domain and search space analyses, or different problem encodings. Given a planning problem to solve, its features are extracted and compared to those of problems stored in the case base, in order to identify most similar problems. Since the use of existing planning features is not always able to effectively distinguish between problems within the same planning domain, we introduce a large number of new features.

An experimental analysis in this paper investigates the best set of features to be exploited for retrieving plans in case-based planning, and shows that our feature-based retrieval approach can significantly improve the performance of a state-of-the-art case-based planning system.