Contributed Talks 9
Chair: Valentin Goranko
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
| 14:00 |
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. Bibliography
|
|
| 14:25 |
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. Bibliography
|
|
| 14:50 |
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. |
|
| 15:15 |
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. Bibliography
|
|
| 15:40 |
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. Bibliography
|