Showing 1–27 of 27 results for author: Veres, M

Flaires: A Comprehensive Catalog of Dust-Echo-like Infrared Flares

Authors: Jannis Necker, Eleni Graikou, Marek Kowalski, Anna Franckowiak, Jakob Nordin, Teresa Pernice, Sjoert van Velzen, Patrik M. Veres

Abstract: Context: Observations of transient emission from extreme accretion events onto supermassive black holes can reveal conditions in the center of galaxies and the black hole itself. Most recently, they have been suggested to be emitters of high-energy neutrinos. If it is suddenly rejuvenated accretion or a tidal disruption event (TDE) is not clear in most cases. Aims: We expanded on existing samples… ▽ More Context: Observations of transient emission from extreme accretion events onto supermassive black holes can reveal conditions in the center of galaxies and the black hole itself. Most recently, they have been suggested to be emitters of high-energy neutrinos. If it is suddenly rejuvenated accretion or a tidal disruption event (TDE) is not clear in most cases. Aims: We expanded on existing samples of infrared flares to compile the largest and most complete list available. A large sample size is necessary to provide high enough statistics for far away and faint objects to estimate their rate. Our catalog is large enough to facilitate a preliminary study of the rate evolution with redshift for the first time. Methods: We compiled a sample of 40 million galaxies, and, using a custom, publicly available pipeline, analyzed the WISE light curves for these 40 million objects using the Bayesian Blocks algorithm. We selected promising candidates for dust echos of transient accretion events and inferred the luminosity, extension, and temperature of the hot dust by fitting a blackbody spectrum. Results: We established a clean sample of 823 dust-echo-like infrared flares, of which we can estimate the dust properties for 568. After removing 70 objects with possible contribution by synchrotron emission, the luminosity, extension, and temperature are consistent with dust echos. Estimating the dust extension from the light curve shape revealed that the duration of the incident flare is broadly compatible with the duration of TDEs. The resulting rate per galaxy is consistent with the latest measurements of infrared-detected TDEs and appears to decline at increasing redshift. Conclusions: Although systematic uncertainties may impact the calculation of the rate evolution, this catalog will enable further research in phenomena related to dust-echos from TDEs and extreme accretion flares. △ Less

Submitted 1 July, 2024; originally announced July 2024.

Comments: 23 pages, 11 figures, to be submitted to A&A

Pulsed laser intensity dependence of crater formation and light reflection in the UDMA-TEGDMA copolymer nanocomposite, doped with resonant plasmonic gold nanorods

Authors: Ágnes Nagyné Szokol, Judit Kámán, Roman Holomb, Márk Aladi, Miklós Kedves, Béla Ráczkevi, Péter Rácz, Attila Bonyár, Alexandra Borók, Shereen Zangana, Melinda Szalóki, István Papp, Gábor Galbács, Tamás S. Biró, László P. Csernai, Norbert Kroó, Miklós Veres, NAPLIFE Collaboration

Abstract: Plasmonic nanoparticles embedded into a solid matrix could play crucial role in laser-matter interactions. In this study, excess energy creation was observed during the single-shot irradiation of a polymer matrix containing plasmonic gold nanorods, resonant to the laser wavelength, with a high intensity femtosecond laser pulse. This effect was manifested in a 7-fold rise in the crater volume for a… ▽ More Plasmonic nanoparticles embedded into a solid matrix could play crucial role in laser-matter interactions. In this study, excess energy creation was observed during the single-shot irradiation of a polymer matrix containing plasmonic gold nanorods, resonant to the laser wavelength, with a high intensity femtosecond laser pulse. This effect was manifested in a 7-fold rise in the crater volume for a 1.7-fold increase of the laser intensity, and was absent in the pure polymer without the gold do**. It occurred at laser intensities > 1.5 x 1017 W/cm2, being the vanishing threshold of plasma mirror formation, resulting in a more than 80% increase of the amount of laser light entering the target. This threshold was found to be critical for the plasmonic effect of gold nanoantennas tuned to the wavelength of the laser on the crater formation. △ Less

Submitted 28 February, 2024; originally announced February 2024.

Comments: 13 pages, 5 figures

European VLBI Network observations of the peculiar radio source 4C 35.06 overlap** with a compact group of nine galaxies

Authors: Patrik Milán Veres, Krisztina Éva Gabányi, Sándor Frey, Zsolt Paragi, Tao An, Joydeep Bagchi, Ákos Bogdán, K. G. Biju, Emma Kun, Joe Jacob, Björn Adebahr

Abstract: Context. According to the hierarchical structure formation model, brightest cluster galaxies (BCGs) evolve into the most luminous and massive galaxies in the Universe through multiple merger events. The peculiar radio source 4C 35.06 is located at the core of the galaxy cluster Abell 407, overlap** with a compact group of nine galaxies. Low-frequency radio observations have revealed a helical, s… ▽ More Context. According to the hierarchical structure formation model, brightest cluster galaxies (BCGs) evolve into the most luminous and massive galaxies in the Universe through multiple merger events. The peculiar radio source 4C 35.06 is located at the core of the galaxy cluster Abell 407, overlap** with a compact group of nine galaxies. Low-frequency radio observations have revealed a helical, steep-spectrum, kiloparsec-scale jet structure and inner lobes with less steep spectra, compatible with a recurring active galactic nucleus (AGN) activity scenario. However, the host galaxy of the AGN responsible for the detected radio emission remained unclear. Aims. We aim to identify the host of 4C 35.06 by studying the object at high angular resolution and thereby confirm the recurrent AGN activity scenario. Methods. To reveal the host of the radio source, we carried out very long baseline interferometry (VLBI) observations with the European VLBI Network of the nine galaxies in the group at 1.7 and 4.9 GHz. Results. We detected compact radio emission from an AGN located between the two inner lobes at both observing frequencies. In addition, we detected another galaxy at 1.7 GHz, whose position appears more consistent with the principal jet axis and is located closer to the low-frequency radio peak of 4C 35.06. The presence of another radio-loud AGN in the nonet sheds new light on the BCG formation and provides an alternative scenario in which not just one but two AGNs are responsible for the complex large-scale radio structure △ Less

Submitted 20 February, 2024; originally announced February 2024.

Comments: accepted for publication in Astronomy & Astrophysics (A&A), 7 pages, 4 figures, 2 tables

Monitoring of nanoplasmonics-assisted deuterium production in a polymer seeded with resonant Au nanorods using in situ femtosecond laser induced breakdown spectroscopy

Authors: N. Kroó, M. Aladi, M. Kedves, B. Ráczkevi, A. Kumari, P. Rácz, M. Veres, G. Galbács, L. P. Csernai, T. S. Biró

Abstract: In this brief report, we present laser induced breakdown spectroscopy (LIBS) evidence of deuterium (D) production in a 3:1 urethane dimethacrylate (UDMA) and triethylene glycol dimethacrylate (TEGDMA) polymer doped with resonant gold nanorods, induced by intense, 40 fs laser pulses. The in situ recorded LIBS spectra revealed that the D/(2D+H) increased to 4-8% in the polymer samples in selected ev… ▽ More In this brief report, we present laser induced breakdown spectroscopy (LIBS) evidence of deuterium (D) production in a 3:1 urethane dimethacrylate (UDMA) and triethylene glycol dimethacrylate (TEGDMA) polymer doped with resonant gold nanorods, induced by intense, 40 fs laser pulses. The in situ recorded LIBS spectra revealed that the D/(2D+H) increased to 4-8% in the polymer samples in selected events. The extent of transmutation was found to linearly increase with the laser pulse energy (intensity) between 2 and 25 mJ (up to 3x10^17 W/cm). The observed effect is attributed only to the field enhancing effects due to excited localized surface plasmons on the gold nanoparticles. △ Less

Submitted 27 December, 2023; originally announced December 2023.

Crater Formation and Deuterium Production in Laser Irradiation of Polymers with Implanted Nano-antennas

Authors: L. P. Csernai, I. N. Mishustin, L. M. Satarov, H. Stoecker, L. Bravina, M. Csete, J. Kaman, A. Kumari, A. Motornenko, I. Papp, P. Racz, D. D. Strottman, A. Scenes, A. Szokol, D. Vass, M. Veres, T. S. Biro, N. Kroo

Abstract: Recent validation experiments on laser irradiation of polymer foils with and without implanted golden nano-particles are discussed. First we analyze characteristics of craters, formed in the target after its interaction with laser beam. Preliminary experimental results show significant production of deuterons when both the energy of laser pulse and concentration of nano-particles are high enough.… ▽ More Recent validation experiments on laser irradiation of polymer foils with and without implanted golden nano-particles are discussed. First we analyze characteristics of craters, formed in the target after its interaction with laser beam. Preliminary experimental results show significant production of deuterons when both the energy of laser pulse and concentration of nano-particles are high enough. We consider the deuteron production via the nuclear transmutation reactions $p+C\rightarrow d+X$ where protons are accelerated by Coulomb field, generated in the target plasma. We argue that maximal proton energy can be above threshold values for these reactions and the deuteron yield may noticeably increase due to presence of nano-particles. △ Less

Submitted 25 November, 2022; originally announced November 2022.

Comments: 9 pages, 4 figures

Raman spectroscopic characterization of crater walls formed upon single-shot high energy femtosecond laser irradiation of dimethacrylate polymer doped with plasmonic gold nanorods

Authors: István Rigó, Judit Kámán, Ágnes Nagyné Szokol, Attila Bonyár, Melinda Szalóki, Alexandra Borók, Shereen Zangana, Péter Rácz, Márk Aladi, Miklós Ákos Kedves, Gábor Galbács, László P. Csernai, Tamás S. Biró, Norbert Kroó, Miklós Veres, NAPLIFE Collaboration

Abstract: The bonding configuration of the crater walls formed in urethane dimethacrylate-based polymer doped with plasmonic gold nanorods upon irradiation with a single-shot high-energy femtosecond laser pulse has been studied by Raman spectroscopy. New Raman bands were detected in the 2000-2500 cm-1 region of the Raman spectrum the intensities of which showed strong dependence on the concentration of the… ▽ More The bonding configuration of the crater walls formed in urethane dimethacrylate-based polymer doped with plasmonic gold nanorods upon irradiation with a single-shot high-energy femtosecond laser pulse has been studied by Raman spectroscopy. New Raman bands were detected in the 2000-2500 cm-1 region of the Raman spectrum the intensities of which showed strong dependence on the concentration of the plasmonic nanoparticles and the energy of the laser pulse. Based on model calculations of the Raman frequencies of the polymer these peaks were attributed to carbon-deuterium and nitrogen-deuterium vibrations. Their appearance might indicate the occurrence of nuclear reactions in the polymer excited by the ultra-strong laser field amplified by the plasmonic nanoparticles. △ Less

Submitted 28 February, 2024; v1 submitted 2 October, 2022; originally announced October 2022.

Comments: 17 pages, 10 figures

Establishing accretion flares from massive black holes as a source of high-energy neutrinos

Authors: Sjoert van Velzen, Robert Stein, Marat Gilfanov, Marek Kowalski, Kimitake Hayasaki, Simeon Reusch, Yuhan Yao, Simone Garrappa, Anna Franckowiak, Suvi Gezari, Jakob Nordin, Christoffer Fremling, Yashvi Sharma, Lin Yan, Erik C. Kool, Daniel Stern, Patrik M. Veres, Jesper Sollerman, Pavel Medvedev, Rashid Sunyaev, Eric C. Bellm, Richard G. Dekany, Dimitri A. Duev, Matthew J. Graham, Mansi M. Kasliwal , et al. (4 additional authors not shown)

Abstract: The origin of cosmic high-energy neutrinos remains largely unexplained. For high-energy neutrino alerts from IceCube, a coincidence with time-variable emission has been seen for three different types of accreting black holes: (1) a gamma-ray flare from a blazar (TXS 0506+056), (2) an optical transient following a stellar tidal disruption event (TDE; AT2019dsg), and (3) an optical outburst from an… ▽ More The origin of cosmic high-energy neutrinos remains largely unexplained. For high-energy neutrino alerts from IceCube, a coincidence with time-variable emission has been seen for three different types of accreting black holes: (1) a gamma-ray flare from a blazar (TXS 0506+056), (2) an optical transient following a stellar tidal disruption event (TDE; AT2019dsg), and (3) an optical outburst from an active galactic nucleus (AGN; AT2019fdr). For the latter two sources, infrared follow-up observations revealed a powerful reverberation signal due to dust heated by the flare. This discovery motivates a systematic study of neutrino emission from all supermassive black hole with similar dust echoes. Because dust reprocessing is agnostic to the origin of the outburst, our work unifies TDEs and high-amplitude flares from AGN into a population that we dub accretion flares. Besides the two known events, we uncover a third flare that is coincident with a PeV-scale neutrino (AT2019aalc). Based solely on the optical and infrared properties, we estimate a significance of 3.6$σ$ for this association of high-energy neutrinos with three accretion flares. Our results imply that at least ~10% of the IceCube high-energy neutrino alerts could be due to accretion flares. This is surprising because the sum of the fluence of these flares is at least three orders of magnitude lower compared to the total fluence of normal AGN. It thus appears that the efficiency of high-energy neutrino production in accretion flares is increased compared to non-flaring AGN. We speculate that this can be explained by the high Eddington ratio of the flares. △ Less

Submitted 3 April, 2024; v1 submitted 17 November, 2021; originally announced November 2021.

Comments: Accepted for publication in MNRAS

Journal ref: Monthly Notices of the Royal Astronomical Society (2024), Volume 529, Issue 3, 2559-2576

European VLBI Network Observations of the Proposed Dual AGN SDSS J101022.95+141300.9

Authors: Patrik Milán Veres, Krisztina É. Gabányi, Sándor Frey, Zsolt Paragi, Emma Kun, Tao An

Abstract: During galaxy merger events, the supermassive black holes in the center of the galaxies may form a pair of active galactic nuclei (AGN) with kpc-scale or even pc-scale separation. Recently, optical observations revealed a promising dual AGN candidate at the center of the galaxy SDSS J101022.95$+$141300.9 (hereafter J1010$+$1413). The presence of two distinct [O III]-emitting point sources with a p… ▽ More During galaxy merger events, the supermassive black holes in the center of the galaxies may form a pair of active galactic nuclei (AGN) with kpc-scale or even pc-scale separation. Recently, optical observations revealed a promising dual AGN candidate at the center of the galaxy SDSS J101022.95$+$141300.9 (hereafter J1010$+$1413). The presence of two distinct [O III]-emitting point sources with a projected separation of $\sim 430$ pc indicates a dual AGN system. To search for AGN-dominated radio emission originating from the Hubble Space Telescope (HST) point sources, we carried out very long baseline interferometry observations. We resolved the radio structure of J1010$+$1413 and detected a single feature offset from the HST point sources and also from the Gaia optical position of the object. Our multi-wavelength analysis of J1010$+$1413 inferred two possible interpretations of the observed properties challenging its proposed dual AGN classification. △ Less

Submitted 19 October, 2021; originally announced October 2021.

Comments: accepted to ApJ 16 pages, 3 figures

Concepts of Self-maintaining Robots and Their Design

Authors: Chenjie Shi, Sandor M Veres

Abstract: This paper proposes an initial theory for robotic systems that can be fully self-maintaining. The new design principles focus on functional survival of the robots over long periods of time without human maintenance. Self-maintaining semi-autonomous mobile robots are in great demand in nuclear disposal sites from where their removal for maintenance is undesirable due to their radioactive contaminat… ▽ More This paper proposes an initial theory for robotic systems that can be fully self-maintaining. The new design principles focus on functional survival of the robots over long periods of time without human maintenance. Self-maintaining semi-autonomous mobile robots are in great demand in nuclear disposal sites from where their removal for maintenance is undesirable due to their radioactive contamination. Similar are requirements for robots in various defence tasks or space missions. For optimal design, modular solutions are balanced against capabilities to replace smaller components in a robot by itself or by help from another robot. Modules are proposed for the basic platform, which enable self-maintenance within a team of robots hel** each other. The primary method of self-maintenance is replacement of malfunctioning modules or components by the robots themselves. Replacement necessitates a robot team's ability to diagnose and replace malfunctioning modules as needed. Due to their design, these robots still remain manually re-configurable if opportunity arises for human intervention. Apart from the basic principles, an evolutionary design approach is presented and a first mathematical theory of the reliability of a team of self-maintaining robots is introduced. △ Less

Submitted 12 October, 2021; originally announced October 2021.

Very Long Baseline Interferometry Observations of the Proposed Radio Counterpart of an EGRET Source

Authors: Patrik Milán Veres, Krisztina Éva Gabányi, Sándor Frey

Abstract: We present high-resolution radio interferometric imaging observations of the radio source NVSS J182659+343113 (hereafter J1826+3431), the proposed radio counterpart of the $γ$-ray source, 3EG J1824+3441 detected by the Energetic Gamma Ray Experiment Telescope (EGRET) on board the Compton Gamma Ray Observatory satellite. We analyzed eight epochs of archival multi-frequency very long baseline interf… ▽ More We present high-resolution radio interferometric imaging observations of the radio source NVSS J182659+343113 (hereafter J1826+3431), the proposed radio counterpart of the $γ$-ray source, 3EG J1824+3441 detected by the Energetic Gamma Ray Experiment Telescope (EGRET) on board the Compton Gamma Ray Observatory satellite. We analyzed eight epochs of archival multi-frequency very long baseline interferometry data. We imaged the asymmetric core-jet structure of the source, and detected apparent superluminal motion in the jet. At the highest observing frequency, 15.3 GHz, the core shows high brightness temperature indicating Doppler boosting. Additionally, the radio features undergo substantial flux density variability. These findings strengthen the previous claim of the association of the blazar J1826+3431 with the possible $γ$-ray source, 3EG J1824+3441. △ Less

Submitted 15 September, 2020; originally announced September 2020.

Journal ref: Symmetry 2020, 12, 1516

Verification Framework for Control System Functionality of Unmanned Aerial Vehicles

Authors: Omar A. Jasim, Sandor M. Veres

Abstract: A control system verification framework is presented for unmanned aerial vehicles using theorem proving. The framework's aim is to set out a procedure for proving that the mathematically designed control system of the aircraft satisfies robustness requirements to ensure safe performance under varying environmental conditions. Extensive mathematical derivations, which have formerly been carried out… ▽ More A control system verification framework is presented for unmanned aerial vehicles using theorem proving. The framework's aim is to set out a procedure for proving that the mathematically designed control system of the aircraft satisfies robustness requirements to ensure safe performance under varying environmental conditions. Extensive mathematical derivations, which have formerly been carried out manually, are checked for their correctness on a computer. To illustrate the proceedures, a higher-order logic interactive theorem-prover and an automated theorem-prover are utilized to formally verify a nonlinear attitude control system of a generic multi-rotor UAV over a stability domain within the dynamical state space of the drone. Further benefits of the proceedures are that some of the resulting methods can be implemented onboard the aircraft to detect when its controller breaches its flight envelop limits due to severe weather conditions or actuator/sensor malfunction. Such a detection procedure can be used to advise the remote pilot or an onboard intelligent agent to decide on some alterations of the planned flight path or to perform emergency landing. △ Less

Submitted 18 June, 2020; originally announced June 2020.

An Integrated Simulator and Dataset that Combines Gras** and Vision for Deep Learning

Authors: Matthew Veres, Medhat Moussa, Graham W. Taylor

Abstract: Deep learning is an established framework for learning hierarchical data representations. While compute power is in abundance, one of the main challenges in applying this framework to robotic gras** has been obtaining the amount of data needed to learn these representations, and structuring the data to the task at hand. Among contemporary approaches in the literature, we highlight key properties… ▽ More Deep learning is an established framework for learning hierarchical data representations. While compute power is in abundance, one of the main challenges in applying this framework to robotic gras** has been obtaining the amount of data needed to learn these representations, and structuring the data to the task at hand. Among contemporary approaches in the literature, we highlight key properties that have encouraged the use of deep learning techniques, and in this paper, detail our experience in develo** a simulator for collecting cylindrical precision grasps of a multi-fingered dexterous robotic hand. △ Less

Submitted 17 April, 2017; v1 submitted 7 February, 2017; originally announced February 2017.

Modeling Grasp Motor Imagery through Deep Conditional Generative Models

Authors: Matthew Veres, Medhat Moussa, Graham W. Taylor

Abstract: Gras** is a complex process involving knowledge of the object, the surroundings, and of oneself. While humans are able to integrate and process all of the sensory information required for performing this task, equip** machines with this capability is an extremely challenging endeavor. In this paper, we investigate how deep learning techniques can allow us to translate high-level concepts such… ▽ More Gras** is a complex process involving knowledge of the object, the surroundings, and of oneself. While humans are able to integrate and process all of the sensory information required for performing this task, equip** machines with this capability is an extremely challenging endeavor. In this paper, we investigate how deep learning techniques can allow us to translate high-level concepts such as motor imagery to the problem of robotic grasp synthesis. We explore a paradigm based on generative models for learning integrated object-action representations, and demonstrate its capacity for capturing and generating multimodal, multi-finger grasp configurations on a simulated gras** dataset. △ Less

Submitted 11 January, 2017; originally announced January 2017.

Comments: Accepted for publication in Robotics and Automation Letters (RA-L)

SMCL - Stochastic Model Checker for Learning in Games

Authors: Hongyang Qu, Michalis Smyrnakis, Sandor M. Veres

Abstract: A stochastic model checker is presented for analysing the performance of game-theoretic learning algorithms. The method enables the comparison of short-term behaviour of learning algorithms intended for practical use. The procedure of comparison is automated and it can be tuned for accuracy and speed. Users can choose from among various learning algorithms to select a suitable one for a given prac… ▽ More A stochastic model checker is presented for analysing the performance of game-theoretic learning algorithms. The method enables the comparison of short-term behaviour of learning algorithms intended for practical use. The procedure of comparison is automated and it can be tuned for accuracy and speed. Users can choose from among various learning algorithms to select a suitable one for a given practical problem. The powerful performance of the method is enabled by a novel behaviour-similarity-relation, which compacts large state spaces into small ones. The stochastic model checking tool is tested on a set of examples classified into four categories to demonstrate the effectiveness of selecting suitable algorithms for distributed decision making. △ Less

Submitted 10 November, 2016; originally announced November 2016.

Fictitious play for cooperative action selection in robot teams

Authors: Michalis Smyrnakis, Sandor M. Veres

Abstract: A game theoretic distributed decision making approach is presented for the problem of control effort allocation in a robotic team based on a novel variant of fictitious play. The proposed learning process allows the robots to accomplish their objectives by coordinating their actions in order to efficiently complete their tasks. In particular, each robot of the team predicts the other robots' plann… ▽ More A game theoretic distributed decision making approach is presented for the problem of control effort allocation in a robotic team based on a novel variant of fictitious play. The proposed learning process allows the robots to accomplish their objectives by coordinating their actions in order to efficiently complete their tasks. In particular, each robot of the team predicts the other robots' planned actions while making decisions to maximise their own expected reward that depends on the reward for joint successful completion of the task. Action selection is interpreted as an $n$-player cooperative game. The approach presented can be seen as part of the \emph{Belief Desire Intention} (BDI) framework, also can address the problem of cooperative, legal, safe, considerate and emphatic decisions by robots if their individual and group rewards are suitably defined. After theoretical analysis the performance of the proposed algorithm is tested on four simulation scenarios. The first one is a coordination game between two material handling robots, the second one is a warehouse patrolling task by a team of robots, the third one presents a coordination mechanism between two robots that carry a heavy object on a corridor and the fourth one is an example of coordination on a sensors network. △ Less

Submitted 17 November, 2016; originally announced November 2016.

Comments: arXiv admin note: text overlap with arXiv:1301.3347

Journal ref: Engineering Applications of Artificial Intelligence, Volume 56, November 2016, Pages 14-29

A stochastically verifiable autonomous control architecture with reasoning

Authors: Paolo Izzo, Hongyang Qu, Sandor M. Veres

Abstract: A new agent architecture called Limited Instruction Set Agent (LISA) is introduced for autonomous control. The new architecture is based on previous implementations of AgentSpeak and it is structurally simpler than its predecessors with the aim of facilitating design-time and run-time verification methods. The process of abstracting the LISA system to two different types of discrete probabilistic… ▽ More A new agent architecture called Limited Instruction Set Agent (LISA) is introduced for autonomous control. The new architecture is based on previous implementations of AgentSpeak and it is structurally simpler than its predecessors with the aim of facilitating design-time and run-time verification methods. The process of abstracting the LISA system to two different types of discrete probabilistic models (DTMC and MDP) is investigated and illustrated. The LISA system provides a tool for complete modelling of the agent and the environment for probabilistic verification. The agent program can be automatically compiled into a DTMC or a MDP model for verification with Prism. The automatically generated Prism model can be used for both design-time and run-time verification. The run-time verification is investigated and illustrated in the LISA system as an internal modelling mechanism for prediction of future outcomes. △ Less

Submitted 10 November, 2016; originally announced November 2016.

Comments: Accepted at IEEE Conf. Decision and Control, 2016

Testing, Verification and Improvements of Timeliness in ROS processes

Authors: Mohammed Y. Hazim, Hongyang Qu, Sandor M. Veres

Abstract: This paper addresses the problem of improving response times of robots implemented in the Robotic Operating System (ROS) using formal verification of computational-time feasibility. In order to verify the real time behaviour of a robot under uncertain signal processing times, methods of formal verification of timeliness properties are proposed for data flows in a ROS-based control system using Pro… ▽ More This paper addresses the problem of improving response times of robots implemented in the Robotic Operating System (ROS) using formal verification of computational-time feasibility. In order to verify the real time behaviour of a robot under uncertain signal processing times, methods of formal verification of timeliness properties are proposed for data flows in a ROS-based control system using Probabilistic Timed Programs (PTPs). To calculate the probability of success under certain time limits, and to demonstrate the strength of our approach, a case study is implemented for a robotic agent in terms of operational times verification using the PRISM model checker, which points to possible enhancements to the operation of the robotic agent. △ Less

Submitted 10 November, 2016; originally announced November 2016.

Comments: 13 pages, 4 figures

Journal ref: TAROS Conference, Volume 9716 of the series Lecture Notes in Computer Science pp 146-157, 2016

Verification of Logical Consistency in Robotic Reasoning

Authors: Hongyang Qu, Sandor M. Veres

Abstract: Most autonomous robotic agents use logic inference to keep themselves to safe and permitted behaviour. Given a set of rules, it is important that the robot is able to establish the consistency between its rules, its perception-based beliefs, its planned actions and their consequences. This paper investigates how a robotic agent can use model checking to examine the consistency of its rules, belief… ▽ More Most autonomous robotic agents use logic inference to keep themselves to safe and permitted behaviour. Given a set of rules, it is important that the robot is able to establish the consistency between its rules, its perception-based beliefs, its planned actions and their consequences. This paper investigates how a robotic agent can use model checking to examine the consistency of its rules, beliefs and actions. A rule set is modelled by a Boolean evolution system with synchronous semantics, which can be translated into a labelled transition system (LTS). It is proven that stability and consistency can be formulated as computation tree logic (CTL) and linear temporal logic (LTL) properties. Two new algorithms are presented to perform realtime consistency and stability checks respectively. Their implementation provides us a computational tool, which can form the basis of efficient consistency checks on-board robots. △ Less

Submitted 10 November, 2016; originally announced November 2016.

Journal ref: Robotics and Autonomous Systems, Vol. 83(2016), 44-56

Dynamical Behavior Investigation and Analysis of Novel Mechanism for Simulated Spherical Robot named "RollRoller"

Authors: Seyed Amir Tafrishi, Sandor M. Veres, Esmaeil Esmaeilzadeh, Mikhail Svinin

Abstract: This paper introduces a simulation study of fluid actuated multi-driven closed system as spherical mobile robot called "RollRoller". Robot's mechanism design consists of two essential parts: tubes to lead a core and mechanical controlling parts to correspond movements. Our robot gets its motivation force by displacing the spherical movable mass known as core in curvy manners inside certain pipes.… ▽ More This paper introduces a simulation study of fluid actuated multi-driven closed system as spherical mobile robot called "RollRoller". Robot's mechanism design consists of two essential parts: tubes to lead a core and mechanical controlling parts to correspond movements. Our robot gets its motivation force by displacing the spherical movable mass known as core in curvy manners inside certain pipes. This simulation investigates by explaining the mechanical and structural features of the robot for creating hydraulic-base actuation via force and momentum analysis. Next, we categorize difficult and integrated 2D motions to omit unstable equilibrium points through derived nonlinear dynamics. We propose an algorithmic position control in forward direction that creates hybrid model as solution for motion planning problem in spherical robot. By deriving nonlinear dynamics of the spherical robot and implementing designed motion planning, we show how RollRoller can be efficient in high speed movements in comparison to the other pendulum-driven models. Then, we validate the results of this position control obtained by nonlinear dynamics via Adams/view simulation which uses the imported solid model of RollRoller. Lastly, We have a look to the circular maneuver of this robot by the same simulator. △ Less

Submitted 19 October, 2016; originally announced October 2016.

Comments: 30 pages, 24 figures, submitted to Mechanism and Machine Theory

A Continuous-Time Model of an Autonomous Aerial Vehicle to Inform and Validate Formal Verification Methods

Authors: Murray L. Ireland, Ruth Hoffmann, Alice Miller, Gethin Norman, Sandor M. Veres

Abstract: If autonomous vehicles are to be widely accepted, we need to ensure their safe operation. For this reason, verification and validation (V&V) approaches must be developed that are suitable for this domain. Model checking is a formal technique which allows us to exhaustively explore the paths of an abstract model of a system. Using a probabilistic model checker such as PRISM, we may determine proper… ▽ More If autonomous vehicles are to be widely accepted, we need to ensure their safe operation. For this reason, verification and validation (V&V) approaches must be developed that are suitable for this domain. Model checking is a formal technique which allows us to exhaustively explore the paths of an abstract model of a system. Using a probabilistic model checker such as PRISM, we may determine properties such as the expected time for a mission, or the probability that a specific mission failure occurs. However, model checking of complex systems is difficult due to the loss of information during abstraction. This is especially so when considering systems such as autonomous vehicles which are subject to external influences. An alternative solution is the use of Monte Carlo simulation to explore the results of a continuous-time model of the system. The main disadvantage of this approach is that the approach is not exhaustive as not all executions of the system are analysed. We are therefore interested in develo** a framework for formal verification of autonomous vehicles, using Monte Carlo simulation to inform and validate our symbolic models during the initial stages of development. In this paper, we present a continuous-time model of a quadrotor unmanned aircraft undertaking an autonomous mission. We employ this model in Monte Carlo simulation to obtain specific mission properties which will inform the symbolic models employed in formal verification. △ Less

Submitted 1 September, 2016; originally announced September 2016.

Collision Avoidance of Two Autonomous Quadcopters

Authors: Michalis Smyrnakis, Jonathan M. Aitken, Sandor M. Veres

Abstract: Traffic collision avoidance systems (TCAS) are used in order to avoid incidences of mid-air collisions between aircraft. We present a game-theoretic approach of a TCAS designed for autonomous unmanned aerial vehicles (UAVs). A variant of the canonical example of game-theoretic learning, fictitious play, is used as a coordination mechanism between the UAVs, that should choose between the alternativ… ▽ More Traffic collision avoidance systems (TCAS) are used in order to avoid incidences of mid-air collisions between aircraft. We present a game-theoretic approach of a TCAS designed for autonomous unmanned aerial vehicles (UAVs). A variant of the canonical example of game-theoretic learning, fictitious play, is used as a coordination mechanism between the UAVs, that should choose between the alternative altitudes to fly and avoid collision. We present the implementation results of the proposed coordination mechanism in two quad-copters flying in opposite directions. △ Less

Submitted 17 March, 2016; originally announced March 2016.

Reducing complexity of autonomous control agents for verifiability

Authors: Paolo Izzo, Hongyang Qu, Sandor M. Veres

Abstract: The AgentSpeak type of languages are considered for decision making in autonomous control systems. To reduce the complexity and increase the verifiability of decision making, a limited instruction set agent (LISA) is introduced. The new decision method is structurally simpler than its predecessors and easily lends itself to both design time and runtime verification methods. The process of converti… ▽ More The AgentSpeak type of languages are considered for decision making in autonomous control systems. To reduce the complexity and increase the verifiability of decision making, a limited instruction set agent (LISA) is introduced. The new decision method is structurally simpler than its predecessors and easily lends itself to both design time and runtime verification methods. The process of converting a control agent in LISA into a model in a probabilistic model checker is described. Due to the practical complexity of design time verification the feasibility of runtime probabilistic verification is investigated and illustrated in the LISA agent programming system for verifying symbolic plans of the agent using a probabilistic model checker. △ Less

Submitted 3 March, 2016; originally announced March 2016.

Formal Verification of Autonomous Vehicle Platooning

Authors: Maryam Kamali, Louise A. Dennis, Owen McAree, Michael Fisher, Sandor M. Veres

Abstract: The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out b… ▽ More The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the agent code does not scale to the full system and as the global verification technique does not capture the essential verification of autonomous behavior, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles. △ Less

Submitted 4 February, 2016; originally announced February 2016.

Practical Verification of Decision-Making in Agent-Based Autonomous Systems

Authors: Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa, Sandor M. Veres

Abstract: We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex… ▽ More We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems. △ Less

Submitted 9 October, 2013; originally announced October 2013.

Comments: Submitted to Journal of Automated Software Engineering

MSC Class: 03B70

Centrality dependence of proton and antiproton spectra in Pb+Pb collisions at 40A GeV and 158A GeV measured at the CERN SPS

Authors: T. Anticic, B. Baatar, D. Barna, J. Bartke, H. Beck, L. Betev, H. Bialkowska, C. Blume, M. Bogusz, B. Boimska, J. Book, M. Botje, P. Buncic, T. Cetner, P. Christakoglou, P. Chung, O. Chvala, J. G. Cramer, V. Eckardt, Z. Fodor, P. Foka, V. Friese, M. Gazdzicki, K. Grebieszkow, C. Höhne , et al. (46 additional authors not shown)

Abstract: The yields of (anti-)protons were measured by the NA49 Collaboration in centrality selected Pb+Pb collisions at 40A GeV and 158A GeV. Particle identification was obtained in the laboratory momentum range from 5 to 63 GeV/c by the measurement of the energy loss dE/dx in the TPC detector gas. The corresponding rapidity coverage extends 1.6 units from mid-rapidity into the forward hemisphere. Transve… ▽ More The yields of (anti-)protons were measured by the NA49 Collaboration in centrality selected Pb+Pb collisions at 40A GeV and 158A GeV. Particle identification was obtained in the laboratory momentum range from 5 to 63 GeV/c by the measurement of the energy loss dE/dx in the TPC detector gas. The corresponding rapidity coverage extends 1.6 units from mid-rapidity into the forward hemisphere. Transverse mass spectra, the rapidity dependences of the average transverse mass, and rapidity density distributions were studied as a function of collision centrality. The values of the average transverse mass as well as the midrapidity yields of protons when normalized to the number of wounded nucleons show only modest centrality dependences. In contrast, the shape of the rapidity distribution changes significantly with collision centrality, especially at 40A GeV. The experimental results are compared to calculations of the HSD and UrQMD transport models. △ Less

Submitted 10 September, 2010; v1 submitted 9 September, 2010; originally announced September 2010.

Comments: 25 pages, 12 figures, submitted to PRC

Report number: CERN-PH-EP-2010-030

Journal ref: Phys.Rev.C83:014901,2011

Agent Based Approaches to Engineering Autonomous Space Software

Authors: Louise A. Dennis, Michael Fisher, Nicholas Lincoln, Alexei Lisitsa, Sandor M. Veres

Abstract: Current approaches to the engineering of space software such as satellite control systems are based around the development of feedback controllers using packages such as MatLab's Simulink toolbox. These provide powerful tools for engineering real time systems that adapt to changes in the environment but are limited when the controller itself needs to be adapted. We are investigating ways in wh… ▽ More Current approaches to the engineering of space software such as satellite control systems are based around the development of feedback controllers using packages such as MatLab's Simulink toolbox. These provide powerful tools for engineering real time systems that adapt to changes in the environment but are limited when the controller itself needs to be adapted. We are investigating ways in which ideas from temporal logics and agent programming can be integrated with the use of such control systems to provide a more powerful layer of autonomous decision making. This paper will discuss our initial approaches to the engineering of such systems. △ Less

Submitted 2 March, 2010; originally announced March 2010.

Comments: 3 pages, 1 Figure, Formal Methods in Aerospace

Journal ref: EPTCS 20, 2010, pp. 63-67

Charge-Generated Changes in Graphite Structures

Authors: I. Pocsik, M. Veres, M. Fule, S. Toth, M. Koos

Abstract: It will be shown that a negatively charged carbon atom in a graphite sheet has an electron structure that is unusual in carbons, viz. the lone pair of electrons. This atom, similarly to the positively charged ones, is no longer able to participate in the (pi) bond network: both pop out from the sheet because of their elongated single bonds and tetrahedral structure. The lone-pair structure local… ▽ More It will be shown that a negatively charged carbon atom in a graphite sheet has an electron structure that is unusual in carbons, viz. the lone pair of electrons. This atom, similarly to the positively charged ones, is no longer able to participate in the (pi) bond network: both pop out from the sheet because of their elongated single bonds and tetrahedral structure. The lone-pair structure localizes the extra electron. Forbidden gaps open above and below the Fermi level as a consequence of the destroyed (pi) bonds. This model offers an explanation for many anomalous experimental data. △ Less

Submitted 18 July, 2003; originally announced July 2003.