-
A Coalgebraic Semantics for Intuitionistic Modal Logic
Authors:
Rodrigo Nicolau Almeida,
Nick Bezhanishvili
Abstract:
We give a new coalgebraic semantics for intuitionistic modal logic with $\Box$. In particular, we provide a colagebraic representation of intuitionistic descriptive modal frames and of intuitonistic modal Kripke frames based on image-finite posets. This gives a solution to a problem in the area of coalgebaic logic for these classes of frames, raised explicitly by Litak (2014) and de Groot and Patt…
▽ More
We give a new coalgebraic semantics for intuitionistic modal logic with $\Box$. In particular, we provide a colagebraic representation of intuitionistic descriptive modal frames and of intuitonistic modal Kripke frames based on image-finite posets. This gives a solution to a problem in the area of coalgebaic logic for these classes of frames, raised explicitly by Litak (2014) and de Groot and Pattinson (2020). Our key technical tool is a recent generalization of a construction by Ghilardi, in the form of a right adjoint to the inclusion of the category of Esakia spaces in the category of Priestley spaces. As an application of these results, we study bisimulations of intuitionistic modal frames, describe dual spaces of free modal Heyting algebras, and provide a path towards a theory of coalgebraic intuitionistic logics.
△ Less
Submitted 15 June, 2024;
originally announced June 2024.
-
Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules
Authors:
Rodrigo Nicolau Almeida,
Silvio Ghilardi
Abstract:
We develop a method to recognize admissibility of $Π_{2}$-rules, relating this problem to a specific instance of the unification problem with linear constants restriction, called here "unification with simple variable restriction". It is shown that for logical systems enjoying an appropriate algebraic semantics and a finite approximation of left uniform interpolation, this unification with simple…
▽ More
We develop a method to recognize admissibility of $Π_{2}$-rules, relating this problem to a specific instance of the unification problem with linear constants restriction, called here "unification with simple variable restriction". It is shown that for logical systems enjoying an appropriate algebraic semantics and a finite approximation of left uniform interpolation, this unification with simple variable restriction can be reduced to standard unification. As a corollary, we obtain the decidability of admissibility of $Π_{2}$-rules for many logical systems.
△ Less
Submitted 5 June, 2024;
originally announced June 2024.
-
$Π_{2}$-Rule Systems and Inductive Classes of Gödel Algebras
Authors:
Rodrigo Nicolau Almeida
Abstract:
In this paper we present a general theory of $Π_{2}$-rules for systems of intuitionistic and modal logic. We introduce the notions of $Π_{2}$-rule system and of an Inductive Class, and provide model-theoretic and algebraic completeness theorems, which serve as our basic tools. As an illustration of the general theory, we analyse the structure of inductive classes of Gödel algebras, from a structur…
▽ More
In this paper we present a general theory of $Π_{2}$-rules for systems of intuitionistic and modal logic. We introduce the notions of $Π_{2}$-rule system and of an Inductive Class, and provide model-theoretic and algebraic completeness theorems, which serve as our basic tools. As an illustration of the general theory, we analyse the structure of inductive classes of Gödel algebras, from a structure theoretic and logical point of view. We show that unlike other well-studied settings (such as logics, or single-conclusion rule systems), there are continuum many $Π_{2}$-rule systems extending $\mathsf{LC}=\mathsf{IPC}+(p\rightarrow q)\vee (q\rightarrow p)$, and show how our methods allow easy proofs of the admissibility of the well-known Takeuti-Titani rule. Our final results concern general questions admissibility in $\mathsf{LC}$: (1) we present a full classification of those inductive classes which are inductively complete, i.e., where all $Π_{2}$-rules which are admissible are derivable, and (2) show that the problem of admissibility of $Π_{2}$-rules over $\mathsf{LC}$ is decidable.
△ Less
Submitted 13 November, 2023;
originally announced November 2023.
-
UAV-Assisted Wireless Communications: An Experimental Analysis of A2G and G2A Channels
Authors:
Kamran Shafafi,
Eduardo Nuno Almeida,
André Coelho,
Helder Fontes,
Manuel Ricardo,
Rui Campos
Abstract:
Unmanned Aerial Vehicles (UAVs) offer promising potential as communications node carriers, providing on-demand wireless connectivity to users. While existing literature presents various wireless channel models, it often overlooks the impact of UAV heading. This paper provides an experimental characterization of the Air-to-Ground (A2G) and Ground-to-Air (G2A) wireless channels in an open environmen…
▽ More
Unmanned Aerial Vehicles (UAVs) offer promising potential as communications node carriers, providing on-demand wireless connectivity to users. While existing literature presents various wireless channel models, it often overlooks the impact of UAV heading. This paper provides an experimental characterization of the Air-to-Ground (A2G) and Ground-to-Air (G2A) wireless channels in an open environment with no obstacles nor interference, considering the distance and the UAV heading. We analyze the received signal strength indicator and the TCP throughput between a ground user and a UAV, covering distances between 50~m and 500~m, and considering different UAV headings. Additionally, we characterize the antenna's radiation pattern based on UAV headings. The paper provides valuable perspectives on the capabilities of UAVs in offering on-demand and dynamic wireless connectivity, as well as highlights the significance of considering UAV heading and antenna configurations in real-world scenarios.
△ Less
Submitted 12 August, 2023; v1 submitted 29 March, 2023;
originally announced March 2023.
-
Position-Based Machine Learning Propagation Loss Model Enabling Fast Digital Twins of Wireless Networks in ns-3
Authors:
Eduardo Nuno Almeida,
Helder Fontes,
Rui Campos,
Manuel Ricardo
Abstract:
Digital twins have been emerging as a hybrid approach that combines the benefits of simulators with the realism of experimental testbeds. The accurate and repeatable set-ups replicating the dynamic conditions of physical environments, enable digital twins of wireless networks to be used to evaluate the performance of next-generation networks. In this paper, we propose the Position-based Machine Le…
▽ More
Digital twins have been emerging as a hybrid approach that combines the benefits of simulators with the realism of experimental testbeds. The accurate and repeatable set-ups replicating the dynamic conditions of physical environments, enable digital twins of wireless networks to be used to evaluate the performance of next-generation networks. In this paper, we propose the Position-based Machine Learning Propagation Loss Model (P-MLPL), enabling the creation of fast and more precise digital twins of wireless networks in ns-3. Based on network traces collected in an experimental testbed, the P-MLPL model estimates the propagation loss suffered by packets exchanged between a transmitter and a receiver, considering the absolute node's positions and the traffic direction. The P-MLPL model is validated with a test suite. The results show that the P-MLPL model can predict the propagation loss with a median error of 2.5 dB, which corresponds to 0.5x the error of existing models in ns-3. Moreover, ns-3 simulations with the P-MLPL model estimated the throughput with an error up to 2.5 Mbit/s, when compared to the real values measured in the testbed.
△ Less
Submitted 22 February, 2023;
originally announced February 2023.
-
Machine Learning and Thermography Applied to the Detection and Classification of Cracks in Building
Authors:
Angela Busheska,
Nara Almeida,
Nicholas Sabella,
Eudes de A. Rocha
Abstract:
Due to the environmental impacts caused by the construction industry, repurposing existing buildings and making them more energy-efficient has become a high-priority issue. However, a legitimate concern of land developers is associated with the buildings' state of conservation. For that reason, infrared thermography has been used as a powerful tool to characterize these buildings' state of conserv…
▽ More
Due to the environmental impacts caused by the construction industry, repurposing existing buildings and making them more energy-efficient has become a high-priority issue. However, a legitimate concern of land developers is associated with the buildings' state of conservation. For that reason, infrared thermography has been used as a powerful tool to characterize these buildings' state of conservation by detecting pathologies, such as cracks and humidity. Thermal cameras detect the radiation emitted by any material and translate it into temperature-color-coded images. Abnormal temperature changes may indicate the presence of pathologies, however, reading thermal images might not be quite simple. This research project aims to combine infrared thermography and machine learning (ML) to help stakeholders determine the viability of reusing existing buildings by identifying their pathologies and defects more efficiently and accurately. In this particular phase of this research project, we've used an image classification machine learning model of Convolutional Neural Networks (DCNN) to differentiate three levels of cracks in one particular building. The model's accuracy was compared between the MSX and thermal images acquired from two distinct thermal cameras and fused images (formed through multisource information) to test the influence of the input data and network on the detection results.
△ Less
Submitted 30 December, 2022;
originally announced December 2022.
-
Machine Learning Based Propagation Loss Module for Enabling Digital Twins of Wireless Networks in ns-3
Authors:
Eduardo Nuno Almeida,
Mohammed Rushad,
Sumanth Reddy Kota,
Akshat Nambiar,
Hardik L. Harti,
Chinmay Gupta,
Danish Waseem,
Gonçalo Santos,
Helder Fontes,
Rui Campos,
Mohit P. Tahiliani
Abstract:
The creation of digital twins of experimental testbeds allows the validation of novel wireless networking solutions and the evaluation of their performance in realistic conditions, without the cost, complexity and limited availability of experimental testbeds. Current trace-based simulation approaches for ns-3 enable the repetition and reproduction of the same exact conditions observed in past exp…
▽ More
The creation of digital twins of experimental testbeds allows the validation of novel wireless networking solutions and the evaluation of their performance in realistic conditions, without the cost, complexity and limited availability of experimental testbeds. Current trace-based simulation approaches for ns-3 enable the repetition and reproduction of the same exact conditions observed in past experiments. However, they are limited by the fact that the simulation setup must exactly match the original experimental setup, including the network topology, the mobility patterns and the number of network nodes. In this paper, we propose the Machine Learning based Propagation Loss (MLPL) module for ns-3. Based on network traces collected in an experimental testbed, the MLPL module estimates the propagation loss as the sum of a deterministic path loss and a stochastic fast-fading loss. The MLPL module is validated with unit tests. Moreover, we test the MLPL module with real network traces, and compare the results obtained with existing propagation loss models in ns-3 and real experimental results. The results obtained show that the MLPL module can accurately predict the propagation loss observed in a real environment and reproduce the experimental conditions of a given testbed, enabling the creation of digital twins of wireless network environments in ns-3.
△ Less
Submitted 9 May, 2022;
originally announced May 2022.
-
Traffic-Aware UAV Placement Using a Generalizable Deep Reinforcement Learning Methodology
Authors:
Eduardo Nuno Almeida,
Rui Campos,
Manuel Ricardo
Abstract:
Unmanned Aerial Vehicles (UAVs) acting as Flying Access Points (FAPs) are being used to provide on-demand wireless connectivity in extreme scenarios. Despite ongoing research, the optimization of UAVs' positions according to dynamic users' traffic demands remains challenging. We propose the Traffic-aware UAV Placement Algorithm (TUPA), which positions a UAV acting as FAP according to the users' tr…
▽ More
Unmanned Aerial Vehicles (UAVs) acting as Flying Access Points (FAPs) are being used to provide on-demand wireless connectivity in extreme scenarios. Despite ongoing research, the optimization of UAVs' positions according to dynamic users' traffic demands remains challenging. We propose the Traffic-aware UAV Placement Algorithm (TUPA), which positions a UAV acting as FAP according to the users' traffic demands, in order to maximize the network utility. Using a DRL approach enables the FAP to autonomously learn and adapt to dynamic conditions and requirements of networking scenarios. Moreover, the proposed DRL methodology allows TUPA to generalize knowledge acquired during training to unknown combinations of users' positions and traffic demands, with no additional training. TUPA is trained and evaluated using network simulator ns-3 and ns3-gym framework. The results demonstrate that TUPA increases the network utility, compared to baseline solutions, increasing the average network utility up to 4x in scenarios with heterogeneous traffic demands.
△ Less
Submitted 16 March, 2022;
originally announced March 2022.
-
Wi-Fi Rate Adaptation using a Simple Deep Reinforcement Learning Approach
Authors:
Ruben Queiros,
Eduardo Nuno Almeida,
Helder Fontes,
Jose Ruela,
Rui Campos
Abstract:
The increasing complexity of recent Wi-Fi amendments is making optimal Rate Adaptation (RA) a challenge. The use of classic algorithms or heuristic models to address RA is becoming unfeasible due to the large combination of configuration parameters along with the variability of the wireless channel. Machine Learning-based solutions have been proposed in the state of art, to deal with this complexi…
▽ More
The increasing complexity of recent Wi-Fi amendments is making optimal Rate Adaptation (RA) a challenge. The use of classic algorithms or heuristic models to address RA is becoming unfeasible due to the large combination of configuration parameters along with the variability of the wireless channel. Machine Learning-based solutions have been proposed in the state of art, to deal with this complexity. However, they typically use complex models and their implementation in real scenarios is difficult. We propose a simple Deep Reinforcement Learning approach for the automatic RA in Wi-Fi networks, named Data-driven Algorithm for Rate Adaptation (DARA). DARA is standard-compliant. It dynamically adjusts the Wi-Fi Modulation and Coding Scheme (MCS) solely based on the observation of the Signal-to-Noise Ratio (SNR) of the received frames at the transmitter. Our simulation results show that DARA achieves up to 15\% higher throughput when compared with Minstrel High Throughput (HT) and equals the performance of the Ideal Wi-Fi RA algorithm.
△ Less
Submitted 11 February, 2022; v1 submitted 8 February, 2022;
originally announced February 2022.
-
Joint Traffic-Aware UAV Placement and Predictive Routing for Aerial Networks
Authors:
Eduardo Nuno Almeida,
André Coelho,
José Ruela,
Rui Campos,
Manuel Ricardo
Abstract:
Aerial networks, composed of Unmanned Aerial Vehicles (UAVs) acting as Wi-Fi access points or cellular base stations, are emerging as an interesting solution to provide on-demand wireless connectivity to users, when there is no network infrastructure available, or to enhance the network capacity. This article proposes a traffic-aware topology control solution for aerial networks that holistically…
▽ More
Aerial networks, composed of Unmanned Aerial Vehicles (UAVs) acting as Wi-Fi access points or cellular base stations, are emerging as an interesting solution to provide on-demand wireless connectivity to users, when there is no network infrastructure available, or to enhance the network capacity. This article proposes a traffic-aware topology control solution for aerial networks that holistically combines the placement of UAVs with a predictive and centralized routing protocol. The synergy created by the combination of the UAV placement and routing solutions allows the aerial network to seamlessly update its topology according to the users' traffic demand, whilst minimizing the disruption caused by the movement of the UAVs. As a result, the Quality of Service (QoS) provided to the users is improved. The components of the proposed solution are described and evaluated individually in this article by means of simulation and an experimental testbed. The results show that all the components improve the QoS provided to the users when compared to the corresponding baseline solutions.
△ Less
Submitted 15 April, 2020;
originally announced April 2020.
-
A Routing Metric for Inter-flow Interference-aware Flying Multi-hop Networks
Authors:
André Coelho,
Eduardo Nuno Almeida,
José Ruela,
Rui Campos,
Manuel Ricardo
Abstract:
The growing demand for broadband communications anytime, anywhere has paved the way to the usage of Unmanned Aerial Vehicles (UAVs) for providing Internet access in areas without network infrastructure and enhancing the performance of existing networks. However, the usage of Flying Multi-hop Networks (FMNs) in such scenarios brings up significant challenges concerning network routing, in order to…
▽ More
The growing demand for broadband communications anytime, anywhere has paved the way to the usage of Unmanned Aerial Vehicles (UAVs) for providing Internet access in areas without network infrastructure and enhancing the performance of existing networks. However, the usage of Flying Multi-hop Networks (FMNs) in such scenarios brings up significant challenges concerning network routing, in order to permanently provide the Quality of Service expected by the users. The problem is exacerbated in crowded events, where the FMN may be formed by many UAVs to address the traffic demand, causing inter-flow interference within the FMN. Typically, estimating inter-flow interference is not straightforward and requires the exchange of probe packets, thus increasing network overhead. The main contribution of this paper is an inter-flow interference-aware routing metric, named I2R, designed for centralized routing in FMNs with controllable topology. I2R does not require any control packets and enables the configuration of paths with minimal Euclidean distance formed by UAVs with the lowest number of neighbors in carrier-sense range, thus minimizing inter-flow interference in the FMN. Simulation results show the I2R superior performance, with significant gains in terms of throughput and end-to-end delay, when compared with state of the art routing metrics.
△ Less
Submitted 17 December, 2019;
originally announced December 2019.
-
Joint User Mobility and Traffic Characterization in Temporary Crowded Events
Authors:
Adriano Valadar,
Eduardo Nuno Almeida,
Jorge Mamede
Abstract:
In TCEs (Temporary Crowded Events), for example, music festivals, users are faced with problems accessing the Internet. TCEs are limited time events with a high concentration of people moving within the event enclosure while accessing the Internet. Unlike other events where the user locations are constant and known at the start (e.g. stadiums), the traffic generation and the user movement in TCEs…
▽ More
In TCEs (Temporary Crowded Events), for example, music festivals, users are faced with problems accessing the Internet. TCEs are limited time events with a high concentration of people moving within the event enclosure while accessing the Internet. Unlike other events where the user locations are constant and known at the start (e.g. stadiums), the traffic generation and the user movement in TCEs is variable and influenced by the dynamics of the event. The movement of users can lead to overloads in APs (Access Point) in case they are fixed. In order to minimize this phenomenon, new techniques have been explored that resort to the adjustable positioning of APs integrated into UAVs (Unmanned Aerial Vehicles). In these scenarios, the dynamic of the location of the APs requires that tools of prediction of the users movements and, in turn, of the sources of traffic, gain particular expression when being related to the algorithms of positioning of the referred APs. In order to allow the development and analysis of new network planning solutions for TCEs, it is necessary to recreate these scenarios in simulation, which, in turn, requires a detailed characterization of this kind of events. This article aims to characterize and model the mobility and traffic generated by users in TCEs. This characterization will enable the development of new statistical models of traffic generation and user mobility in TCEs.
△ Less
Submitted 3 July, 2019; v1 submitted 30 June, 2019;
originally announced July 2019.
-
Grid-Brick Event Processing Framework in GEPS
Authors:
Antonio Amorim,
Luis Pedro,
Han Fei,
Nuno Almeida,
Paulo Trezentos,
Jaime E. Villate
Abstract:
Experiments like ATLAS at LHC involve a scale of computing and data management that greatly exceeds the capability of existing systems, making it necessary to resort to Grid-based Parallel Event Processing Systems (GEPS). Traditional Grid systems concentrate the data in central data servers which have to be accessed by many nodes each time an analysis or processing job starts. These systems requ…
▽ More
Experiments like ATLAS at LHC involve a scale of computing and data management that greatly exceeds the capability of existing systems, making it necessary to resort to Grid-based Parallel Event Processing Systems (GEPS). Traditional Grid systems concentrate the data in central data servers which have to be accessed by many nodes each time an analysis or processing job starts. These systems require very powerful central data servers and make little use of the distributed disk space that is available in commodity computers. The Grid-Brick system, which is described in this paper, follows a different approach. The data storage is split among all grid nodes having each one a piece of the whole information. Users submit queries and the system will distribute the tasks through all the nodes and retrieve the result, merging them together in the Job Submit Server. The main advantage of using this system is the huge scalability it provides, while its biggest disadvantage appears in the case of failure of one of the nodes. A workaround for this problem involves data replication or backup.
△ Less
Submitted 14 June, 2003;
originally announced June 2003.
