Browsing by Author "Lidell, David"

Filter results by typing the first few letters
Now showing 1 - 4 of 4
  • No Thumbnail Available
    Item
    Automata Constructions for LTL with Past
    (Department of Computer Science and Engineering University of Gothenburg | Chalmers University of Technology, 2024) Lidell, David
    Linear temporal logic (LTL) is a popular language in formal verification, especially in the domains of model checking and reactive synthesis. Because its semantics is defined in terms of infinite sequences of symbols that can be interpreted as system variables, it is suitable for expressing how the state of a continuously operating system evolves over time. Due to the tight connection between the semantics of LTL and that of automata over infinite words, and because many common approaches to formal verification are automata-theoretic in nature, it is not surprising that various translations from LTL to automata over infinite words have been developed over the years, both for theoretical and practical purposes. Although many properties are naturally and succinctly expressed in terms of past events, the majority of these translations are restricted to formulae that only refer to the present and future. Those that do handle past are often indirect or lead to automata with an unnecessarily large number of states. In this thesis we present several translations from linear temporal logic with past to various types of automata over infinite words. We also suggest a framework for extending existing tools that are based on manipulating LTL formulae to handle past, together with a prototype tool intended to serve as a proof of this concept.
  • No Thumbnail Available
    Item
    Formalizing domain models of the typed and the untyped lambda calculus in Agda
    (2020-12-17) Lidell, David; Göteborgs universitet/Institutionen för data- och informationsteknik; University of Gothenburg/Department of Computer Science and Engineering
    We present a domain interpretation of the simply typed and the untyped lambda calculus. The interpretations are constructed using the notion of category with families, with added structure. Specifically, for the simply typed case we construct a simply typed category with families of (a version of) neighborhood systems with structures supporting binary product types and function types. For the untyped case, we construct a unityped category with families of neighborhood systems, with added lambda structure. The work is completely formalized in the dependently typed programming language and proof assistant Agda. The categories with families with added structure are formalized as records and then instantiated with neighborhood systems as objects and approximable mappings as morphisms. In constructing the appropriate neighborhood system for the untyped model, we make use of Agda’s sized types; this feature enables us to prove transitivity of the ordering relation between untyped neighborhoods.
  • No Thumbnail Available
    Item
    Gleasons sats
    (2019-06-26) Lidell, David; Karmstrand, Therese; Landgren, Lorents; Ulander, Johan; University of Gothenburg/Department of Mathematical Science; Göteborgs universitet/Institutionen för matematiska vetenskaper
    This paper aims to present Gleason’s theorem and a full proof, by the most elementary methods of analysis possible. Gleason’s theorem is an important theorem in the mathematical foundations of quantum mechanics. It characterizes measures on closed subspaces of separable Hilbert spaces of dimension at least 3. The theorem can be formulated in terms of so-called frame functions. It states that all bounded frame functions, on the specified Hilbert spaces, must have the form hAx, xi, for some self-adjoint operator A. The theorem is proved by first proving the statement in R3, through mostly geometric arguments on the unit sphere, and methods relating to convergence of sequences. It is then shown that this implies the theorem in general Hilbert spaces of higher dimension. The bulk of our proof follows the ideas of Cooke, Keane and Moran [2] with some own additions and clarifications in order to make it more accessible and correct. A lemma of single-variable analysis has been expanded, an oversight in the proof of the geometric lemma 5 (Piron) has been fixed and an erroneous topological argument has led to the much rewritten proposition 2 about extremal values of frame functions. The motivation for the sufficiency of the proof in R3 for higher-dimensional Hilbert spaces follows the ideas of the original proof by Andrew M. Gleason.
  • No Thumbnail Available
    Item
    ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae
    (2023) Azzopardi, Shaun; Lidell, David; Piterman, Nir; Schneider, Gerardo
    This paper presents ppLTLTT, a tool for translating pure-past linear temporal logic formulae into temporal testers in the form of automata. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such as LTL-to-automata translators and reactive synthesis tools, to support a richer input language. Namely, with ppLTLTT, tools that accept LTL input are also made to handle pure-past LTL as atomic formulae. While the addition of past operators does not increase the expressive power of LTL, it opens up the possibility of writing more intuitive and succinct specifications. We illustrate this intended use of ppLTLTT for Slugs, Strix, and Spot ’s command line tool LTL2TGBA by describing three corresponding wrapper tools pSlugs, pStrix, and pLTL2TGBA, that all leverage ppLTLTT. All three wrapper tools are designed to seamlessly fit this paradigm, by staying as close to the respective syntax of each underlying tool as possible.