Phokion G. Kolaitis
University of California Santa Cruz
IBM Research Almaden
Schema Mappings and Data Examples: An Interplay between Syntax and Semantics
Schema mappings are high-level specifications that describe the relationship between two database schemas. Schema mappings constitute the essential building blocks in such critical data inter-operability tasks as data exchange and data integration. For this reason, schema mappings have been the focus of extensive research investigations over the past several years. Since in real-life applications schema mappings can be quite complex, it is important to develop methods and tools for illustrating, explaining, and deriving schema mappings. A promising approach to this effect is to use “good” data examples that illustrate the schema mapping at hand.
In this talk, we will present an overview of recent work on characterizing and deriving schema mappings via a finite set of data examples. We will focus on unique characterizations of schema mappings via a finite set of universal examples and on the learnability of schema mappings from data examples. Along the way, we will unveil a tight connection between unique characterizability of schema mappings and homomorphism dualities in constraint satisfaction.
This is joint work with Bogdan Alexe (IBM Research – Almaden), Balder ten Cate (LogicBlox and UC Santa Cruz), and Wang-Chiew Tan (UC Santa Cruz).
Alessio R. Lomuscio
Imperial College, London
Advances in symbolic model checking for multi-agent systems.
Multi-agent systems (MAS) are distributed autonomous systems
in which the components, or agents, act autonomously or collectively
in order to reach private or common goals. Logic-based specifications
for MAS typically do not only involve their temporal evolution, but
also other agent attitudes, including their knowledge, intentions,
their strategic abilities, etc.
This talk will survey some of our work on model checking MAS against
agent-based specifications. Serial and parallel algorithms for
symbolic model checking against temporal-epistemic specifications as
well as bounded-model checking procedures will be discussed. MCMAS, an
open-source model checker, developed in the VAS group at Imperial
College London, will be briefly demonstrated. A case study concerning
the verification of diagnosability and fault-tolerance of an autonomous
underwater vehicles will be discussed.
I will conclude by considering the case of open MAS where the number of
agents is unbounded. In this context I will report recent results that
enable us to establish a cut-off of a MAS, i.e., the maximal number of
agents that need to be verified for conclusions to be drawn on any
system of any number of components.
Termination of Linear Programs: Advances and Challenges
In the quest for program analysis and verification, program termination — determining whether a given program will always halt or could execute forever — has emerged as a pivotal component. Although proven undecidable in the general case by Alan Turing over 80 years ago, decidability results have been obtained in a variety of restricted instances. We survey the situation with a focus on simple linear programs, i.e., WHILE loops in which all assignments and guards are linear, discussing recent progress as well as ongoing and emerging challenges.