Logic Colloquium 2024

Contributed Talk

Contributed Talks 9

Chair: Valentin Goranko

  Wednesday, 14:00, J336 ! Live

Time allocation: 20 minutes per speaker; 5 minutes for each changeover

Talks in this session


Brett McLean, Bi-intuitionistic linear temporal logic

Authors: David Fernández-Duque, Brett McLean and Lukas Zenger

We investigate an intuitionistic propositional logic extended with both the co-implica-tion connective of Hilbert–Brouwer logic and with the modalities of linear temporal logic. We use a semantics based on intuitionistic Kripke frames equipped with an order-preserving function representing the temporal dynamics. By using the technical notion of a quasimodel, a type of nondeterministic encoding of a linear-time model, first introduced in [1], we establish the decidability of our bi-intuitionistic linear temporal logic and give a sound and complete Hilbert-style calculus for it. This work builds on that of [2], where the decidability of various bi-intuitionistic modal logics was established.


  1. David Fern’andez-Duque,Non-deterministic semantics for dynamic topological logic,Annals of Pure and Applied Logic,vol. 157 (2009), no. 2–3, pp. 110–121.
  2. David Fern’andez-Duque, Brett McLean, and Lukas Zenger,A family of decidable bi-intuitionistic modal logics,proceedings of Principles of Knowledge Representation and Reasoning (KR)(Rhodes, Greece),(Pierre Marquis, Tran Cao Son, and Gabriele Kern-Isberner, editors),vol. 20,IJCAI Organization,2023,pp. 262–271.
  3. Cecylia Rauszer,Semi-boolean algebras and their applications to intuitionistic logic with dual operations,Fundamenta Mathematicae, vol. 83 (1974) no. 3, pp. 219–249.

Giovanni Varricchione, Pure-Past Action Masking: constraining Reinforcement Learning via pure-past LTL

Authors: Giovanni Varricchione, Natasha Alechina, Mehdi Dastani, Giuseppe De Giacomo, Brian Logan and Giuseppe Perelli

We present Pure-Past Action Masking (PPAM), a lightweight approach to action masking for reinforcement learning (RL). In PPAM, actions are disallowed (“masked”) according to specifications expressed in Pure-Past Linear Temporal Logic (PPLTL) [3]. PPAM can enforce non-Markovian constraints, i.e., constraints based on the history of the system, rather than just the current state of the environment. The features used in the safety constraint need not be the same as those used by the learning agent, allowing a clear separation of concerns between the safety constraints and reward specifications of the (learning) agent.

Via [4], we prove formally that PPAM is as expressive as shields [1], another approach to enforce non-Markovian constraints in RL. Then, thanks to a result from [2], we show that PPAM incur a single exponential blowup, instead of the double exponential one of shields.


  1. Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu,Safe reinforcement learning via shielding,Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence(New Orleans, Louisiana, USA),(Sheila McIlraith, and Kilian Weirberger editors),vol. 32,AAAI Press,2018,pp. 2669–2678.
  2. Luigi Bonassi, Giuseppe De Giacomo, Marco Favorito, Francesco Fuggitti, Alfonso Emilio Gerevini and Enrico Scala,Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic,Proceedings of the Thirty-Third International Conference on Automated Planning and Scheduling(Prague, Czech Republic),(Sven Koenig, Roni Stern, and Mauro Vallati editors),vol. 33,AAAI Press,2023,pp. 61-69.
  3. Orna Lichtenstein, Amir Pnueli, and Lenore Zuck,The glory of the past,Logics of Programs(Brooklyn, NY, USA),(Rohit Parikh editor),vol. 193,Springer Berlin Heidelberg,1985,pp. 196–218.
  4. Lenore Zuck,Past temporal logic,PhD thesis,The Weizmann Institute of Science,1986.

Ren-June Wang, Cutfree calculi for modal logics with axiom B or 5

In the study of modal logic, the modal logics in which the axioms \(\mathbf{B}\) and \(\mathbf{5}\) are theorems are difficult to find their proof systems with structural properties such as cut elimination for Gentzen style sequent calculus. From semantic point of view, these logics correspond to the symmetric and euclidean possible world semantics, and reversable and mergeable path models. In the previous work, we have introduced path models and proved the completeness theorem between some classes of this type of models with their corresponding cutfree calculi of sequences of sequents for normal modal logics with axioms \(\mathbf{D}\), \(\mathbf{T}\), or \(\mathbf{4}\). In this current project, we are going to continue our earlier work to prove the completeness theorem between path models – reversable or mergeable – on one side, and their corresponding cutfree calculi of sequences of sequents for normal modal logics with axiom \(\mathbf{B}\), or \(\mathbf{5}\) on the other.


Max Sandström, Comparison of hyperextensions of linear temporal logic

Linear temporal logic (LTL) is a modal logic with the modalities ‘Next Step’, ‘Until’ and ‘Always Going to Be’, and with linear orders as models, which are often called traces. LTL has the expressive power to capture some properties of computation traces, but not all the properties of interest. One class of properties beyond the scope of the logic is characterised by the existence of dependencies between traces. Properties of this kind are referred to as hyperproperties [1]. In this talk we compare the expressive power of two approaches to extending LTL in order to capture hyperproperties. We explore the relation between LTL under team semantics (TeamLTL) and LTL extended with trace quantifiers (HyperLTL), with a focus on the effects of extending the logics with arbitrary disjunctions and negations has on the relative expressivity. In the team semantics setting synchronicity brings with it great expressive power, making the logic incomparable to HyperLTL, whereas without the requirement of synchronicity the logic remains on the level of LTL [2]. Extending the asynchronous logic with connectives familiar from the team semantics literature, namely the Boolean disjunction and Boolean negation, widens what can be characterised in the logic, but how does the relation to HyperLTL fare in these extensions?

We will provide an overview of the results for the synchronous semantics of TeamLTL, while elaborating further on our recent work [3] with the asynchronous semantics of TeamLTL. In that domain we particularly consider the extensions of TeamLTL with the Boolean disjunction and a so-called left-downward closed fragment of the extension of TeamLTL with the Boolean negation, where the negation cannot occur in the left-hand side of the ‘Until’-operator or within the scope of the ‘Always Going to Be’-operator. We show that TeamLTL extended with the Boolean disjunction is equi-expressive with the positive Boolean closure of HyperLTL restricted to one universal quantifier, while the left-downward closed fragment of TeamLTL extended with the Boolean negation is expressively equivalent with the Boolean closure of HyperLTL restricted to one universal quantifier.

This talk is based on joint work with Juha Kontinen and Jonni Virtema.


  1. Michael R. Clarkson and Fred B. Schneider, Hyperproperties, Journal of Computer Security, vol. 18 (2010), no. 6, pp. 1157–1210.
  2. Andreas Krebs and Arne Meier and Jonni Virtema and Martin Zimmermann, Team Semantics for the Specification and Verification of Hyperproperties, 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018 (Liverpool, UK), (Igor Potapov and Paul G. Spirakis and James Worrell, editors), vol. 117, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, pp. 10:1–10:16.
  3. Juha Kontinen and Max Sandström and Jonni Virtema, Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023 (Bordeaux, France), (Jérôme Leroux and Sylvain Lombardy and David Peleg, editors), vol. 272, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, pp. 60:1–60:14.

Mattia Guiotto, Expressiveness issues in interval temporal logics

Authors: Dario Della Monica and Mattia Guiotto

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities [1]. One of the most studied interval temporal logics is Halpern and Shoham’s Modal Logic of Time Intervals (\hs, for short) [2], which features 12 modal operators, one for each binary relation between intervals over linear orders, known as Allen’s relations [3]. It was proved that the satisfiability of \hs formulae is highly undecidable, which motivated the search for syntactic fragments of \hs offering a good balance between expressiveness and computational complexity. Each subset of modal operators gives rise to a syntactically different \hs fragment. Due to the possibility of defining modal operators in terms of others, not all \hs fragments are expressively different. We consider the problem of obtaining a complete classification of the relative expressive power of all \hs fragments over the class of all discrete and the one of all finite linear orders. An almost complete picture has been obtained [4], with a unique, difficult problem being still open. The missing tile of the expressiveness puzzle is that of the definabilities for the modal operator of \hs corresponding to the Allen relation overlaps. The aim of our work is to complete the picture by filling the remaining gap. More precisely, we conjecture that the set of known definabilities for the \hs modal operator corresponding to the relation overlaps is complete for the class of all discrete linear orders. Proving such a conclusion requires the support of an important classic theoretical result, known as the bisimulation invariance property for modal formulae which is at the basis of undefinability results for modal logics [5]. We provide a proposal for a bisimulation construction, and give strong and convincing evidence to support its correctness. A complete formal proof is quite technically involved and tedious, and requires a meticulous case-by-case analysis. We managed to give a partial formal proof by completing one of the most difficult cases [6]. In conclusion, the work done paves the way towards the closure of the long-standing open issue of obtaining a complete expressiveness picture of the family of \hs fragments over the class of all discrete and the one of all finite linear orders.


  1. Ben C. Moszkowski and Zohar Manna,Reasoning in Interval Temporal Logic,Logics of Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings(Edmund M. Clarke and Dexter Kozen),vol. 164,Springer,1983,pp. 371–382.
  2. Halpern, Joseph Y and Shoham, Yoav,A propositional modal logic of time intervals,Journal of the ACM (JACM),vol. 38 (1991), no. 4, pp. 935–962.
  3. Allen, James F,Maintaining knowledge about temporal intervals,Communications of the ACM,vol. 26 (1983), no. 11, pp. 832–843.
  4. Luca Aceto, Dario Della Monica, Anna Ing’olfsd’ottir, Angelo Montanari, and Guido Sciavicco,On the expressiveness of the interval logic of {A}llen’s relations over finite and discrete linear orders,Proc. of the 14th European Conference on Logics in Artificial Intelligence (JELIA),vol. 8761,2014,pp. 267–281.
  5. Goranko, Valentin and Otto, Martin,Handbook of modal logic,Model Theory of Modal LogicAmsterdam, The Netherlands: Elsevier,2006,pp. 255–325.
  6. Mattia Guiotto,Expressiveness issues in Interval Temporal Logic,[Bachelor’s Thesis],University of Udine,2023.https://drive.google.com/file/d/1m6fwreCJg8AUhatlvd9nAiTp96WHD7NX/view?usp=drive_link

 Overview  Program