University of Calabria, Italy
Optimization problems in answer set programming
Answer set programming (ASP) is a declarative language for nonmonotonic reasoning based on stable model semantics, where stable models are classical models of the input program satisfying a stability condition: only necessary information is included in each of these models under the assumptions provided by the model itself for the unknown knowledge in the program, where unknown knowledge is encoded by means of default negation.
Reasoning in presence of unknown knowledge is common for rational agents acting in the real world.
It is also common that real world agents cannot meet all their desiderata, and therefore ASP programs may come with soft literals for representing numerical preferences over jointly incompatible conditions.
Stable models are therefore associated with a cost given by the number of the unsatisfied soft literals, so that stable models of minimum cost are preferred.
In this talk I will show algorithms and strategies for computing optimal stable models, discuss their properties and explain how they can be extended to handle some qualitative preferences.
DISIT, University of Piemonte Orientale, Italy
Reasoning about exceptions in ontologies: a preferential approach in Description Logics
Reasoning about exceptions in ontologies is nowadays one of the challenges the description logics community is facing, a challenge that was already at the very roots of the development of non-monotonic reasoning in the 80’s. The talk describes the preferential approach for dealing with exceptions in Description Logics, where a “typicality operator” is used to select the typical (or most preferred) instances of a concept. A rational closure construction is introduced which is semantically characterized by minimal preferential models.
The presentation will discuss the main achievements of the approach, as well as open issues, both for expressive description logics and for low complexity description logics (such as those at the basis of the OWL EL profile). For the description logics of the EL family, we will describe how preferential and minimal entailment can be computed in Datalog and in Answer Set Programming.
Imperial College London, UK
Towards the Formal Verification of Correctness and Robustness of Robotic Swarms
Robot swarms are large collections of small robots, typically running lightweight programs, interacting with their neighbours and the environment. In recent years swarm robotics has shown considerable applicability in a wide range of domains, including search and rescue,
automatic mining, and plant monitoring. In this talk I will survey some of our results on the formal verification of swarms.
I will begin by arguing that swarm systems benefit from logic-based specification languages typically used in AI and multi-agent systems that go beyond plain temporal logic, but also concern the knowledge, the intentions, and the strategic abilities of the agents in the system.
I will continue by highlighting the key semantical and algorithmic aspects of present approaches to the symbolic verification of multi-agent systems against temporal-epistemic specifications. I will then move to the case of swarms where the number of agents is
unbounded at design time. I will illustrate a semantics based on agent templates and introduce the parameterised model checking problem (PMCP) as the decision problem of establishing whether all infinitely many concrete instances of a swarm design based on agent templates satisfies a given temporal-epistemic specification. Cut-off procedures
to solve the PMCP will be presented together with alternative approaches such as counter-abstraction.
I will conclude by exploring the issue of resilience of a swarm. To do this, I will introduce the parameterised fault-tolerance problem as the decision problem of establishing whether any concrete system in which the ratio of faulty versus total number of agents is bounded by a parameter, satisfies a given temporal-epistemic specification. I will illustrate how faults can be injected automatically into correct designs so that the resulting mutated models can be automatically analysed and conclusions on the resilience of the original design can be drawn.