Future Talks

Ioana Boureanu: Relay-Secure Contactless Payments Even in Presence of Malicous PoS


In relay attacks on contactless payments, an adversary can make an illicit payment in the name a card found outside the accepted range of the point-of-sale (PoS). In this talk, we will discuss the design, formal security-analysis and implementation of contactless payments which are secure against relay attacks even when the PoS is malicious. Our strongly-secure constructions are (in part) backward-compatible with the current EMV standard for contactless payments. For our analysis, we put forward a new formal model for capturing strong relay attacks, a new result for security analysis in this space and a mechanisation in ProVerif. This work is part of a research funded under UK's Research Institute for Secure Hardware and Embedded Systems (RISE), carried out in collaboration (amongst others) with Visa, Mastercard.

Short Bio

Ioana Boureanu is a Senior Lecturer (Associate Professor) in Secure Systems at University of Surrey, in the UK. She obtained her PhD in formal verification of security protocols from Imperial College London (2011). She went on to be a postdoctoral researcher and lecturer in LASEC (Laboratory of Security and Cryptography) at EPFL, Lausanne, Switzerland. She also worked in industry as a security architect at Akamai. She was awarded an H2020 Marie-Curie fellowship in 2015, which she did at Imperial College London. In 2016, she moved to University of Surrey, at the Surrey Centre for Cyber Security. Her research focuses on (automatic) analysis of security using mainly logic-based formalisms, as well as on provable security and applied cryptography, with particular interests in lightweight mechanisms and IoT security.

11th March 2020, 14:00, TBA

Past Talks

Sanjay Modgil: Dialectical Formalizations of Non-monotonic Reasoning: Rationality under Resource Bounds


ASPIC+ is a widely used framework that provides for dialectical formalizations of non-monotonic logics. That is to say, the non-monotonic inferences defined by sets of formulae can equivalently be defined in terms of the claims of arguments that successfully defend themselves against counter-arguments. ASPIC+ provides guidelines for ensuring that any such dialectical formalization yields rational outcomes; notably, that the claims of winning arguments are mutually consistent. However, rationality in this sense is guaranteed only under the assumption that agents are logically omniscient (i.e., they have unbounded resources). Moreover, ASPIC+ is not fully rational, in the sense that given a set of formulae A, then the argumentation defined inferences from A may be retracted when adding some set B that is syntactically disjoint from A (a problem known as contamination). In this talk I will present a new version of ASPIC+ that adopts a radically new notion of argument and counter-argument, and that can be shown to be fully rational under resource bounds. This then means that resource bounded agents can now reason non-monotonically, as individuals or jointly via dialogue, while guaranteeing rational outcomes.
This is joint work with Professor Marcello D’Agostino at the Department of Philosophy, University of Milan.

Short Bio

Sanjay Modgil is a senior lecturer at King’s College London. His primary area of research is in argumentation theory. His key contributions in this area include: 1) the ASPIC+ framework and its provision of dialectical characterisations of non-monotonic reasoning for single agent inference and distributed reasoning in the form of multi-agent dialogues; 2) extensions to the standard model of argumentation so as to accommodate reasoning about (possibly conflicting) preferences and values, and application of these extensions to ethical and moral reasoning. More recently, his focus has been on graded generalisations of Dung’s theory of argumentation, and dialectical formalisations of non-monotonic reasoning that are provably rational under resource bounds.

20th June 2019, 11:00, LT 140

David Pearce: The Logical Basis of Knowledge Representation in Answer Set Programming


In this talk I give an introduction to the underlying logic of Answer Set Programming. The basis is a non-classical, intermediate logic and its non-monotonic extension, known as equilibrium logic. Together they provide an alternative to the standard paradigm of two-valued, classical logic. In view of the origins of answer set programming, it seems appropriate to call this new approach stable reasoning. The talk will focus on the intuitive meaning of the main logical definitions, and explain their effect with some example programs. I will also discuss some of the main extensions of the basic language that may be useful for knowledge representation. In the last part of the talk I will discuss briefly the role that logic could play in the future of AI where Machine Learning is becoming a dominant paradigm.

23th May 2019, 12:00, Huxley 140

Samy Sa: Assumption-Based Argumentation as Logic Programming with Selection


In this talk, we will explore the semantic connections between Assumption-Based Argumentation (ABA) and Logic Programming (LP). We exploit the recently proposed model-based semantics for ABA frameworks, a format that evaluates non-assumptions as well as assumptions in the framework's language. We provide new translations between ABA frameworks and logic programs and show that the models of an ABA framework are precisely the same as those of its corresponding logic program for all flavors of specialization to the complete semantics. In particular, this allows us to further understand the difference between the L-stable and semi-stable semantics, which are found not to coincide in several works involving this same methodology we employ. What is more, out while previous works focus solely on flat ABA frameworks, out results suggest that non-flat ABA frameworks may also be encompassed by normal logic programs. Through all steps, we will be arguing the selection operator from relational algebra has a pivotal role in ABA, as it allows mapping model-based semantics to its labelling-based counterpart, characterizes the difference between semi-stable and L-stable semantics, and ensures every logic program can be transformed into another that has an ABA-framework-like structure and preserves its original semantics.

17th April 2019, 12:00, Huxley 145

Giuseppe Perelli: From Synthesis to Rational Synthesis: a Game-Theoretic Approach


Rational Synthesis is a recent and natural evolution of the Synthesis problem in which the hostility assumption of environment is replaced by rationality of agents, each of them representing an autonomous component. In terms of games, this corresponds to no longer maximizing an individual payoff against all possible environment's behaviours (two-player zero-sum), but rather synthesising a strategy profile that is in some sort of equilibrium, i.e., prevents agents to improve payoff by deviating from it (multi-player nonzero-sum). The Rational Synthesis problem has been recently introduced and investigated under a variety of settings, each of them corresponding to a precise game-theoretic formulation. In this talk, after giving a general introduction to the Synthesis and Rational Synthesis problems, we will present recent results and developments in the area, showing how the game-theoretic setting comes in very handy for representing and solving them.

Short Bio

Giuseppe Perelli is Research Associate at the Department of Informatics, University of Leicester, enrolled in the DSynMA project and, so, working with Prof. Nir Piterman. Prior to this, he was Research Assistant at the University of Oxford, working on the ERC project "RACE" led by Prof. Michael Wooldridge.He got his PhD at Università di Napoli "Federico II" under the supervision of Prof. Aniello Murano. He also visited Rice University (Houston, TX) working with Prof. Moshe Y. Vardi. His research interests include: formal specification, verification, and synthesis; decidability and expressiveness of logic-based languages for strategic reasoning; Equilibrium synthesis for infinite duration games.

April 10, 2pm, room TBD

Stéphane Demri: A Framework for Modalities and Separating Connectives


Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order to verify programs with mutable data structures. The separating conjunction allows us to evaluate formulae in subheaps, and this possibility to evaluate formulae in alternative modelsis a feature shared with many modal logics such as sabotage logics,or relation-changing modal logics. We introduce several versions of modal separation logics whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction. Fragments are genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. We present the decidability status and the computational complexity of several modal separation logics, providing hints about their expressive power. The second part of the talk is dedicated to their relationships with second-order modal logics on tree models, and to the design of internal calculi for a few elementary modal separation logics. Part of the presented work is done jointly with B. Bednarczyk (U. of Wroclaw), R. Fervari (U. of Cordoba) and A. Mansutti (LSV, ENS Paris-Saclay).

Short Bio

Stéphane Demri, Directeur de Recherche CNRS, is currently the head of Laboratoire Specification et Verification (LSV), CNRS & Ecole Normale Superieure Paris-Saclay, France. He has been a Marie Curie IOF Fellow during 2012--2015 (New York University and LSV). His research interests include verification of infinite-state systems, resource logics, temporal logics and analysis of systems with data. He has published over 100 publications in the field of formal/logical methods for analysing computer systems including a book "Temporal Logics in Computer Science" co-authored with V. Goranko and M. Lange, CUP, 2016. Personal Website.

April 2, 2pm, room 144

Yves Lesperance: Abstraction in Situation Calculus Action Theories


In this talk, I will present a general framework for agent abstraction based on the situation calculus and the ConGolog agent programming language. We assume that we have a high-level specification and a low-level specification of the agent, both represented as basic action theories. A refinement mapping specifies how each high-level action is implemented by a low-level ConGolog program and how each high-level fluent can be translated into a low-level formula. We define a notion of sound abstraction between such action theories in terms of the existence of a suitable bisimulation between their respective models. Sound abstractions have many useful properties that ensure that we can reason about the agent's actions (e.g., executability, projection, and planning) at the abstract level, and refine and concretely execute them at the low level. We also characterize the notion of complete abstraction where all actions (including exogenous ones) that the high level thinks can happen can in fact occur at the low level. I will also outline how the framework can be extended to online executions where the agent can acquire new knowledge through sensing as it executes. Finally, I will briefly discuss how the framework can be used to more efficiently perform agent supervision, i.e., minimally restrict the agent's behaviour to ensure it satisfies some specification. This is joint work with my PhD student Bita Banihashemi as well as with Giuseppe De Giacomo of Sapienza University of Rome. The core aspects of the framework have appeared in Proc. AAAI 2017. The results on abstraction in online executions have appeared at IJCAI 2018 and those on hierarchical agent supervision at AAMAS 2018.

Short Bio

Yves Lesperance is Associate Professor in the Department of Electrical Engineering and Computer Science, York University, Toronto, Canada. He received a Ph.D. in Computer Science from the University of Toronto in 1991. His research is in the areas of knowledge representation and reasoning and intelligent agents and multiagent systems. His work on agent programming languages (Golog and ConGolog) and on reasoning about action and mental states in the situation calculus has had a major impact. He is the author of over 120 scholarly publications. He is Associate Editor of both Artificial Intelligence Journal and the Journal of Artificial Intelligence Research (JAIR), the two top journals in the field. He was Local Organization Chair of the International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS) in 2010. He was also a member of the Board of the International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS) from 2007 to 2010.

March 19, 12pm, room 144