-
UTC Time, Formally Verified
Authors:
Ana de Almeida Borges,
Mireia González Bedmar,
Juan Conejero Rodríguez,
Eduardo Hermo Reyes,
Joaquim Casals Buñuel,
Joost J. Joosten
Abstract:
FV Time is a small-scale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually…
▽ More
FV Time is a small-scale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet non-trivial, it nicely illustrates our methodology for verifying software with Coq.
In this paper we present a description of the project, emphasizing the main problems faced while develo** the library, as well as some general-purpose solutions that were produced as by-products and may be used in other verification projects. These include a refinement package between proof-oriented MathComp numbers and computation-oriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through brute-force computation.
△ Less
Submitted 13 December, 2023; v1 submitted 28 September, 2022;
originally announced September 2022.
-
Towards a Coq formalization of a quantified modal logic
Authors:
Ana de Almeida Borges
Abstract:
We present a Coq formalization of the Quantified Reflection Calculus with one modality, or $\mathsf{QRC}_1$. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The highlights are a deep embedding of $\mathsf{QRC}_1$ in the Coq proof assistant, a mechanization of the notion of Kripke model with varying domains and a formalizat…
▽ More
We present a Coq formalization of the Quantified Reflection Calculus with one modality, or $\mathsf{QRC}_1$. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The highlights are a deep embedding of $\mathsf{QRC}_1$ in the Coq proof assistant, a mechanization of the notion of Kripke model with varying domains and a formalization of the soundness theorem. We focus on the design decisions inherent to the formalization and the insights that led to new and simplified proofs.
△ Less
Submitted 2 July, 2022; v1 submitted 7 June, 2022;
originally announced June 2022.
-
Standing Forest Coin (SFC)
Authors:
Marcelo de A. Borges,
Guido L. de S. Filho,
Cicero Inacio da Silva,
Anderson M. P. Barros,
Raul V. B. J. Britto,
Nivaldo M. de C. Junior,
Daniel F. L. de Souza
Abstract:
This article describes a proposal to create a digital currency that allows the decentralized collection of resources directed to initiatives and activities that aim to protect the Brazilian Amazon ecosystem by using blockchain and digital contracts. In addition to the digital currency, the goal is to design a smart contract based in oracles to ensure credibility and security for investors and dono…
▽ More
This article describes a proposal to create a digital currency that allows the decentralized collection of resources directed to initiatives and activities that aim to protect the Brazilian Amazon ecosystem by using blockchain and digital contracts. In addition to the digital currency, the goal is to design a smart contract based in oracles to ensure credibility and security for investors and donors of financial resources invested in projects within the Standing Forest Coin (SFC - standingforest.org).
△ Less
Submitted 4 March, 2022;
originally announced March 2022.
-
Modeling the geospatial evolution of COVID-19 using spatio-temporal convolutional sequence-to-sequence neural networks
Authors:
Mário Cardoso,
André Cavalheiro,
Alexandre Borges,
Ana F. Duarte,
Amílcar Soares,
Maria João Pereira,
Nuno J. Nunes,
Leonardo Azevedo,
Arlindo L. Oliveira
Abstract:
Europe was hit hard by the COVID-19 pandemic and Portugal was one of the most affected countries, having suffered three waves in the first twelve months. Approximately between Jan 19th and Feb 5th 2021 Portugal was the country in the world with the largest incidence rate, with 14-days incidence rates per 100,000 inhabitants in excess of 1000. Despite its importance, accurate prediction of the geos…
▽ More
Europe was hit hard by the COVID-19 pandemic and Portugal was one of the most affected countries, having suffered three waves in the first twelve months. Approximately between Jan 19th and Feb 5th 2021 Portugal was the country in the world with the largest incidence rate, with 14-days incidence rates per 100,000 inhabitants in excess of 1000. Despite its importance, accurate prediction of the geospatial evolution of COVID-19 remains a challenge, since existing analytical methods fail to capture the complex dynamics that result from both the contagion within a region and the spreading of the infection from infected neighboring regions.
We use a previously developed methodology and official municipality level data from the Portuguese Directorate-General for Health (DGS), relative to the first twelve months of the pandemic, to compute an estimate of the incidence rate in each location of mainland Portugal. The resulting sequence of incidence rate maps was then used as a gold standard to test the effectiveness of different approaches in the prediction of the spatial-temporal evolution of the incidence rate. Four different methods were tested: a simple cell level autoregressive moving average (ARMA) model, a cell level vector autoregressive (VAR) model, a municipality-by-municipality compartmental SIRD model followed by direct block sequential simulation and a convolutional sequence-to-sequence neural network model based on the STConvS2S architecture. We conclude that the convolutional sequence-to-sequence neural network is the best performing method, when predicting the medium-term future incidence rate, using the available information.
△ Less
Submitted 6 May, 2021;
originally announced May 2021.
-
Combining Off and On-Policy Training in Model-Based Reinforcement Learning
Authors:
Alexandre Borges,
Arlindo Oliveira
Abstract:
The combination of deep learning and Monte Carlo Tree Search (MCTS) has shown to be effective in various domains, such as board and video games. AlphaGo represented a significant step forward in our ability to learn complex board games, and it was rapidly followed by significant advances, such as AlphaGo Zero and AlphaZero. Recently, MuZero demonstrated that it is possible to master both Atari gam…
▽ More
The combination of deep learning and Monte Carlo Tree Search (MCTS) has shown to be effective in various domains, such as board and video games. AlphaGo represented a significant step forward in our ability to learn complex board games, and it was rapidly followed by significant advances, such as AlphaGo Zero and AlphaZero. Recently, MuZero demonstrated that it is possible to master both Atari games and board games by directly learning a model of the environment, which is then used with MCTS to decide what move to play in each position. During tree search, the algorithm simulates games by exploring several possible moves and then picks the action that corresponds to the most promising trajectory. When training, limited use is made of these simulated games since none of their trajectories are directly used as training examples. Even if we consider that not all trajectories from simulated games are useful, there are thousands of potentially useful trajectories that are discarded. Using information from these trajectories would provide more training data, more quickly, leading to faster convergence and higher sample efficiency. Recent work introduced an off-policy value target for AlphaZero that uses data from simulated games. In this work, we propose a way to obtain off-policy targets using data from simulated games in MuZero. We combine these off-policy targets with the on-policy targets already used in MuZero in several ways, and study the impact of these targets and their combinations in three environments with distinct characteristics. When used in the right combinations, our results show that these targets can speed up the training process and lead to faster convergence and higher rewards than the ones obtained by MuZero.
△ Less
Submitted 28 April, 2021; v1 submitted 24 February, 2021;
originally announced February 2021.
-
Low-complexity Architecture for AR(1) Inference
Authors:
A. Borges Jr.,
R. J. Cintra,
D. F. G. Coelho,
V. S. Dimitrov
Abstract:
In this Letter, we propose a low-complexity estimator for the correlation coefficient based on the signed $\operatorname{AR}(1)$ process. The introduced approximation is suitable for implementation in low-power hardware architectures. Monte Carlo simulations reveal that the proposed estimator performs comparably to the competing methods in literature with maximum error in order of $10^{-2}$. Howev…
▽ More
In this Letter, we propose a low-complexity estimator for the correlation coefficient based on the signed $\operatorname{AR}(1)$ process. The introduced approximation is suitable for implementation in low-power hardware architectures. Monte Carlo simulations reveal that the proposed estimator performs comparably to the competing methods in literature with maximum error in order of $10^{-2}$. However, the hardware implementation of the introduced method presents considerable advantages in several relevant metrics, offering more than 95% reduction in dynamic power and doubling the maximum operating frequency when compared to the reference method.
△ Less
Submitted 21 August, 2020;
originally announced August 2020.
-
When logic lays down the law
Authors:
Bjørn Jespersen,
Ana de Almeida Borges,
Jorge del Castillo Tierz,
Juan José Conejero Rodríguez,
Eric Sancho Adamson,
Aleix Solé Sánchez,
Nika Pona,
Joost J. Joosten
Abstract:
We analyse so-called computable laws, i.e., laws that can be enforced by automatic procedures. These laws should be logically perfect and unambiguous, but sometimes they are not. We use a regulation on road transport to illustrate this issue, and show what some fragments of this regulation would look like if rewritten in the image of logic. We further propose desiderata to be fulfilled by computab…
▽ More
We analyse so-called computable laws, i.e., laws that can be enforced by automatic procedures. These laws should be logically perfect and unambiguous, but sometimes they are not. We use a regulation on road transport to illustrate this issue, and show what some fragments of this regulation would look like if rewritten in the image of logic. We further propose desiderata to be fulfilled by computable laws, and provide a critical platform from which to assess existing laws and a guideline for composing future ones.
△ Less
Submitted 6 October, 2018;
originally announced October 2018.
