Skip to content

Formalisation

Our paper on understanding the ADL of older adults has been published by IEEE Sensors

    Our paper describing “A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes” has been published by the journal  IEEE Sensors. This describes a novel approach and framework integrating symbolic modelling and data from sensors for understanding the Activities of Daily Living (ADLs) of older adults living independently in their homes in Edinburgh and its neighbourhood.

    The work is part of the Integrated Technologies of Care workpackage of the Advanced Care Research Centre (ACRC).

    Abstract:

    There is an urgent need to provide quality-of-life to a growing population of older adults living independently. Solutions that focus on the person and take into account their preferences and context are recognised as key. We introduce a framework for representing and reasoning about the Activities of Daily Living of older adults living independently at home. The framework integrates data from sensors and data from participants derived from semi-structured interviews, home layouts and additional contextual information, such as the researchers’ observations. These data are used to create formal models, personalised for each participant according to their preferences and context. Requirements specific to each individual are formulated and encoded in Linear Temporal Logic, and a model checker is used to verify whether each is satisfied by the model of the participant’s behaviour. We demonstrate the framework’s generalisability by applying it to two different participants, highlighting its potential to enhance the safety and well-being of older adults ageing in place.
    Print ISSN: 1530-437X
    Online ISSN: 1558-1748
    DOI: 10.1109/JSEN.2025.3635781
    More information available here.

    Our paper on differentiable Signal Temporal Logic for neurosymbolic AI has been published by LIPIcs

      GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning

      Authors Mark Chevallier , Filip Smola , Richard Schmoetten , Jacques D. Fleuriot 

      Part of: Volume: 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)
      Series: Leibniz International Proceedings in Informatics (LIPIcs)
      Conference: International Symposium on Temporal Representation and Reasoning (TIME)

      Our formalisation of Linear Resources and Process Compositions has been published in the Archive of Formal Proof

        Abstract

        In this entry we formalise a framework for process composition based on actions that are specified by their input and output resources. We verify their correctness by translating compositions of process into deductions of intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction.

        We describe an earlier version of this formalisation in our article Linear Resources in Isabelle/HOL, which also includes a formalisation of manufacturing processes in the simulation game Factorio.

        Our formalisation of Lie Groups and Algebras has been published in the Archive of Formal Proof

          Abstract

          Lie Groups are formalised as locales, building on the AFP theory of Smooth Manifolds. We formalise the diffeomorphism group of a manifold, and the action of a Lie group on a manifold. The general linear group is shown to be a Lie group by proving properties of the determinant, and matrix inverses. We also develop a theory of smooth vector fields on a manifold , defined as smooth maps from the manifold to its tangent bundle . We employ a shortcut that avoids difficulties in defining the tangent bundle as a manifold, but which still leads to vector fields with the properties one would expect. We then construct the Lie algebra of a Lie group as an algebra of left-invariant smooth vector fields.

          Schmoetten R. and Fleuriot J. D. (2024). Lie Groups and Algebras. Archive of Formal Proofs. ISSN: 2150-914x.

          Our paper “Linear Resources in Isabelle/HOL” has just been published in the Journal of Automated Reasoning

            Abstract:

            We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of these compositions is verified by translating them into deductions in intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction when satisfied. We mechanise the whole framework, including a deep embedding of ILL, in the proof assistant Isabelle/HOL. Beyond the increased confidence in our proofs, this allows us to automatically generate executable code for our verified definitions. We demonstrate our approach by formalising part of the simulation game Factorio and modelling a manufacturing process in it. Our framework guarantees that this model is free of bottlenecks.

            Smola, F., Fleuriot, J.D. Linear Resources in Isabelle/HOL. J Autom Reasoning 68, 9 (2024). https://doi.org/10.1007/s10817-024-09698-2