# Seminar

The seminar generally takes places on Tuesday morning. To keep informed you can

## Point de vue de Connes et Consani sur la fonction zêta de Riemann

**Aurélien Sagnier**(Cosynus)

Tuesday 21 November 2017 at 10:30, room Philippe Flajolet

Nous sommes tous habitués à voir les entiers relatifs comme munis de la structure $(\mathbb{Z},+,\times,\leq)$, i.e., une structure d’anneau ordonné, mais il serait possible de les regarder autrement en « changeant l’ordre » des opérations. Plus précisément on peut munir les entiers de la structure suivante $(\mathbb{Z},\max,+)\circlearrowleft\mathbb{N}^\star$, c’est-à-dire un semi-anneau idemptotent avec une action par multiplication (usuelle) des éléments de $\mathbb{N}^\times$, Connes et Consani ont découvert en 2014 qu’on peut « voir » les entiers munis de la structure précédente avec les yeux de la géométrie algébrique comme un espace dont les points sont reliés aux zéros de la fonction zêta de Riemann or en géométrie algébrique pour certaines variétés définies sur des corps finis, l’analogue de l’hypothèse de Riemann a été démontré. Le but est alors d’essayer de transposer la stratégie de la preuve de la conjecture de Riemann pour les fonction zêta associées aux variétés définies sur des corps finis à la fonction zêta de Riemann.

## Dual space of a lattice as the completion of a Pervin space

**Jean-Eric Pin**(IRIF)

Friday 30 June 2017 at 11:00, room TBA

In this survey lecture, I will mainly cover well-known results from a new angle. A Pervin space is simply a set equipped with a lattice of subsets. This notion suffices to define a natural notion of completion which appears to be the dual of the original lattice. One can then show that any lattice of subsets can be described by a set of inequations of the form u≤v, where u and v are elements of its dual space. Applications to formal languages and complexity classes will be given.

## Control synthesis of nonlinear sampled switched systems using Euler's method

**Adrien Le Coënt**(ENS Paris-Saclay)

Friday 14 April 2017 at 11:00, room Philippe Flajolet

We propose a symbolic control synthesis method for nonlinear sampled switched systems whose vector fields are one-sided Lipschitz. The main idea is to use an approximate model obtained from the forward Euler method to build a guaranteed control. The benefit of this method is that the error introduced by symbolic modeling is bounded by choosing suitable time and space discretizations. The method is implemented in the interpreted language Octave. Several examples of the literature are performed and the results are compared with results obtained with a previous method based on the Runge-Kutta integration method.

## Relation Lifting

**Alexander Kurz**(University of Leicester)

Monday 27 March 2017 at 15:30, room Marcel-Paul Schützenberger

Going back to work by Barr in the 1970ies, the question of how to extend constructions given in terms of maps to constructions given in terms of relations has received considerable attention. For example, in the semantics of programming languages this question is of fundamental importance if programs are abstracted as maps and specifications as relations. We will review the well-known result characterising liftings of functors from sets and maps to sets and relations and then generalise it from sets to partial orders and to metric spaces. Applications to process algebra, modal logic and domain theory will be discussed. The material presented will be based on the work of, amongst others, Barr, Hermida, Jacobs, Levy, Marti, Venema as well as on joint work with my coauthors Bilkova, Jung, Moshier, Petrisan, Velebil.

## Semirings, semimodules, and star-continuity

**Uli Fahrenberg**(LIX)

Wednesday 22 March 2017 at 14:00, room Philippe Flajolet

Semirings are algebraic structures which abound in computer science. Motivated by applications in automata theory, semirings with iteration structures (star semirings, Conway semirings, star-continuous Kleene algebras) have seen extensive development since the 50ies. In order to handle infinite runs, Bloom, Ésik, Kuich and others have developed the algebraic setting of semiring-semimodule pairs with infinite products, with applications in Büchi automata, energy problems and other areas. I will give a gentle introduction to the above algebraic setting, with plenty of motivation and examples. Afterwards, I will give an exposition of recent work on star-continuous Kleene ω-algebras which I have done with the late Zoltán Ésik, including its application to energy problems.

## When Are Prime Formulae Characteristic?

**Ignacio Fábregas**(Reykjavik University)

Monday 13 March 2017 at 15:30, room Grace Hopper

In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to the logics characterizing all the semantics in van Glabbeek’s branching-time spectrum.

## A cartesian-closed category for higher-order model checking

**Jérémy Ledent**(LIX)

Tuesday 28 February 2017 at 10:30, room Philippe Flajolet

In previous work, Martin Hofmann and Wei Chen have described the construction of an abstract lattice from a given Büchi automaton. This abstract lattice is finite and is related by a Galois insertion to the lattice of languages of finite and infinite words. This allows one to decide whether finite and infinite traces of (sequential) non-deterministic first-order recursive programs are accepted by the automaton. In this talk I will show how to extend this work to higher-order programs. This involves the construction of a cartesian-closed category with a fixpoint operator, such that the interpretation of a higher-order recursive program yields precisely the abstraction of its set of finite and infinite traces. This provides an algorithm for the higher-order model checking problem for trace properties by computing the interpretation of a program in this category. It was already known (Ong & Kobayashi) that this higher-order model checking problem is decidable, but all previous algorithms work inherently on tree properties, even when we are only interested in trace properties. This algorithm is considerably simpler since it focuses on trace properties.

## Sculptures for Higher Dimensional Automata

**Christian Johansen**(University of Oslo)

Thursday 12 January 2017 at 15:00, room Philippe Flajolet

This talk will explain Higher Dimensional Automata (HDA) model of concurrency emphasising the fact that events/activities have duration. My view of HDAs is more from a CS point of view, than geometrical, and thus I explain how transitions are now first class citizens, the same as nodes are in standard FSM. Finite state machines are the models on which standard modal logics are interpreted, i.e., in states, which contain propositional formulas, whereas the modalities move on transitions from state to state. In comparison, I will present how Higher Dimensional Modal Logic (HDML) is a natural extension of modal logic to consider the transitions as first class citizens and also to consider the concurrency. I will try to explain the attempt at proving the completeness of HDML over HDAs. Difficulty of obtaining the completeness of HDML may be because HDML is close to the ST structures, which are the natural extension of the configuration structures of van Glabbeek and Plotkin by considering the transitions as first class citizens, i.e., the notion of “during” is made explicit. My results suggest that ST structures do not capture all HDAs, but capture only Sculptures. Sculptures are strange, elusive, since they want to capture the intuition given by Pratt about how to build HDAs, but do not capture full HDAs. This brings now the discussion that maybe this is why the completeness of HDML fails. Thus, if we pin point where the sculptures sit wrt. HDAs, we may be able to understand where the completeness fails for HDML. Note that this talk will be given in a manner understandable also for non-experts in HDA or in HDML. Though some familiarity with modal logics or with event-based models of concurrency would help.

## Complexes de parité et pasting schemes

**Simon Forest**(ENS)

Wednesday 19 October 2016 at 14:00, room Philippe Flajolet

Les ∞-catégories sont une généralisation des catégories où il y a non seulement des morphismes entre objets, mais plus généralement des (n+1)-morphismes entre n-morphismes. Ces catégories généralisées doivent vérifier plusieurs axiomes, notamment l’associativité de la composition ainsi que la loi d’échange. Ces axiomes rendent la représentation de morphismes sous la forme de formules de composition assez maladroite pour plusieurs raisons. D’abord car les formules deviennent rapidement très lourdes et peu intuitives. Mais aussi car les axiomes des ∞-catégories rendent la classe d’équivalence d’une formule difficile à décrire, ce qui en pratique empêche de choisir une formule canonique par morphisme ou de décider facilement de l’égalité de deux formules. Dans ce cadre, Street et Johnson ont introduit des théories permettant de représenter une certaine classe de ∞-catégories à l’aide de structures basées sur des ensembles. Ces structures permettent de représenter chaque morphisme par un élément unique (donc canonique) et fournissent donc une façon plus commode de représenter les morphismes que les formules de composition. Dans cet exposé, on essayera de mieux comprendre ces deux structures et de les comparer. À partir de cette analyse, on donnera une généralisation axiomatiquement plus simple et qui permet de représenter plus de cas.

## A type theory for weak ω-categories

**Eric Finster**(LIX)

Sunday 4 September 2016 at 11:00, room Marcel-Paul Schützenberger

## An Overview of the Sheaf-theoretic Approach to Contextuality

**Shane Mansfield**(IRIF)

Monday 23 May 2016 at 13:30, room Philippe Flajolet

Contextuality is a key feature which distinguishes super-classical (e.g. quantum) correlations from classical ones. In the quantum setting it is the subject of celebrated no-go theorems of Bell, Kochen-Specker, and others. We will also mention recent results suggesting that it is the essential ingredient for enabling quantum advantages over classical computing in various settings. The language of sheaf theory and algebraic topology provides a powerful, general setting in which to treat contextuality. In this talk we will present an overview of the approach. We will see that empirical data can be represented as a compatible family of sections in a certain presheaf of probability distributions, and that contextuality is characterised by the absence of any global section which recovers the empirical data by restriction. The perspective uncovers a rich hierarchy of qualitatively different levels of contextuality, leads to a cohomological characterisation of certain kinds of contextuality, and to a geometric understanding of empirical models over fixed scenarios which enables quantification of contextuality via simple linear programs.

## Consensensus asymptotique dans un réseau dynamique

**Bernadette Charron-Bost**(LIX)

Tuesday 3 May 2016 at 11:00, room Emmy Noether

## Reachability in Space-Time for Piecewise Affine Dynamics

**Goran Frehse**(Verimag)

Thursday 3 March 2016 at 10:30, room Grace Hopper

In set-based reachability, a cover of the reachable states of a hybrid system is obtained by repeatedly computing one-step successor states. It can be used to show safety or to obtain quantitative information, e.g., for finding bounds on the jitter in an oscillator circuit. In general, one-step successors can only be computed approximately and are difficult to scale in the number of continuous variables. The approximation error requires particular attention since it can accumulate rapidly, leading to a coarse cover, prohibitive state explosion, or preventing termination. We present an approach with precise control over the balance between approximation error and scalability. By lazy evaluation of abstract set representations, the precision can be increased in a targeted manner, e.g., to show that a particular transition is spurious. Each evaluation step scales well in the number of continuous variables. The set representations are particularly suited for clustering and containment checking, which are essential for reducing the state explosion. This provides the building blocks for refining the cover of the reachable set just enough to show a property of interest. The approach is illustrated on several examples.

## A Topological Method for Finding Invariant Sets of Switched Systems

**Sameh Mohamed**(LIX, École Polytechnique)

Monday 15 February 2016 at 10:30, room Philippe Flajolet

We revisit the problem of finding invariants sets, or more generally speaking, viability kernels, for a class of differential inclusions, using topological methods based on Wazewski property. In many ways, this generalizes the Viability Theorem approach, which is itself a generalization of the Lyapunov function approach for systems described by ordinary differential equations. We give a computable criterion based on SOS methods for a class of differential inclusions to have a non-empty viability kernel within some given region. We use this method to prove the existence of invariant sets of switched systems inside a region described by a polynomial template, both with time-dependent switching and with state-based switching through a finite set of hypersurfaces.

## Itérations sur les politiques pour les systèmes affines par morceaux

**Assalé Adjé**(IRIT)

Tuesday 12 January 2016 at 10:30, room Marcel-Paul Schützenberger

Dans cette présentation, je montrerai comment utiliser la théorie des fonctions de Lyapunov quadratiques par morceaux pour calculer automatiquement des bornes sur les valeurs atteignables d’un système dynamique affine par morceaux à temps discret. Dans un deuxième temps, je développerai une méthode d’itérations sur les politiques pour obtenir une surapproximation plus précise des ensembles des valeurs atteignables.

## Partial Higher-Dimensional Automata, Bisimilarity, and Natural Homology

**Ulrich Fahrenberg**(IRISA Rennes)

Thursday 26 November 2015 at 10:00, room Philippe Flajolet

We propose a generalization of higher-dimensional automata, partial HDA. Unlike HDA, and also extending event structures and Petri nets, partial HDA can model phenomena such as priorities or the disabling of an event by another event. Using open maps and unfoldings, we introduce a natural notion of (higher-dimensional) bisimilarity for partial HDA and relate it to history-preserving bisimilarity and split bisimilarity. Higher-dimensional bisimilarity has a game characterization and is decidable in polynomial time. We also explore the relationship between bisimilarity of (partial) HDA and bisimilarity in natural homology.

## Interacting Hopf Algebras - an axiomatisation of linear systems

**Fabio Zanassi**(ENS Lyon)

Monday 23 November 2015 at 14:00, room Philippe Flajolet

We present by generators and equations the theory IH whose free model is the category of linear subspaces over a field k. Terms of IH are string diagrams which, for different choices of k, express different kinds of networks and graphical formalisms used by scientists in various fields, such as categorical quantum mechanics, concurrency and control theory. The equations of IH arise by distributive laws between PROPs of Hopf algebras – from which the name “Interacting Hopf algebras”. The characterisation in terms of subspaces allows to think of IH as a string diagrammatic syntax for linear algebra: linear maps, spaces and their transformations are all faithfully represented in the graphical language, resulting in an alternative, often insightful perspective on the subject matter. As main application, we use IH to axiomatise a formal semantics of signal processing circuits, for which we study full abstraction and realisability. Our analysis suggests a reflection about the role of causality in the semantics of computing devices. This is a joint work with Filippo Bonchi and Pawel Sobocinski.

## Order-Theoretic, Geometric and Combinatorial Models of Intuitionistic S4 Proofs

**Jean Goubault-Larrecq**(LSV, ENS Cachan)

Monday 14 September 2015 at 14:00, room Philippe Flajolet

We propose a few models of proof terms for the intuitionistic modal propositional logic S4. Some of them are based on partial orders, or cpos, or dcpos, some of them on a suitable category of topological spaces and continuous maps. A structure that emerges from these interpretations is that of augmented simplicial sets. This leads to so-called combinatorial models, where simplices play an important role: the point is that the simplicial structure interprets the □ modality, and that the category of augmented simplicial sets is itself already a model of intuitionistic propositional S4 proof terms. In fact, this category is an elementary topos, and is therefore a prime candidate to interpret all proof terms for intuitionistic S4 set theory. Finally, we suggest that geometric-like realizations functors provide a recipe to build other models of intuitionistic propositional S4 proof terms.

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Tuesday 8 September 2015 at 10:00, room Robin Milner

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Thursday 3 September 2015 at 14:00, room Philippe Flajolet

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Thursday 3 September 2015 at 14:00, room Philippe Flajolet

## An introduction to Homotopy Type Theory

**Assia Mahboubi**(LIX, École Polytechnique)

Wednesday 8 July 2015 at 14:00, room Philippe Flajolet

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Wednesday 17 June 2015 at 14:00, room Marcel-Paul Schützenberger

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Wednesday 3 June 2015 at 14:00, room Philippe Flajolet

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Wednesday 20 May 2015 at 14:00, room Philippe Flajolet

## A cubical evaluation model for Type Theory

**Cyril Cohen**(Inria Sophia Antipolis)

Tuesday 21 April 2015 at 10:30, room Philippe Flajolet

The connection between Type Theory and Homotopy Theory as described by Vladimir Voevodsky’s simplicial set model of type theory does not explain the computational behaviour of the univalence axiom. I will introduce cubical sets with connections and explain why they form a model of type theory that we could use to compute with univalence. The talk will consist of chosen bits from Thierry Coquand’s lectures notes. This new type theory has an ongoing implementation in Haskell.

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Friday 3 April 2015 at 10:30, room Marcel-Paul Schützenberger

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Tuesday 24 March 2015 at 13:30, room Philippe Flajolet

## Programming with Numerical Uncertainties

**Eva Darulova**(EPFL)

Monday 23 March 2015 at 13:30, room Marcel-Paul Schützenberger

Numerical software, common in scientific computing or embedded systems, inevitably uses an approximation of the real arithmetic in which most algorithms are designed. Finite-precision arithmetic, such as fixed-point or floating-point, is a common and efficient choice, but introduces an uncertainty on the computed result that is often very hard to quantify. We need adequate tools to estimate the errors introduced in order to choose suitable approximations which satisfy the accuracy requirements. I will present a new programming model where the scientist writes his or her numerical program in a real-valued specification language with explicit error annotations. It is then the task of our verifying compiler to select a suitable floating-point or fixed-point data type which guarantees the needed accuracy. I will show how a combination of SMT theorem proving, interval and affine arithmetic and function derivatives yields an accurate, sound and automated error estimation which can handle nonlinearity, discontinuities and certain classes of loops. We have further combined our error computation with genetic programming to not only verify but also improve accuracy. Finally, together with techniques from validated numerics we developed a runtime technique to certify solutions of nonlinear systems of equations, quantifying truncation in addition to roundoff errors.

## Functors are Type Refinement Systems

**Noam Zeilberger**(Mathematical Components group, MSR-INRIA Joint Centre)

Thursday 12 February 2015 at 14:00, room Philipppe Flajolet

There is a standard dogma about how to read type theory through the lens of category theory, based on the idea of viewing a type system as a category of well-typed terms. In a long-running project with Paul-André Melliès, at some point we realized that it is better to view a type system as a *functor* from a category of typing derivations to a category of underlying terms, and indeed that this can even serve as a working *definition* of “type system” (or what we now call a “refinement system”), as being (in the most general case) simply an arbitrary functor.

In the talk I want to motivate and introduce this general framework, which was described in our paper at POPL 2015^{1}. If time permits, I might also outline some more technical results from a recent draft^{2}, related to the “fundamental embedding” of any refinement system into the refinement system of presheaves over categories.

## Presenting Categories Modulo a Rewriting System

**Florence Clerc**(CEA, LIST / PPS, Université Paris 7)

Thursday 29 January 2015 at 14:00, room Marcel-Paul Schützenberger

Presentations of categories are a well-known algebraic tool to provide descriptions of categories by the means of generators, for objects and morphisms, and relations on morphisms. We generalize here this notion, in order to consider situations where the objects are considered modulo an equivalence relation (in the spirit of rewriting modulo), which is described by equational generators. When those form a convergent (abstract) rewriting system on objects, there are three very natural constructions that can be used to define the category which is described by the presentation: one is based on restricting to objects which are normal forms, one consists in turning equational generators into identities (i.e. considering a quotient category), and one consists in formally adding inverses to equational generators (i.e. localizing the category). We show that, under suitable assumptions on the presentation, the three constructions coincide, thus generalizing celebrated results on presentations of groups. We illustrate our techniques on a non-trivial example, and hint at a generalization for 2-categories.

## Directed homology

**Jérémy Dubut**(École Normale Supérieure de Cachan)

Tuesday 9 December 2014 at 10:00, room Philipppe Flajolet

The purpose of directed algebraic topology is to study systems in which we have a notion of direction, order, time, in exploring their geometry. A quite natural use (which historically motivated the field in the 90s) is the study of truly concurrent systems, in particular higher dimension automata, introduced by Pratt in 1991. If the theory of directed homotopy (analogue of classical theory of homotopy in a directed setting) is well developed, it lacks of a satisfactory notion of directed homology. We propose in this talk a candidate matching some criteria: invariance by actions refinement, modularity, precision and computability in a finite, loop-free case.

## Computational Complexity of the GPAC

**Amaury Pouly**(LIX, École Polytechnique)

Tuesday 2 December 2014 at 10:00, room Philipppe Flajolet

In 1941, Claude Shannon introduced a model for the Differential Analyzer, called the General Purpose Analog Computer (GPAC). Originally it was presented as a model based on circuits, where several units performing basic operations (e.g. sums, integration) are interconnected. However, Shannon itself realized that functions computed by a GPAC are nothing more than solutions of a special class of differential equations of the form y’=p(y) where p is a (vector of) polynomial. Analog computer have since been replace by digital counterpart. Nevertheless, once can wonder whether the GPAC could in theory have super-Turing computable power. A few years ago, it was shown that Turing-based paradigm and the GPAC have the same computational power. So, switching to analog computers would not enable us to solve the Halting problem, or any uncomputable exotic thing, but we can nonetheless compute everything a Turing machine does (given enough resources), and a return to analog technology would at least not mean a loss of computational power. However, this result did not shed any light on what happens at a computational complexity level: can an analog computer (GPAC) solve a problem faster (modulo polynomial reductions) than a digital computer (Turing machine)? I will provide some elements which show that some reasonable restrictions of the GPAC are actually equivalent to P (polynomial time) and going even further, that we can show an equivalence with the polynomial of computable analysis. This gives an elegant, analog definition for polynomial time computable functions over real numbers.

## Double Glueing and Models of Linear Logic

**Hugh Steele**(LIPN, Université Paris 13)

Thursday 27 November 2014 at 10:00, room Philipppe Flajolet

Many full completeness theorems have been established for fragments of linear logic since the notion was first defined by Samson Abramsky and Radha Jagadeesan in their 1992 paper. For the most part, these results are obtained on a case-by-case basis: the subject of each proof is precisely one category. In this talk it is shown that certain double glueing constructions can transform tensor-generated compact closed categories with finite biproducts into stronger models of linear logic. By creating a “glueing” over homfunctors and using only standard linear algebra, we show that every such category can act as the basis of a fully complete model of unit-free MLL. We also discuss how the category of hypercoherence spaces can also be seen as a double-glued category, and that the associated construction may be generalised to help create a family of accurate unit-free MALL models.

## Opetopic Diagrams as a Language for Higher Categorical Proofs

**Éric Finster**(EPFL)

Friday 21 November 2014 at 10:00, room Philipppe Flajolet

Recent advances in type theory have demonstrated interesting new links between formal languages, formal proof assistants and ideas from higher category theory. The identity types of Martin-Lof type theory give us a systematic logical formalism for reasoning synthetically about weak infinity groupoids, or equivalently, homotopy types. On the other hand, the problem of applying these ideas to higher categories, in place of higher groupoids, remains open. Here I will demonstrate a prototype proof assistant for higher category theory based on the opetopic model of higher categories. The proof assistant employs a diagrammatic syntax based on the opetopic diagrams of Joyal, Kock, Batanin and Mascari and implements a definition of opetopic higher category due to Thorsten Palm.

## Linear numeral systems

**Ian Mackie**(LIX, École Polytechnique)

Tuesday 18 November 2014 at 10:00, room Philipppe Flajolet

We take a fresh look at an old problem of representing natural numbers in the λ-calculus. Our interest is in finding representations where we can compute efficiently (and where possible, in constant time) the following functions: successor, predecessor, addition, subtraction and test for zero. Surprisingly, we find a solution in the linear λ-calculus, where copying and erasing are not permitted.

## Cohomological invariants for complexity?

**Thomas Seiller**(IHES)

Thursday 13 November 2014 at 10:00, room Philipppe Flajolet

This talk will be about recent results at the intersection of complexity theory and logic. In the last decade, several logical systems that characterize complexity classes appeared, some of them defined as variants of Girard’s linear logic – constrained linear logic systems. Studying mathematical models of linear logic and its constrained variants, we can show a correspondance between a hierarchy of complexity classes and a hierarchy of mathematical objects called graphings. This result enables the use of new techniques and invariants, such as cohomological invariants for graphings, in complexity theory.

## dTL2: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems

**Jean-Baptiste Jeannin**(Carnegie Mellon University)

Tuesday 4 November 2014 at 10:00, room Philipppe Flajolet

Differential Dynamic Logic can express important properties about Cyber-Physical Systems, by combining discrete assignments and control structures with differential equations. However it can only express properties about the end state of a system. In this talk, we introduce the differential temporal dynamic logic dTL2, a logic to specify properties about the intermediate states reached by a hybrid system. It combines differential dynamic logic with temporal logic, and supports some linear time temporal properties of LTL. It extends differential temporal dynamic logic dTL with nested temporalities. We provide a semantics and a proof system for the logic dTL2, and show its usefulness for nontrivial temporal properties of hybrid systems. We take particular care to handle the case of alternating universal dynamic and existential temporal modalities and its dual, solving an open problem formulated in previous work.