Franz Baader

Talk title: Ontology-Based Monitoring of Dynamic Systems

Abstract:
Our understanding of the notion “dynamic system” is a rather broad one: such a system has states, which can change over time. Ontologies are used to describe the states of the system, possibly in an incomplete way. Monitoring is then concerned with deciding whether some run of the system or all of its runs satisfy a certain property, which can be expressed by a formula of an appropriate temporal logic. We consider different instances of this broad framework, which can roughly be classified into two cases. In one instance, the system is assumed to be a black box, whose inner working is not known, but whose states can be (partially) observed during a run of the system. In the second instance, one has (partial) knowledge about the inner working of the system, which provides information on which runs of the system are possible.
In this talk, we will review some of our recent research that investigates different instances of this general framework of ontology-based monitoring of dynamic systems. We will also sketch possible extensions towards probabilistic reasoning and the integration of mathematical modelling of dynamical systems.

Edmund Clarke

Talk title: Verification of Computer Systems with Model Checking

Abstract:
Model Checking is an automatic verification technique for large state transition systems. The technique has been used successfully to debug complex computer hardware and communication protocols. Now, it is beginning to be used for complex hybrid (continuous/discrete) systems as well. The major disadvantage of the technique is a phenomenon called the State Explosion Problem. This problem is impossible to avoid in worst case. However, by using sophisticated data structures and clever search algorithms, it is now possible to verify hybrid systems with astronomical numbers of states.

Christos Papadimitriou

Talk title: Computational Ideas and the Theory of Evolution

Abstract:
Covertly computational insights have influenced the Theory of Evolution from the very start. I shall discuss recent work on some central problems in Evolution that was inspired and informed by computational ideas. Considerations about the performance of genetic algorithms led to a novel theory of the role of sex in Evolution based on the concept of mixability, the population genetic equations describing the evolution of a species can be reinterpreted as a repeated game between genes played through the multiplicative update algorithm, while a theorem on satisfiability can shed light on the emergence of complex adaptations.

Alex Wilkie

Talk title: The theory and applications of o-minimal structures

Abstract:
This is a talk in the branch of logic known as model theory, more precisely, in o-minimality. The first example of an o-minimal structure is the ordered algebraic structure on the set of real numbers and I shall focus on expansions of this structure. Being o-minimal means that the first order definable sets in the structure do not exhibit wild phenomena (this will be made precise). After discussing some basic theory of such structures I shall present some recent applications to diophantine geometry.

Véronique Cortier

Talk title: Electronic voting: how logic can help?

Abstract:

Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more traditional case of authentication or key exchange protocols. All these protocols are notoriously difficult to design and flaws may be found years after their first release. Formal models, such as process algebra, Horn clauses, or constraint systems, have been successfully applied to automatically analyze traditional protocols and discover flaws. Electronic voting protocols however significantly increase the difficulty of the analysis task. Indeed, they involve for example new and sophisticated cryptographic primitives, new dedicated security properties, and new execution structures.

After an introduction to electronic voting, we will describe the current techniques for e-voting protocols analysis and review the key challenges towards a fully automated verification.

Orna Kupferman

Talk title: From Reachability to Temporal Specifications in Game Theory

Abstract:

Multi-agents games are extensively used for modelling settings in which different entities share resources. For example, the setting in which entities need to route messages in a network is modelled by network-formation games: the network is modelled by a graph, and each agent has to select a path satisfying his reachability objective. In practice, the objectives of the entities are often more involved than reachability. The need to specify and reason about rich specifications has been extensively studied in the context of verification and synthesis of reactive systems. The talk describes a lifting of ideas from formal methods to multi-agent games. For example, in network-formation games with regular objectives, the edges of the graph are labeled by alphabet letters and the objective of each player is a regular language over the alphabet of labels. Thus, beyond reachability, a player may restrict attention to paths that satisfy certain properties, referring, for example, to the providers of the traversed edges, the actions associated with them, their quality of service, security, etc.

The talk assumes no previous knowledge in game theory. We will introduce the basic concepts and problems, describe how their extension to games with more expressive specification of objectives poses new challenges, and study the resulting games.

Joint work with Guy Avni and Tami Tamir.