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.