-
Formal Simulation and Visualisation of Hybrid Programs
Authors:
Pedro Mendes,
Ricardo Correia,
Renato Neves,
José Proença
Abstract:
The design and analysis of systems that combine computational behaviour with physical processes' continuous dynamics - such as movement, velocity, and voltage - is a famous, challenging task. Several theoretical results from programming theory emerged in the last decades to tackle the issue; some of which are the basis of a proof-of-concept tool, called Lince, that aids in the analysis of such sys…
▽ More
The design and analysis of systems that combine computational behaviour with physical processes' continuous dynamics - such as movement, velocity, and voltage - is a famous, challenging task. Several theoretical results from programming theory emerged in the last decades to tackle the issue; some of which are the basis of a proof-of-concept tool, called Lince, that aids in the analysis of such systems, by presenting simulations of their respective behaviours.
However being a proof-of-concept, the tool is quite limited with respect to usability, and when attempting to apply it to a set of common, concrete problems, involving autonomous driving and others, it either simply cannot simulate them or fails to provide a satisfactory user-experience.
The current work complements the aforementioned theoretical approaches with a more practical perspective, by improving Lince along several dimensions: to name a few, richer syntactic constructs, more operations, more informative plotting systems and errors messages, and a better performance overall. We illustrate our improvements via a variety of examples that involve both autonomous driving and electrical systems.
△ Less
Submitted 21 November, 2024;
originally announced November 2024.
-
An adequacy theorem between mixed powerdomains and probabilistic concurrency
Authors:
Renato Neves
Abstract:
We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains which combine non-determinism with stochasticity. The theorem itself is formulated via M. Smyth's idea of treating observable properties as open sets of a topological space.
One application of our theorem is that it entails semi-decida…
▽ More
We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains which combine non-determinism with stochasticity. The theorem itself is formulated via M. Smyth's idea of treating observable properties as open sets of a topological space.
One application of our theorem is that it entails semi-decidability w.r.t. whether a concurrent program satisfies an observable property (written in a certain form). This is intimately connected to M. Escardó's conjecture about semi-decidability w.r.t. may and must probabilistic testing.
△ Less
Submitted 24 September, 2024;
originally announced September 2024.
-
Embedding Aggregation for Forensic Facial Comparison
Authors:
Rafael Oliveira Ribeiro,
João C. R. Neves,
Arnout C. C. Ruifrok,
Flavio de Barros Vidal
Abstract:
In forensic facial comparison, questioned-source images are usually captured in uncontrolled environments, with non-uniform lighting, and from non-cooperative subjects. The poor quality of such material usually compromises their value as evidence in legal matters. On the other hand, in forensic casework, multiple images of the person of interest are usually available. In this paper, we propose to…
▽ More
In forensic facial comparison, questioned-source images are usually captured in uncontrolled environments, with non-uniform lighting, and from non-cooperative subjects. The poor quality of such material usually compromises their value as evidence in legal matters. On the other hand, in forensic casework, multiple images of the person of interest are usually available. In this paper, we propose to aggregate deep neural network embeddings from various images of the same person to improve performance in facial verification. We observe significant performance improvements, especially for very low-quality images. Further improvements are obtained by aggregating embeddings of more images and by applying quality-weighted aggregation. We demonstrate the benefits of this approach in forensic evaluation settings with the development and validation of score-based likelihood ratio systems and report improvements in Cllr of up to 95% (from 0.249 to 0.012) for CCTV images and of up to 96% (from 0.083 to 0.003) for social media images.
△ Less
Submitted 29 April, 2023;
originally announced May 2023.
-
A Complete V-Equational System for Graded lambda-Calculus
Authors:
Fredrik Dahlqvist,
Renato Neves
Abstract:
Modern programming frequently requires generalised notions of program equivalence based on a metric or a similar structure. Previous work addressed this challenge by introducing the notion of a V-equation, i.e. an equation labelled by an element of a quantale V, which covers inter alia (ultra-)metric, classical, and fuzzy (in)equations. It also introduced a V-equational system for the linear varia…
▽ More
Modern programming frequently requires generalised notions of program equivalence based on a metric or a similar structure. Previous work addressed this challenge by introducing the notion of a V-equation, i.e. an equation labelled by an element of a quantale V, which covers inter alia (ultra-)metric, classical, and fuzzy (in)equations. It also introduced a V-equational system for the linear variant of lambda-calculus where any given resource must be used exactly once.
In this paper we drop the (often too strict) linearity constraint by adding graded modal types which allow multiple uses of a resource in a controlled manner. We show that such a control, whilst providing more expressivity to the programmer, also interacts more richly with V-equations than the linear or Cartesian cases. Our main result is the introduction of a sound and complete V-equational system for a lambda-calculus with graded modal types interpreted by what we call a Lipschitz exponential comonad. We also show how to build such comonads canonically via a universal construction, and use our results to derive graded metric equational systems (and corresponding models) for programs with timed and probabilistic behaviour.
△ Less
Submitted 17 November, 2023; v1 submitted 4 April, 2023;
originally announced April 2023.
-
The syntactic side of autonomous categories enriched over generalised metric spaces
Authors:
Fredrik Dahlqvist,
Renato Neves
Abstract:
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the intro…
▽ More
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear λ-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear λ-theories based on this V-equational system form a category that is equivalent to a category of autonomous categories enriched over 'generalised metric spaces'. If we instantiate this result to inequations, we get an equivalence with autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an equivalence with autonomous categories enriched over (ultra)metric spaces. We additionally show that this syntax-semantics correspondence extends to the affine setting. We use our results to develop examples of inequational and metric equational systems for higher-order programming in the setting of real-time, probabilistic, and quantum computing.
△ Less
Submitted 15 December, 2023; v1 submitted 30 August, 2022;
originally announced August 2022.
-
An Internal Language for Categories Enriched over Generalised Metric Spaces
Authors:
Fredrik Dahlqvist,
Renato Neves
Abstract:
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the intro…
▽ More
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear λ-calculus together with a proof that it is sound and complete (in fact, an internal language) for a class of enriched autonomous categories. In the case of inequations, we get an internal language for autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an internal language for autonomous categories enriched over (ultra)metric spaces. We use our results to obtain examples of inequational and metric equational systems for higher-order programs that contain real-time and probabilistic behaviour
△ Less
Submitted 27 October, 2021; v1 submitted 18 May, 2021;
originally announced May 2021.
-
Implementing Hybrid Semantics: From Functional to Imperative
Authors:
Sergey Goncharov,
Renato Neves,
José Proença
Abstract:
Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combi…
▽ More
Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combination of hybrid behaviour with other effects. A systematic treatment of hybridness as a dedicated computational effect has emerged recently. In particular, a generic idealized functional language HybCore with a sound and adequate operational semantics has been proposed. The latter semantics however did not provide hints to implementing HybCore as a runnable language, suitable for hybrid system simulation (e.g. the semantics features rules with uncountably many premises). We introduce an imperative counterpart of HybCore, whose semantics is simpler and runnable, and yet intimately related with the semantics of HybCore at the level of hybrid monads. We then establish a corresponding soundness and adequacy theorem. To attest that the resulting semantics can serve as a firm basis for the implementation of typical tools of programming oriented to the hybrid domain, we present a web-based prototype implementation to evaluate and inspect hybrid programs, in the spirit of GHCi for Haskell and UTop for OCaml. The major asset of our implementation is that it formally follows the operational semantic rules.
△ Less
Submitted 29 September, 2020;
originally announced September 2020.
-
Medical idioms for clinical Bayesian network development
Authors:
Evangelia Kyrimi,
Mariana Raniere Neves,
Scott McLachlan,
Martin Neil,
William Marsh,
Norman Fenton
Abstract:
Bayesian Networks (BNs) are graphical probabilistic models that have proven popular in medical applications. While numerous medical BNs have been published, most are presented fait accompli without explanation of how the network structure was developed or justification of why it represents the correct structure for the given medical application. This means that the process of building medical BNs…
▽ More
Bayesian Networks (BNs) are graphical probabilistic models that have proven popular in medical applications. While numerous medical BNs have been published, most are presented fait accompli without explanation of how the network structure was developed or justification of why it represents the correct structure for the given medical application. This means that the process of building medical BNs from experts is typically ad hoc and offers little opportunity for methodological improvement. This paper proposes generally applicable and reusable medical reasoning patterns to aid those developing medical BNs. The proposed method complements and extends the idiom-based approach introduced by Neil, Fenton, and Nielsen in 2000. We propose instances of their generic idioms that are specific to medical BNs. We refer to the proposed medical reasoning patterns as medical idioms. In addition, we extend the use of idioms to represent interventional and counterfactual reasoning. We believe that the proposed medical idioms are logical reasoning patterns that can be combined, reused and applied generically to help develop medical BNs. All proposed medical idioms have been illustrated using medical examples on coronary artery disease. The method has also been applied to other ongoing BNs being developed with medical experts. Finally, we show that applying the proposed medical idioms to published BN models results in models with a clearer structure.
△ Less
Submitted 2 July, 2020; v1 submitted 1 July, 2020;
originally announced July 2020.
-
A Comprehensive Scoping Review of Bayesian Networks in Healthcare: Past, Present and Future
Authors:
Evangelia Kyrimi,
Scott McLachlan,
Kudakwashe Dube,
Mariana R. Neves,
Ali Fahmi,
Norman Fenton
Abstract:
No comprehensive review of Bayesian networks (BNs) in healthcare has been published in the past, making it difficult to organize the research contributions in the present and identify challenges and neglected areas that need to be addressed in the future. This unique and novel scoping review of BNs in healthcare provides an analytical framework for comprehensively characterizing the domain and its…
▽ More
No comprehensive review of Bayesian networks (BNs) in healthcare has been published in the past, making it difficult to organize the research contributions in the present and identify challenges and neglected areas that need to be addressed in the future. This unique and novel scoping review of BNs in healthcare provides an analytical framework for comprehensively characterizing the domain and its current state. The review shows that: (1) BNs in healthcare are not used to their full potential; (2) a generic BN development process is lacking; (3) limitations exists in the way BNs in healthcare are presented in the literature, which impacts understanding, consensus towards systematic methodologies, practice and adoption of BNs; and (4) a gap exists between having an accurate BN and a useful BN that impacts clinical practice. This review empowers researchers and clinicians with an analytical framework and findings that will enable understanding of the need to address the problems of restricted aims of BNs, ad hoc BN development methods, and the lack of BN adoption in practice. To map the way forward, the paper proposes future research directions and makes recommendations regarding BN development methods and adoption in practice.
△ Less
Submitted 28 February, 2020; v1 submitted 20 February, 2020;
originally announced February 2020.
-
An Adequate While-Language for Hybrid Computation
Authors:
Sergey Goncharov,
Renato Neves
Abstract:
Hybrid computation combines discrete and continuous dynamics in the form of an entangled mixture inherently present both in various natural phenomena, and in applications ranging from control theory to microbiology. The emergent behaviours bear signs of both computational and physical processes, and thus present difficulties not only for analysis, but also for describing them adequately in a struc…
▽ More
Hybrid computation combines discrete and continuous dynamics in the form of an entangled mixture inherently present both in various natural phenomena, and in applications ranging from control theory to microbiology. The emergent behaviours bear signs of both computational and physical processes, and thus present difficulties not only for analysis, but also for describing them adequately in a structural, well-founded way. Here, we introduce a language for hybrid computation, inspired by the fine-grain call-by-value paradigm, and equip it with a denotational and computationally adequate denotational semantics. Our denotational semantics crucially relies on a hybrid monad supporting an (Elgot) iteration operator, we developed elsewhere. As an intermediate step we introduce a more lightweight duration semantics furnished with analogous results and drawing on a new duration monad that we introduce as a lightweight counterpart to the hybrid monad.
△ Less
Submitted 17 July, 2019; v1 submitted 20 February, 2019;
originally announced February 2019.
-
A Semantics for Hybrid Iteration
Authors:
Sergey Goncharov,
Julian Jakob,
Renato Neves
Abstract:
The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and preserving its merits. In this paper we use these notions and the corresponding stock of results to examine different types of iteration for hybrid computations. As…
▽ More
The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and preserving its merits. In this paper we use these notions and the corresponding stock of results to examine different types of iteration for hybrid computations. As a starting point we use an available notion of hybrid monad restricted to the category of sets, and modify it in order to obtain a suitable notion of guarded iteration with guardedness interpreted as progressiveness in time - we motivate this modification by our intention to capture Zeno behaviour in an arguably general and feasible way. We illustrate our results with a simple programming language for hybrid computations and interpret it over the developed semantic foundations.
△ Less
Submitted 5 February, 2019; v1 submitted 3 July, 2018;
originally announced July 2018.
-
Currency exchange prediction using machine learning, genetic algorithms and technical analysis
Authors:
Gonçalo Abreu,
Rui Neves,
Nuno Horta
Abstract:
Technical analysis is used to discover investment opportunities. To test this hypothesis we propose an hybrid system using machine learning techniques together with genetic algorithms. Using technical analysis there are more ways to represent a currency exchange time series than the ones it is possible to test computationally, i.e., it is unfeasible to search the whole input feature space thus a g…
▽ More
Technical analysis is used to discover investment opportunities. To test this hypothesis we propose an hybrid system using machine learning techniques together with genetic algorithms. Using technical analysis there are more ways to represent a currency exchange time series than the ones it is possible to test computationally, i.e., it is unfeasible to search the whole input feature space thus a genetic algorithm is an alternative. In this work, an architecture for automatic feature selection is proposed to optimize the cross validated performance estimation of a Naive Bayes model using a genetic algorithm. The proposed architecture improves the return on investment of the unoptimized system from 0,43% to 10,29% in the validation set. The features selected and the model decision boundary are visualized using the algorithm t-Distributed Stochastic Neighbor embedding.
△ Less
Submitted 28 May, 2018;
originally announced May 2018.
-
Compositional semantics for new paradigms: probabilistic, hybrid and beyond
Authors:
Fredrik Dahlqvist,
Renato Neves
Abstract:
Emerging computational paradigms, such as probabilistic and hybrid programming, introduce new primitive operations that often need to be combined with classic programming constructs. However, it still remains a challenge to provide a semantics to these features and their combination in a systematic manner. For this reason, we introduce a generic, monadic framework that allows us to investigate not…
▽ More
Emerging computational paradigms, such as probabilistic and hybrid programming, introduce new primitive operations that often need to be combined with classic programming constructs. However, it still remains a challenge to provide a semantics to these features and their combination in a systematic manner. For this reason, we introduce a generic, monadic framework that allows us to investigate not only which programming features a given paradigm supports, but also on how it can be extended with new constructs. By applying our method to the probabilistic and hybrid case, we list for example all binary program operations they possess, and show precisely when and if important axioms such as commutativity and idempotency hold. Using this framework, we also study the possibility of incorporating notions of failure and non-determinism, and obtain new results on this topic for hybrid and probabilistic programming.
△ Less
Submitted 11 April, 2018;
originally announced April 2018.
-
Limits in Categories of Vietoris Coalgebras
Authors:
Dirk Hofmann,
Renato Neves,
Pedro Nora
Abstract:
Motivated by the need to reason about hybrid systems, we study limits in categories of coalgebras whose underlying functor is a Vietoris polynomial one - intuitively, the topological analogue of a Kripke polynomial functor. Among other results, we prove that every Vietoris polynomial functor admits a final coalgebra if it respects certain conditions concerning separation axioms and compactness. Wh…
▽ More
Motivated by the need to reason about hybrid systems, we study limits in categories of coalgebras whose underlying functor is a Vietoris polynomial one - intuitively, the topological analogue of a Kripke polynomial functor. Among other results, we prove that every Vietoris polynomial functor admits a final coalgebra if it respects certain conditions concerning separation axioms and compactness. When the functor is restricted to some of the categories induced by these conditions the resulting categories of coalgebras are even complete. As a practical application, we use these developments in the specification and analysis of non-deterministic hybrid systems, in particular to obtain suitable notions of stability, and behaviour.
△ Less
Submitted 6 February, 2017; v1 submitted 10 December, 2016;
originally announced December 2016.
-
Continuity as a computational effect
Authors:
Renato Neves,
Luis S. Barbosa,
Dirk Hofmann,
Manuel A. Martins
Abstract:
The original purpose of component-based development was to provide techniques to master complex software, through composition, reuse and parametrisation. However, such systems are rapidly moving towards a level in which software becomes prevalently intertwined with (continuous) physical processes. A possible way to accommodate the latter in component calculi relies on a suitable encoding of contin…
▽ More
The original purpose of component-based development was to provide techniques to master complex software, through composition, reuse and parametrisation. However, such systems are rapidly moving towards a level in which software becomes prevalently intertwined with (continuous) physical processes. A possible way to accommodate the latter in component calculi relies on a suitable encoding of continuous behaviour as (yet another) computational effect. This paper introduces such an encoding through a monad which, in the compositional development of hybrid systems, may play a role similar to the one played by the 1+, powerset, and distribution monads in the characterisation of partial, non deterministic and probabilistic components, respectively. This monad and its Kleisli category provide a setting in which the effects of continuity over (different forms of) composition can be suitably studied.
△ Less
Submitted 1 August, 2016; v1 submitted 12 July, 2015;
originally announced July 2015.
