### Thursday, February 27, 2020 in Google Hall 214

**Ulrich Kohlenbach
(Technische Universität Darmstadt)
A quantitative analysis of the ''Lion-Man" game
**

**Abstract**: We analyze, based on an interplay between ideas and techniques from logic and geometric analysis, a pursuit-evasion game. More precisely, we focus on a discrete lion and man game with an $\varepsilon$-capture criterion. We prove that in uniformly convex bounded domains the lion always wins and, using ideas stemming from proof mining, we extract a uniform rate of convergence for the successive distances between the lion and the man. As a byproduct of our analysis, we study the relation among different convexity properties in the setting of geodesic spaces.

Joint work with Genaro López-Acedo and Adriana Nicolae.

### Thursday, December 19, 2019

**Marian Călborean (University of Bucharest)
First-order logic and vagueness
**

**Abstract**: The Sorites paradox is usually studied as a propositional paradox. However, the general form of the Sorites is second-order, with three main features. It doesn’t contain any arbitrary parameters. It can be used to generate the propositional Sorites by appropriate replacement of the second-order premise with arbitrary clauses. Finally, it is generally nonfirstorderizable, relying on the notion of transitive closure of a relation. However, it can be expressed in FOL with a finite upper bound on the elements of the relation. This leads to a definition of vagueness in classical FOL, using the interplay between a total preorder and a monadic predicate. A notational extension of FOL will introduce a vague structure formed by the predicate (e.g.tall), the broad predicate (e.g. broadly tall) and the strict predicate (e.g. strictly tall). It allows the failure of a weak non-contradiction (e.g. ‘Some men are both broadly tall and broadly short’), the failure of a weak LEM (e.g. ‘Some men are neither strictly tall nor strictly short`), and the truth of a non-paradoxical tolerance (e.g. ‘If a person of n cm is strictly tall, a person of n-1 cm is broadly tall’).

References:

[1] P. Cobreros, P. Egré, D. Ripley, R, Van Rooij, Tolerant, Classical, Strict, Journal of Philosophical Logic 41 (2019), 347-385.

[2] D. Graff, Shifting Sands: An Interest-Relative Theory of Vagueness, Philosophical Topics 28 (2000), 45-81.

[3] U. Keller, Some remarks on the definability of transitive closure in first-order logic and Datalog, Internal report, Digital Enterprise Research Institute (DERI), University of Innsbruck, 2004.

[4] K.G. Lucey, he ancestral relation without classes, Notre Dame Journal of Formal Logic 20 (1979), 281-284.

### Thursday, December 12, 2019

** Ioana Leuștean (University of Bucharest)
Operational Semantics of Security Protocols II
**

### Thursday, November 21, 2019

** Ioana Leuștean (University of Bucharest)
Operational Semantics of Security Protocols
**

**Abstract**: After a brief overview of the formal methods used for analysing security protocols, we will focus on the operational semantics developped in [1].

References:

[1] C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Springer, 2012.

### Monday, November 4, 2019 at 09.00

** Andrei Sipoș (TU Darmstadt & IMAR)
Bounds on strong unicity for Chebyshev approximation with bounded coefficients
**

**Abstract**: In the early 1990s, Kohlenbach pursued a program of applying proof-theoretic techniques in order to obtain effective results in best approximation theory, specifically moduli of uniqueness and constants of strong unicity. This was part of a larger research program of Kreisel from the 1950s called ‘unwinding of proofs’, a program that aimed at applying proof transformations to potentially non-constructive proofs in ordinary mathematics in order to extract new information. The program was later developed by Kohlenbach and his students and collaborators under the name of ‘proof mining’, extending it to a variety of mathematical areas.

What we do is to build upon the work mentioned above in order to obtain a modulus of uniqueness for best uniform approximation with bounded coefficients, as first considered by Roulier and Taylor. The main novelty is the application of Schur polynomials to obtain useful explicit formulas for the interpolation results which are needed in the proof. We present ways these formulas may be bounded and how those bounds may in turn be used to derive and verify the desired modulus.

References:

[1] A. Sipoș, Bounds on strong unicity for Chebyshev approximation with bounded coefficients, arXiv:1904.10284 [math.CA], 2019.

### Thursday, October 24, 2019

**Alexandru Dragomir (University of Bucharest)
An introduction to BAN logic (a logic of authentication)
**

**Abstract**: One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic (Burrows, Abadi \& Needham 1989). BAN logic is a many-sorted modal logic used for its intuitive and compelling set of inference rules devised for reasoning about an agent’s beliefs, trust and message exchange. My presentation will focus on (1) presenting the language and inference rules of BAN logic, (2) following the original paper's analysis of the Otway-Rees protocol, (3) presenting some objections to using BAN, and (4) discussing the problem of offering a semantics of BAN logic.

### Thursday, September 19, 2019 in Hall 214

** Radu Iosif (CNRS - VERIMAG, France) )
Checking Deadlock Freedom of Component-based Systems
**

**Abstract**: We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g. rendez-vous, broadcast) and the topology (i.e. architecture) of the system (e.g. pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. We applied our technique to the verification of several textbook examples, such as dining philosophers, mutual exclusion protocols and concurrent systems with preemption and priorities.

Joint work with Marius Bozga and Joseph Sifakis.