Showing 1–15 of 15 results for author: Marin, S

Optimizing Plastic Waste Collection in Water Bodies Using Heterogeneous Autonomous Surface Vehicles with Deep Reinforcement Learning

Authors: Alejandro Mendoza Barrionuevo, Samuel Yanes Luis, Daniel Gutiérrez Reina, Sergio L. Toral Marín

Abstract: This paper presents a model-free deep reinforcement learning framework for informative path planning with heterogeneous fleets of autonomous surface vehicles to locate and collect plastic waste. The system employs two teams of vehicles: scouts and cleaners. Coordination between these teams is achieved through a deep reinforcement approach, allowing agents to learn strategies to maximize cleaning e… ▽ More This paper presents a model-free deep reinforcement learning framework for informative path planning with heterogeneous fleets of autonomous surface vehicles to locate and collect plastic waste. The system employs two teams of vehicles: scouts and cleaners. Coordination between these teams is achieved through a deep reinforcement approach, allowing agents to learn strategies to maximize cleaning efficiency. The primary objective is for the scout team to provide an up-to-date contamination model, while the cleaner team collects as much waste as possible following this model. This strategy leads to heterogeneous teams that optimize fleet efficiency through inter-team cooperation supported by a tailored reward function. Different trainings of the proposed algorithm are compared with other state-of-the-art heuristics in two distinct scenarios, one with high convexity and another with narrow corridors and challenging access. According to the obtained results, it is demonstrated that deep reinforcement learning based algorithms outperform other benchmark heuristics, exhibiting superior adaptability. In addition, training with greedy actions further enhances performance, particularly in scenarios with intricate layouts. △ Less

Submitted 3 December, 2024; originally announced December 2024.

Comments: This article is currently under revision for the Robotics and Automation Letters (IEEE)

Nested Sequents for Quasi-transitive Modal Logics

Authors: Sonia Marin, Paaras Padhiar

Abstract: Previous works by Goré, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cut-elimination procedure and (ii) alternative modular formulations for these systems. We present our methodology to achieve these two goals on a subclass of path axioms, namely q… ▽ More Previous works by Goré, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cut-elimination procedure and (ii) alternative modular formulations for these systems. We present our methodology to achieve these two goals on a subclass of path axioms, namely quasi-transitivity axioms. △ Less

Submitted 13 June, 2024; originally announced June 2024.

Deep Reinforcement Multi-agent Learning framework for Information Gathering with Local Gaussian Processes for Water Monitoring

Authors: Samuel Yanes Luis, Dmitriy Shutin, Juan Marchal Gómez, Daniel Gutiérrez Reina, Sergio Toral Marín

Abstract: The conservation of hydrological resources involves continuously monitoring their contamination. A multi-agent system composed of autonomous surface vehicles is proposed in this paper to efficiently monitor the water quality. To achieve a safe control of the fleet, the fleet policy should be able to act based on measurements and to the the fleet state. It is proposed to use Local Gaussian Processe… ▽ More The conservation of hydrological resources involves continuously monitoring their contamination. A multi-agent system composed of autonomous surface vehicles is proposed in this paper to efficiently monitor the water quality. To achieve a safe control of the fleet, the fleet policy should be able to act based on measurements and to the the fleet state. It is proposed to use Local Gaussian Processes and Deep Reinforcement Learning to jointly obtain effective monitoring policies. Local Gaussian processes, unlike classical global Gaussian processes, can accurately model the information in a dissimilar spatial correlation which captures more accurately the water quality information. A Deep convolutional policy is proposed, that bases the decisions on the observation on the mean and variance of this model, by means of an information gain reward. Using a Double Deep Q-Learning algorithm, agents are trained to minimize the estimation error in a safe manner thanks to a Consensus-based heuristic. Simulation results indicate an improvement of up to 24% in terms of the mean absolute error with the proposed models. Also, training results with 1-3 agents indicate that our proposed approach returns 20% and 24% smaller average estimation errors for, respectively, monitoring water quality variables and monitoring algae blooms, as compared to state-of-the-art approaches △ Less

Submitted 9 January, 2024; originally announced January 2024.

Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics

Authors: Anupam Das, Iris van der Giessen, Sonia Marin

Abstract: We derive an intuitionistic version of Gödel-Löb modal logic ($\sf{GL}$) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, $\sf{\ell IGL}$, by restricting a non-wellfounded labelled system for $\sf{GL}$ to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that $\sf{GL}$'s usual frame c… ▽ More We derive an intuitionistic version of Gödel-Löb modal logic ($\sf{GL}$) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, $\sf{\ell IGL}$, by restricting a non-wellfounded labelled system for $\sf{GL}$ to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that $\sf{GL}$'s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of $\sf{GL}$ are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that $\sf{\ell IGL}$ coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic $\sf{IGL}$. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of $\sf{IGL}$. △ Less

Submitted 1 September, 2023; originally announced September 2023.

Comments: 25 pages including 8 pages appendix, 4 figures

ACM Class: F.4.1

A Logical Interpretation of Asynchronous Multiparty Compatibility

Authors: Marco Carbone, Sonia Marin, Carsten Schürmann

Abstract: Session types are types for specifying the protocols that communicating processes must follow in a concurrent system. When composing two or more well-typed processes, a session typing system must check whether such processes are multiparty compatible, a property that guarantees that all sent messages are eventually received and no deadlock ever occurs. Previous work has shown that duality and the… ▽ More Session types are types for specifying the protocols that communicating processes must follow in a concurrent system. When composing two or more well-typed processes, a session typing system must check whether such processes are multiparty compatible, a property that guarantees that all sent messages are eventually received and no deadlock ever occurs. Previous work has shown that duality and the more general notion of coherence are sufficient syntactic conditions for guaranteeing the multiparty compatibility property. In this paper, following a propositions-as-types fashion which relates session types to linear logic, we generalise coherence to forwarders. Forwarders are processes that act as middleware by forwarding messages according to a given protocol. Our main result shows that forwarders not only generalise coherence, but fully capture all well-typed multiparty compatible processes. △ Less

Submitted 25 May, 2023; originally announced May 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:2112.07636

Intuitionistic S4 is decidable

Authors: Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, Lutz Straßburger

Abstract: In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson's PhD thesis in 1994. We obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one cor… ▽ More In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson's PhD thesis in 1994. We obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area. △ Less

Submitted 24 April, 2023; originally announced April 2023.

Comments: 13 pages conference paper + 26 pages appendix with examples and proofs

Journal ref: Proceedings of LICS 2023 (2023)

InMyFace: Inertial and Mechanomyography-Based Sensor Fusion for Wearable Facial Activity Recognition

Authors: Hymalai Bello, Luis Alfredo Sanchez Marin, Sungho Suh, Bo Zhou, Paul Lukowicz

Abstract: Recognizing facial activity is a well-understood (but non-trivial) computer vision problem. However, reliable solutions require a camera with a good view of the face, which is often unavailable in wearable settings. Furthermore, in wearable applications, where systems accompany users throughout their daily activities, a permanently running camera can be problematic for privacy (and legal) reasons.… ▽ More Recognizing facial activity is a well-understood (but non-trivial) computer vision problem. However, reliable solutions require a camera with a good view of the face, which is often unavailable in wearable settings. Furthermore, in wearable applications, where systems accompany users throughout their daily activities, a permanently running camera can be problematic for privacy (and legal) reasons. This work presents an alternative solution based on the fusion of wearable inertial sensors, planar pressure sensors, and acoustic mechanomyography (muscle sounds). The sensors were placed unobtrusively in a sports cap to monitor facial muscle activities related to facial expressions. We present our integrated wearable sensor system, describe data fusion and analysis methods, and evaluate the system in an experiment with thirteen subjects from different cultural backgrounds (eight countries) and both sexes (six women and seven men). In a one-model-per-user scheme and using a late fusion approach, the system yielded an average F1 score of 85.00% for the case where all sensing modalities are combined. With a cross-user validation and a one-model-for-all-user scheme, an F1 score of 79.00% was obtained for thirteen participants (six females and seven males). Moreover, in a hybrid fusion (cross-user) approach and six classes, an average F1 score of 82.00% was obtained for eight users. The results are competitive with state-of-the-art non-camera-based solutions for a cross-user study. In addition, our unique set of participants demonstrates the inclusiveness and generalizability of the approach. △ Less

Submitted 8 February, 2023; originally announced February 2023.

Comments: Submitted to Information Fusion, Elsevier

Journal ref: Information Fusion Elsevier 2023

Censored Deep Reinforcement Patrolling with Information Criterion for Monitoring Large Water Resources using Autonomous Surface Vehicles

Authors: Samuel Yanes Luis, Daniel Gutiérrez Reina, Sergio Toral Marín

Abstract: Monitoring and patrolling large water resources is a major challenge for conservation. The problem of acquiring data of an underlying environment that usually changes within time involves a proper formulation of the information. The use of Autonomous Surface Vehicles equipped with water quality sensor modules can serve as an early-warning system agents for contamination peak-detection, algae bloom… ▽ More Monitoring and patrolling large water resources is a major challenge for conservation. The problem of acquiring data of an underlying environment that usually changes within time involves a proper formulation of the information. The use of Autonomous Surface Vehicles equipped with water quality sensor modules can serve as an early-warning system agents for contamination peak-detection, algae blooms monitoring, or oil-spill scenarios. In addition to information gathering, the vehicle must plan routes that are free of obstacles on non-convex maps. This work proposes a framework to obtain a collision-free policy that addresses the patrolling task for static and dynamic scenarios. Using information gain as a measure of the uncertainty reduction over data, it is proposed a Deep Q-Learning algorithm improved by a Q-Censoring mechanism for model-based obstacle avoidance. The obtained results demonstrate the usefulness of the proposed algorithm for water resource monitoring for static and dynamic scenarios. Simulations showed the use of noise-networks are a good choice for enhanced exploration, with 3 times less redundancy in the paths. Previous coverage strategies are also outperformed both in the accuracy of the obtained contamination model by a 13% on average and by a 37% in the detection of dangerous contamination peaks. Finally, these results indicate the appropriateness of the proposed framework for monitoring scenarios with autonomous vehicles. △ Less

Submitted 12 October, 2022; originally announced October 2022.

Comments: This article is currently under revision for the Applied Soft Computing Journal (Elsevier)

Separability and harmony in ecumenical systems

Authors: Sonia Marin, Luiz Carlos Pereira, Elaine Pimentel, Emerson Sales

Abstract: The quest of smoothly combining logics so that connectives from classical and intuitionistic logics can co-exist in peace has been a fascinating topic of research for decades now. In 2015, Dag Prawitz proposed a natural deduction system for an ecumenical first-order logic. We start this work by proposing a {\em pure} sequent calculus version for it, in the sense that connectives are introduced wit… ▽ More The quest of smoothly combining logics so that connectives from classical and intuitionistic logics can co-exist in peace has been a fascinating topic of research for decades now. In 2015, Dag Prawitz proposed a natural deduction system for an ecumenical first-order logic. We start this work by proposing a {\em pure} sequent calculus version for it, in the sense that connectives are introduced without the use of other connectives. For doing this, we extend sequents with an extra context, the stoup, and define the ecumenical notion of polarities. Finally, we smoothly extend these ideas for handling modalities, presenting pure labeled and nested systems for ecumenical modal logics. △ Less

Submitted 5 April, 2022; originally announced April 2022.

Comments: 26 pages

MSC Class: F.4.1

Advancing an Interdisciplinary Science of Conversation: Insights from a Large Multimodal Corpus of Human Speech

Authors: Andrew Reece, Gus Cooney, Peter Bull, Christine Chung, Bryn Dawson, Casey Fitzpatrick, Tamara Glazer, Dean Knox, Alex Liebscher, Sebastian Marin

Abstract: People spend a substantial portion of their lives engaged in conversation, and yet our scientific understanding of conversation is still in its infancy. In this report we advance an interdisciplinary science of conversation, with findings from a large, novel, multimodal corpus of 1,656 recorded conversations in spoken English. This 7+ million word, 850 hour corpus totals over 1TB of audio, video,… ▽ More People spend a substantial portion of their lives engaged in conversation, and yet our scientific understanding of conversation is still in its infancy. In this report we advance an interdisciplinary science of conversation, with findings from a large, novel, multimodal corpus of 1,656 recorded conversations in spoken English. This 7+ million word, 850 hour corpus totals over 1TB of audio, video, and transcripts, with moment-to-moment measures of vocal, facial, and semantic expression, along with an extensive survey of speaker post conversation reflections. We leverage the considerable scope of the corpus to (1) extend key findings from the literature, such as the cooperativeness of human turn-taking; (2) define novel algorithmic procedures for the segmentation of speech into conversational turns; (3) apply machine learning insights across various textual, auditory, and visual features to analyze what makes conversations succeed or fail; and (4) explore how conversations are related to well-being across the lifespan. We also report (5) a comprehensive mixed-method report, based on quantitative analysis and qualitative review of each recording, that showcases how individuals from diverse backgrounds alter their communication patterns and find ways to connect. We conclude with a discussion of how this large-scale public dataset may offer new directions for future research, especially across disciplinary boundaries, as scholars from a variety of fields appear increasingly interested in the study of conversation. △ Less

Submitted 1 March, 2022; originally announced March 2022.

Comments: 116 pages; Cross-posted to PsyArxiv; To request data access, go to https://betterup-data-requests.herokuapp.com/

Forwarders as Process Compatibility, Logically

Authors: Marco Carbone, Sonia Marin, Carsten Schürmann

Abstract: Session types define protocols that processes must follow when communicating. The special case of binary session types, i.e. type annotations of protocols between two parties, is known to be in a propositions-as-types correspondence with linear logic. In previous work, we have shown that the generalization to multiparty session types can be expressed either by coherence proofs or by arbiters, proc… ▽ More Session types define protocols that processes must follow when communicating. The special case of binary session types, i.e. type annotations of protocols between two parties, is known to be in a propositions-as-types correspondence with linear logic. In previous work, we have shown that the generalization to multiparty session types can be expressed either by coherence proofs or by arbiters, processes that act as middleware by forwarding messages according to the given protocol. In this paper, following the propositions-as-types fashion, we generalize arbiters to a logic, which we call forwarder logic, a fragment of classical linear logic still satisfying cut-elimination. Our main result is summarized as follows: forwarders generalize coherence and give an elegant proof-theoretic characterization of multiparty compatibility, a property of concurrent systems guaranteeing that all sent messages are eventually received and no deadlock ever occurs. △ Less

Submitted 14 December, 2021; originally announced December 2021.

Health Detection on Cattle Compressed Images in Precision Livestock Farming

Authors: Miguel Angel Calvache, Valeria Cardona, Sebastian Tapias, Simon Marin, Mauricio Toro

Abstract: The constant population growth brings the needing to make up for food also grows at the same rate. The livestock provides one-third of humans protein base as meat and milk. To improve cattles health and welfare the pastoral farming employs Precision Livestock farming (PLF). This technique implementation brings a challenge to minimize energy consumption due to farmers not having enough energy or de… ▽ More The constant population growth brings the needing to make up for food also grows at the same rate. The livestock provides one-third of humans protein base as meat and milk. To improve cattles health and welfare the pastoral farming employs Precision Livestock farming (PLF). This technique implementation brings a challenge to minimize energy consumption due to farmers not having enough energy or devices to transmit large volumes of information at the size are received from their farms monitors. Therefore, in this project, we will design an algorithm to compress and decompress images reducing energy consumption with the less information lost. Initially, the related problems have been read and analyzed to learn about the techniques used in the past and to be updated with the current works. We implemented Seam Carving and LZW algorithms. The compression of all images, around 1000 takes a time of 5 hours 10 min. We got a compression rate of 1.82:1 with 13.75s average time for each file and a decompression rate of 1.64:1 and 7.5 s average time for each file. The memory consumption we obtained was between 146MB and 504 MB and time consumption was between 30,5s for 90MB to 12192s for 24410 MB, it was all files. △ Less

Submitted 22 November, 2021; originally announced December 2021.

Comments: 8 pages, 10 images, 2 figures

MSC Class: 68Wxx ACM Class: E.1; E.4

Synchronous Forwarders

Authors: Marco Carbone, Sonia Marin, Carsten Schürmann

Abstract: Session types are types for specifying protocols that processes must follow when communicating with each other. Session types are in a propositions-as-types correspondence with linear logic. Previous work has shown that a multiparty session type, a generalisation of session types to protocols of two or more parties, can be modelled as a proof of coherence, a generalisation of linear logic duality.… ▽ More Session types are types for specifying protocols that processes must follow when communicating with each other. Session types are in a propositions-as-types correspondence with linear logic. Previous work has shown that a multiparty session type, a generalisation of session types to protocols of two or more parties, can be modelled as a proof of coherence, a generalisation of linear logic duality. And, protocols expressed as coherence can be simulated by arbiters, processes that act as a middleware by forwarding messages according to the given protocol. In this paper, we generalise the concept of arbiter to that of synchronous forwarder, that is a processes that implements the behaviour of an arbiter in several different ways. In a propositions-as-types fashion, synchronous forwarders form a logic equipped with cut elimination which is a special restriction of classical linear logic. Our main result shows that synchronous forwarders are a characterisation of coherence, i.e., coherence proofs can be transformed into synchronous forwarders and, viceversa, every synchronous forwarder corresponds to a coherence proofs. △ Less

Submitted 9 February, 2021; originally announced February 2021.

Focused Proof-search in the Logic of Bunched Implications

Authors: Alexander Gheorghiu, Sonia Marin

Abstract: The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper, we show that focused proof-sear… ▽ More The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper, we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications. △ Less

Submitted 26 January, 2021; v1 submitted 16 October, 2020; originally announced October 2020.

Comments: 18 pages content

MSC Class: 03F08 ACM Class: F.3; F.4; I.1

Journal ref: FoSSaCs 2020

Ecumenical modal logic

Authors: Sonia Marin, Luiz Carlos Pereira, Elaine Pimentel, Emerson Sales

Abstract: The discussion about how to put together Gentzen's systems for classical and intuitionistic logic in a single unified system is back in fashion. Indeed, recently Prawitz and others have been discussing the so called Ecumenical Systems, where connectives from these logics can co-exist in peace. In Prawitz' system, the classical logician and the intuitionistic logician would share the universal quan… ▽ More The discussion about how to put together Gentzen's systems for classical and intuitionistic logic in a single unified system is back in fashion. Indeed, recently Prawitz and others have been discussing the so called Ecumenical Systems, where connectives from these logics can co-exist in peace. In Prawitz' system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation, and the constant for the absurd, but they would each have their own existential quantifier, disjunction, and implication, with different meanings. Prawitz' main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. In a recent work, Ecumenical sequent calculi and a nested system were presented, and some very interesting proof theoretical properties of the systems were established. In this work we extend Prawitz' Ecumenical idea to alethic K-modalities. △ Less

Submitted 28 May, 2020; originally announced May 2020.

MSC Class: 03B45; 03F03 ACM Class: F.4.1