Arved will give a talk on Propagator Networks for Unification and Proof Search on Monday (29.03) and Jay will present his research on Trustable Machine Learning Systems on Tuesday (30.03).

# Category Archives: Research

# Talk by Adam Ó Conghaile

Today Adam Ó Conghaile will give a talk on “Games & Comonads in Finite Model Theory” as a part of our Theory Seminar Series.

**Abstract.** Model-comparison games (such as Ehrenfeucht-Fraïssé games, pebble games and modal bisimulation) capture various approximations to isomorphism and homomorphism between structures. These approximations are important and well-studied in computer science for their connections with logic and algorithms but their descriptions are often ad hoc and unified approach to these games is lacking in classical finite model theory. Game comonads, introduced by Abramsky, Dawar & Wang [1], provide a categorical semantics for these games which reveals connections between these games and relates them in a surprising and elegant way to structural parameters such as treewidth.

In my talk, I will survey the landscape of model-comparison games and developments in this new comonadic perspective to them, including contributions from my recent work with Anuj Dawar on game comonads for logics with generalised quantifiers. [2]

[1] – S. Abramsky, A. Dawar, P. Wang *The pebbling comonad in finite model theory*, LiCS 2017

[2] – A. Ó Conghaile, A. Dawar *Game comonads & generalised quantifiers*, CSL 2021

# CCC 2020

A number of Swansea theory group members are attending the CCC 2020 (Continuity, Computability, Constructivity – From Logic to Algorithms) conference, taking place from 31 August to 4 September via Zoom. Their work will be presented in the following talks:

- Ulrich Berger, Andrew Lawrence and Monika Seisenberger
*Towards the extraction of clause learning* - Tonicha Crook and Arno Pauly
*Finding Roots of Polynomials* - Arno Pauly
*On the non-existence of some universal spaces*

CCC conference series are linked to the CID project that Swansea University actively participates in the recent years. This year the conference features talks by a number of invited speakers:

- Holger Boche (Munich)
- Elvira Mayordomo (Zaragoza)
- Eike Neumann (Oxford)
- Hideki Tsuiki (Kyoto)

# Working remotely but staying together

# Tonicha at CiE

Our PhD student Tonicha Crook attended her first CIE conference and gave an interesting talk on *The Weihrauch degree of finding Nash Equilibria in multiplayer games.*

First CiE conference this year was great and full of interesting talks! Happy to have been part of the informal presentations. Hopefully next year I can meet everyone in person @AssociationCiE @AimlaCcommunity pic.twitter.com/CboAATtgYh

— Tonicha Crook (@TonichaCrook) July 2, 2020

# Prawf: an interactive proof assistant for program extraction (CIE 2020 talk)

# BCTCS 2020 going ahead

In spite of the COVID-19 outbreak, we are glad to host BCTCS 2020 starting today, even if virtually. For more information on invited and contributed talks, check the official BCTCS 2020 website.

# 25th International Workshop on Algebraic Development Techniques 2020

Today Swansea is hosting the first virtual WADT, and you are gently invited to participate.

The virtual WADT is part of the 25th International Workshop on Algebraic Development Techniques 2020, which hopefully will still happen as a physical meeting in autumn this year. The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as a formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems).

The workshop takes place under the auspices of IFIP WG 1.3.

Please see below for the programme.

# Seminar series on Computability Theory and its Applications

Our colleague Arno Pauly is on the Programme Committee of the Computability Theory and its Applications seminar series, which currently is taking place virtually.

The seminar now has a YouTube channel where you can find the recordings of past talks you may have missed. The information on future talks, the timings of those, and the links to the videos are all available on the webpage here:

# Yoruki Yamagata’s talk on Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning

**Due to COVID-19 outbreak across the world, we need to move our theory seminars online to ZOOM.** We are staying on track with the schedule and **Yoriyuki Yamagata** will give his talk tomorrow at 2pm.

Topic:* Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning.*

Abstract: “Falsification” is a method to find a system input or parameter (counter-example) which causes a behavior violating a given specification (usually given by metric or signal temporal logic). Because the correctness of a complex CPS is difficult to be proven, falsification is more practical approach than full verification. A counter-example found by falsification can be used for debugging and testing. Failure of falsification does not generally mean the correctness of the system, but suggests it in some degree. “Robustness guided falsification” is an approach of falsification. “Robustness” is a numerical measure of how robustly a formula holds. If robustness becomes negative, the formula is false. Therefore, minimizing robustness can lead falsification of a formula.

In this talk, we introduce a method to recast robustness guided falsification to a “reinforcement learning problem”. Reinforcement learning is a machine learning technique in which an agent finds a law of an interacting environment and maximizes a reward. We implement our method using “deep reinforcement leaning”, in which deep neural networks are used, and present a case study to explore its effectiveness. (This work is a collaboration with Shuang Liu, Takumi Akazaki, Yihai Duan, Jianye Hao)