Showing 1–50 of 65 results for author: Ferrando, A

Solvent: liquidity verification of smart contracts

Authors: Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini, Vadim Malvone

Abstract: Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to with… ▽ More Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts. △ Less

Submitted 20 June, 2024; v1 submitted 27 April, 2024; originally announced April 2024.

VITAMIN: A Compositional Framework for Model Checking of Multi-Agent Systems

Authors: Angelo Ferrando, Vadim Malvone

Abstract: The verification of Multi-Agent Systems (MAS) poses a significant challenge. Various approaches and methodologies exist to address this challenge; however, tools that support them are not always readily available. Even when such tools are accessible, they tend to be hard-coded, lacking in compositionality, and challenging to use due to a steep learning curve. In this paper, we introduce a methodol… ▽ More The verification of Multi-Agent Systems (MAS) poses a significant challenge. Various approaches and methodologies exist to address this challenge; however, tools that support them are not always readily available. Even when such tools are accessible, they tend to be hard-coded, lacking in compositionality, and challenging to use due to a steep learning curve. In this paper, we introduce a methodology designed for the formal verification of MAS in a modular and versatile manner, along with an initial prototype, that we named VITAMIN. Unlike existing verification methodologies and frameworks for MAS, VITAMIN is constructed for easy extension to accommodate various logics (for specifying the properties to verify) and models (for determining on what to verify such properties). △ Less

Submitted 4 July, 2024; v1 submitted 4 March, 2024; originally announced March 2024.

3vLTL: A Tool to Generate Automata for Three-valued LTL

Authors: Francesco Belardinelli, Angelo Ferrando, Vadim Malvone

Abstract: Multi-valued logics have a long tradition in the literature on system verification, including run-time verification. However, comparatively fewer model-checking tools have been developed for multi-valued specification languages. We present 3vLTL, a tool to generate Buchi automata from formulas in Linear-time Temporal Logic (LTL) interpreted on a three-valued semantics. Given an LTL formula, a set… ▽ More Multi-valued logics have a long tradition in the literature on system verification, including run-time verification. However, comparatively fewer model-checking tools have been developed for multi-valued specification languages. We present 3vLTL, a tool to generate Buchi automata from formulas in Linear-time Temporal Logic (LTL) interpreted on a three-valued semantics. Given an LTL formula, a set of atomic propositions as the alphabet for the automaton, and a truth value, our procedure generates a Buchi automaton that accepts all the words that assign the chosen truth value to the LTL formula. Given the particular type of the output of the tool, it can also be seamlessly processed by third-party libraries in a natural way. That is, the Buchi automaton can then be used in the context of formal verification to check whether an LTL formula is true, false, or undefined on a given model. △ Less

Submitted 16 November, 2023; originally announced November 2023.

Comments: In Proceedings FMAS 2023, arXiv:2311.08987

ACM Class: F.1.1; D.2.4

Journal ref: EPTCS 395, 2023, pp. 180-187

Scalable Verification of Strategy Logic through Three-valued Abstraction

Authors: Francesco Belardinelli, Angelo Ferrando, Wojciech Jamroga, Vadim Malvone, Aniello Murano

Abstract: The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle this issue but at the expense of expressiveness. In this paper, we propose a three-valued semantics for Strategy Logic upon which we define an abstraction method. We show that the latter semantics is an approximation of… ▽ More The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle this issue but at the expense of expressiveness. In this paper, we propose a three-valued semantics for Strategy Logic upon which we define an abstraction method. We show that the latter semantics is an approximation of the classic two-valued one for Strategy Logic. Furthermore, we extend MCMAS, an open-source model checker for multi-agent specifications, to incorporate our abstraction method and present some promising experimental results. △ Less

Submitted 26 October, 2023; originally announced October 2023.

Runtime Verification for Trustworthy Computing

Authors: Robert Abela, Christian Colombo, Axel Curmi, Mattea Fenech, Mark Vella, Angelo Ferrando

Abstract: Autonomous and robotic systems are increasingly being trusted with sensitive activities with potentially serious consequences if that trust is broken. Runtime verification techniques present a natural source of inspiration for monitoring and enforcing the desirable properties of the communication protocols in place, providing a formal basis and ways to limit intrusiveness. A recently proposed app… ▽ More Autonomous and robotic systems are increasingly being trusted with sensitive activities with potentially serious consequences if that trust is broken. Runtime verification techniques present a natural source of inspiration for monitoring and enforcing the desirable properties of the communication protocols in place, providing a formal basis and ways to limit intrusiveness. A recently proposed approach, RV-TEE, shows how runtime verification can enhance the level of trust to the Rich Execution Environment (REE), consequently adding a further layer of protection around the Trusted Execution Environment (TEE). By reflecting on the implication of deploying RV in the context of trustworthy computing, we propose practical solutions to two threat models for the RV-TEE monitoring process: one where the adversary has gained access to the system without elevated privileges, and another where the adversary gains all privileges to the host system but fails to steal secrets from the TEE. △ Less

Submitted 3 October, 2023; originally announced October 2023.

Comments: In Proceedings AREA 2023, arXiv:2310.00333

Journal ref: EPTCS 391, 2023, pp. 49-62

Proceedings of the Third Workshop on Agents and Robots for reliable Engineered Autonomy

Authors: Angelo Ferrando, Rafael Cardoso

Abstract: The volume comprises the proceedings of the Third Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2023), held alongside the 26th European Conference on Artificial Intelligence (ECAI 2023). It explores the convergence of autonomous agents and robotics, emphasizing the practical application of agents in real-world scenarios with physical interactions. The workshop highlights the… ▽ More The volume comprises the proceedings of the Third Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2023), held alongside the 26th European Conference on Artificial Intelligence (ECAI 2023). It explores the convergence of autonomous agents and robotics, emphasizing the practical application of agents in real-world scenarios with physical interactions. The workshop highlights the growing importance of enhanced autonomy and reliable behavior in robotic systems and the need for novel verification and validation methods. Its primary objective is to promote collaboration between researchers in these fields, aiming to address complex challenges in autonomous robotic systems. The volume includes 7 full papers and 5 short papers. △ Less

Submitted 30 September, 2023; originally announced October 2023.

Journal ref: EPTCS 391, 2023

Ain't No Stop** Us Monitoring Now

Authors: Luca Ciccone, Francesco Dagnino, Angelo Ferrando

Abstract: Not all properties are monitorable. This is a well-known fact, and it means there exist properties that cannot be fully verified at runtime. However, given a non-monitorable property, a monitor can still be synthesised, but it could end up in a state where no verdict will ever be concluded on the satisfaction (resp., violation) of the property. For this reason, non-monitorable properties are usual… ▽ More Not all properties are monitorable. This is a well-known fact, and it means there exist properties that cannot be fully verified at runtime. However, given a non-monitorable property, a monitor can still be synthesised, but it could end up in a state where no verdict will ever be concluded on the satisfaction (resp., violation) of the property. For this reason, non-monitorable properties are usually discarded. In this paper, we carry out an in-depth analysis on monitorability, and how non-monitorable properties can still be partially verified. We present our theoretical results at a semantic level, without focusing on a specific formalism. Then, we show how our theory can be applied to achieve partial runtime verification of Linear Temporal Logic (LTL). △ Less

Submitted 21 November, 2022; originally announced November 2022.

Extending Attack-Fault Trees with Runtime Verification

Authors: Rafael C. Cardoso, Angelo Ferrando, Michael Fisher

Abstract: Autonomous systems are often complex and prone to software failures and cyber-attacks. We introduce RVAFTs, an extension of Attack-Fault Trees (AFTs) with runtime events that can be used to construct runtime monitors. These monitors are able to detect when failures, that can be caused either by an attack or by a fault, occur. The safety and security properties monitored are, in turn, derived from… ▽ More Autonomous systems are often complex and prone to software failures and cyber-attacks. We introduce RVAFTs, an extension of Attack-Fault Trees (AFTs) with runtime events that can be used to construct runtime monitors. These monitors are able to detect when failures, that can be caused either by an attack or by a fault, occur. The safety and security properties monitored are, in turn, derived from the hierarchical decomposition of RVAFTs. Our approach not only provides further use of AFTs, but also improves the process of instrumentation often required in runtime verification. We explain the principles and provide a simple case study demonstrating how RVAFTs can be used in practice. Through this we are also able to evaluate the detection of faults and attacks as well as assessing the computational overhead of the monitors. △ Less

Submitted 28 September, 2022; originally announced September 2022.

Comments: In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181

Journal ref: EPTCS 371, 2022, pp. 193-207

A Compositional Approach to Verifying Modular Robotic Systems

Authors: Matt Luckcuck, Marie Farrell, Angelo Ferrando, Rafael C. Cardoso, Louise A. Dennis, Michael Fisher

Abstract: Robotic systems used in safety-critical industrial situations often rely on modular software architectures, and increasingly include autonomous components. Verifying that these modular robotic systems behave as expected requires approaches that can cope with, and preferably take advantage of, this inherent modularity. This paper describes a compositional approach to specifying the nodes in robotic… ▽ More Robotic systems used in safety-critical industrial situations often rely on modular software architectures, and increasingly include autonomous components. Verifying that these modular robotic systems behave as expected requires approaches that can cope with, and preferably take advantage of, this inherent modularity. This paper describes a compositional approach to specifying the nodes in robotic systems built using the Robotic Operating System (ROS), where each node is specified using First-Order Logic (FOL) assume-guarantee contracts that link the specification to the ROS implementation. We introduce inference rules that facilitate the composition of these node-level contracts to derive system-level properties. We also present a novel Domain-Specific Language, the ROS Contract Language, which captures a node's FOL specification and links this contract to its implementation. RCL contracts can be automatically translated, by our tool Vanda, into executable monitors; which we use to verify the contracts at runtime. We illustrate our approach through the specification and verification of an autonomous rover engaged in the remote inspection of a nuclear site, and finish with smaller examples that illustrate other useful features of our framework. △ Less

Submitted 30 November, 2023; v1 submitted 10 August, 2022; originally announced August 2022.

Comments: Version submitted to RAS

Vortex solitons in twisted circular waveguide arrays

Authors: Liangwei Dong, Yaroslav V. Kartashov, Lluis Torner, Albert Ferrando

Abstract: We address the formation of topological states in twisted circular waveguide arrays and find that twisting leads to important differences of the fundamental properties of new vortex solitons with opposite topological charges that arise in the nonlinear regime. We find that such system features the rare property that clockwise and counter-clockwise vortex states are nonequivalent. Focusing on array… ▽ More We address the formation of topological states in twisted circular waveguide arrays and find that twisting leads to important differences of the fundamental properties of new vortex solitons with opposite topological charges that arise in the nonlinear regime. We find that such system features the rare property that clockwise and counter-clockwise vortex states are nonequivalent. Focusing on arrays with C_{6v} discrete rotation symmetry, we find that a longitudinal twist stabilizes the vortex solitons with the lowest topological charges m=+-1, which are always unstable in untwisted arrays with the same symmetry. Twisting also leads to the appearance of instability domains for otherwise stable solitons with m=+-2 and generates vortex modes with topological charges m=+-3 that are forbidden in untwisted arrays. By and large, we establish a rigorous relation between the discrete rotation symmetry of the array, its twist direction, and the possible soliton topological charges. △ Less

Submitted 9 August, 2022; originally announced August 2022.

Comments: 6 pages, 5 figures, to appear in Physical Review Letters

Journal ref: Phys. Rev. Lett. 129, 123903 (2022)

A method for the dynamics of vortices in a Bose-Einstein condensate: analytical equations of the trajectories of phase singularities

Authors: S. de María-García, A. Ferrando, J. A. Conejero, P. Fernández de Córdoba, M. A. García-March

Abstract: We present a method to study the dynamics of a quasi-two dimensional Bose-Einstein condensate which contains initially many vortices at arbitrary locations. We present first the analytical solution of the dynamics in a homogeneous medium and in a parabolic trap for the ideal non-interacting case. For the homogeneous case this was introduced in the context of photonics. Here we discuss this case in… ▽ More We present a method to study the dynamics of a quasi-two dimensional Bose-Einstein condensate which contains initially many vortices at arbitrary locations. We present first the analytical solution of the dynamics in a homogeneous medium and in a parabolic trap for the ideal non-interacting case. For the homogeneous case this was introduced in the context of photonics. Here we discuss this case in the context of Bose-Einstein condensates and extend the analytical solution to the trapped case, for the first time. This linear case allows one to obtain the trajectories of the position of phase singularities present in the initial condensate along with time. Also, it allows one to predict some quantities of interest, such as the time at which a vortex and an antivortex contained in the initial condensate will merge. Secondly, the method is complemented with numerical simulations of the non-linear case. We use a numerical split-step simulation of the non-linear Gross-Pitaevskii equation to determine how these trajectories and quantities of interest are changed by the presence of interactions. We illustrate the method with several simple cases of interest both in the homogeneous and parabolically trapped systems. △ Less

Submitted 24 February, 2023; v1 submitted 25 July, 2022; originally announced July 2022.

Comments: 11 pages, 4 figures. Published in the Special Issue "Computational Methods for Quantum Matter", https://www.mdpi.com/journal/condensedmatter/special_issues/Comput_Quantum_Matter

Journal ref: Condens. Matter 8(1), 12 (2023)

RV4JaCa -- Runtime Verification for Multi-Agent Systems

Authors: Debora C. Engelmann, Angelo Ferrando, Alison R. Panisson, Davide Ancona, Rafael H. Bordini, Viviana Mascardi

Abstract: This paper presents a Runtime Verification (RV) approach for Multi-Agent Systems (MAS) using the JaCaMo framework. Our objective is to bring a layer of security to the MAS. This layer is capable of controlling events during the execution of the system without needing a specific implementation in the behaviour of each agent to recognise the events. MAS have been used in the context of hybrid intell… ▽ More This paper presents a Runtime Verification (RV) approach for Multi-Agent Systems (MAS) using the JaCaMo framework. Our objective is to bring a layer of security to the MAS. This layer is capable of controlling events during the execution of the system without needing a specific implementation in the behaviour of each agent to recognise the events. MAS have been used in the context of hybrid intelligence. This use requires communication between software agents and human beings. In some cases, communication takes place via natural language dialogues. However, this kind of communication brings us to a concern related to controlling the flow of dialogue so that agents can prevent any change in the topic of discussion that could impair their reasoning. We demonstrate the implementation of a monitor that aims to control this dialogue flow in a MAS that communicates with the user through natural language to aid decision-making in hospital bed allocation. △ Less

Submitted 20 July, 2022; originally announced July 2022.

Comments: In Proceedings AREA 2022, arXiv:2207.09058

Journal ref: EPTCS 362, 2022, pp. 23-36

Proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy

Authors: Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini, Mehrnoosh Askarpour, Louise A. Dennis

Abstract: This volume contains the proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2022), co-located with the 31st International Joint Conference on Artificial Intelligence and the 25th European Conference on Artificial Intelligence (IJCAI-ECAI 2022). The AREA workshop brings together researchers from autonomous agents, software engineering and robotic communit… ▽ More This volume contains the proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2022), co-located with the 31st International Joint Conference on Artificial Intelligence and the 25th European Conference on Artificial Intelligence (IJCAI-ECAI 2022). The AREA workshop brings together researchers from autonomous agents, software engineering and robotic communities, as combining knowledge coming from these research areas may lead to innovative approaches that solve complex problems related with the verification and validation of autonomous robotic systems. △ Less

Submitted 19 July, 2022; originally announced July 2022.

Journal ref: EPTCS 362, 2022

Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems

Authors: Angelo Ferrando, Vadim Malvone

Abstract: Multi-Agent Systems (MAS) are notoriously complex and hard to verify. In fact, it is not trivial to model a MAS, and even when a model is built, it is not always possible to verify, in a formal way, that it is actually behaving as we expect. Usually, it is relevant to know whether an agent is capable of fulfilling its own goals. One possible way to check this is through Model Checking. Specificall… ▽ More Multi-Agent Systems (MAS) are notoriously complex and hard to verify. In fact, it is not trivial to model a MAS, and even when a model is built, it is not always possible to verify, in a formal way, that it is actually behaving as we expect. Usually, it is relevant to know whether an agent is capable of fulfilling its own goals. One possible way to check this is through Model Checking. Specifically, by verifying Alternating-time Temporal Logic (ATL) properties, where the notion of strategies for achieving goals can be described. Unfortunately, the resulting model checking problem is not decidable in general. In this paper, we present a verification procedure based on combining Model Checking and Runtime Verification, where sub-models of the MAS model belonging to decidable fragments are verified by a model checker, and runtime monitors are used to verify the rest. Furthermore, we implement our technique and show experimental results. △ Less

Submitted 19 April, 2022; v1 submitted 18 February, 2022; originally announced February 2022.

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

Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information

Authors: Angelo Ferrando, Vadim Malvone

Abstract: In logics for the strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall. In this work, we show a technique to approximate the verification of Alternating-time Temporal Logic (ATL*) under imperfect information and perfect recall, which is known to be undecidable. Given a model M and a formula $\varphi$, we propose a verif… ▽ More In logics for the strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall. In this work, we show a technique to approximate the verification of Alternating-time Temporal Logic (ATL*) under imperfect information and perfect recall, which is known to be undecidable. Given a model M and a formula $\varphi$, we propose a verification procedure that generates sub-models of M in which each sub-model M' satisfies a sub-formula $\varphi'$ of $\varphi$ and the verification of $\varphi'$ in M' is decidable. Then, we use CTL* model checking to provide a verification result of $\varphi$ on M. We prove that our procedure is in the same class of complexity of ATL* model checking under perfect information and perfect recall, we present a tool that implements our procedure, and provide experimental results. △ Less

Submitted 27 December, 2021; originally announced December 2021.

Towards Partial Monitoring: It is Always too Soon to Give Up

Authors: Angelo Ferrando, Rafael C. Cardoso

Abstract: Runtime Verification is a lightweight formal verification technique. It is used to verify at runtime whether the system under analysis behaves as expected. The expected behaviour is usually formally specified by means of properties, which are used to automatically synthesise monitors. A monitor is a device that, given a sequence of events representing a system execution, returns a verdict symbolis… ▽ More Runtime Verification is a lightweight formal verification technique. It is used to verify at runtime whether the system under analysis behaves as expected. The expected behaviour is usually formally specified by means of properties, which are used to automatically synthesise monitors. A monitor is a device that, given a sequence of events representing a system execution, returns a verdict symbolising the satisfaction or violation of the formal property. Properties that can (resp. cannot) be verified at runtime by a monitor are called monitorable and non-monitorable, respectively. In this paper, we revise the notion of monitorability from a practical perspective, where we show how non-monitorable properties can still be used to generate partial monitors, which can partially check the properties. Finally, we present the implications both from a theoretical and practical perspectives. △ Less

Submitted 24 October, 2021; originally announced October 2021.

Comments: In Proceedings FMAS 2021, arXiv:2110.11527

Journal ref: EPTCS 348, 2021, pp. 38-53

MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest

Authors: Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini, Matt Luckcuck, Sven Linker, Terry R. Payne

Abstract: In this paper, we describe the strategies used by our team, MLFC, that led us to achieve the 2nd place in the 15th edition of the Multi-Agent Programming Contest. The scenario used in the contest is an extension of the previous edition (14th) "Agents Assemble" wherein two teams of agents move around a 2D grid and compete to assemble complex block structures. We discuss the languages and tools used… ▽ More In this paper, we describe the strategies used by our team, MLFC, that led us to achieve the 2nd place in the 15th edition of the Multi-Agent Programming Contest. The scenario used in the contest is an extension of the previous edition (14th) "Agents Assemble" wherein two teams of agents move around a 2D grid and compete to assemble complex block structures. We discuss the languages and tools used during the development of our team. Then, we summarise the main strategies that were carried over from our previous participation in the 14th edition and list the limitations (if any) of using these strategies in the latest contest edition. We also developed new strategies that were made specifically for the extended scenario: cartography (determining the size of the map); formal verification of the map merging protocol (to provide assurances that it works when increasing the number of agents); plan cache (efficiently scaling the number of planners); task achievement (forming groups of agents to achieve tasks); and bullies (agents that focus on stop** agents from the opposing team). Finally, we give a brief overview of our performance in the contest and discuss what we believe were our shortcomings. △ Less

Submitted 18 October, 2021; v1 submitted 15 October, 2021; originally announced October 2021.

Comments: Published in The Multi-Agent Programming Contest 2021: One-and-a-Half Decades of Exploring Multi-Agent Systems

Topological edge states of nonequilibrium polaritons in hollow honeycomb arrays

Authors: Xuekai Ma, Yaroslav V. Kartashov, Albert Ferrando, Stefan Schumacher

Abstract: We address topological currents in polariton condensates excited by uniform resonant pumps in finite honeycomb arrays of microcavity pillars with a hole in the center. Such currents arise under combined action of the spin-orbit coupling and the Zeeman splitting that break the time-reversal symmetry and open a topological gap in the spectrum of the structure. The most representative feature of this… ▽ More We address topological currents in polariton condensates excited by uniform resonant pumps in finite honeycomb arrays of microcavity pillars with a hole in the center. Such currents arise under combined action of the spin-orbit coupling and the Zeeman splitting that break the time-reversal symmetry and open a topological gap in the spectrum of the structure. The most representative feature of this structure is the presence of two interfaces, inner and outer ones, where the directions of topological currents are opposite. Due to the finite size of the structure polariton-polariton interactions lead to the coupling of the edge states at the inner and outer interfaces, which depends on the size of the hollow region. Moreover, switching between currents can be realized by tuning the pump frequency. We illustrate that currents in this finite structure can be stable and study bistability effects arising due to the resonant character of the pump. △ Less

Submitted 17 September, 2020; originally announced September 2020.

Journal ref: Optics Letters 45, 5311-5314 (2020)

Can determinism and compositionality coexist in RML?

Authors: Davide Ancona, Angelo Ferrando, Viviana Mascardi

Abstract: Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system whic… ▽ More Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system which drives the implementation of the interpreter of the monitors generated by the RML compiler from the specifications. While determinism of the trace calculus ensures better performances of the generated monitors, it makes the semantics of its operators less intuitive. In this paper we move a first step towards a compositional semantics of the RML trace calculus, by interpreting its basic operators as operations on sets of instantiated event traces and by proving that such an interpretation is equivalent to the operational semantics of the calculus. △ Less

Submitted 31 August, 2020; originally announced September 2020.

Comments: In Proceedings EXPRESS/SOS 2020, arXiv:2008.12414. Author extended version is arXiv:2008.06453

ACM Class: F.3.1; D.2.5

Journal ref: EPTCS 322, 2020, pp. 13-32

Can determinism and compositionality coexist in RML? (extended version)

Authors: Davide Ancona, Angelo Ferrando, Viviana Mascardi

Abstract: Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system whic… ▽ More Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system which drives the implementation of the interpreter of the monitors generated by the RML compiler from the specifications. While determinism of the trace calculus ensures better performances of the generated monitors, it makes the semantics of its operators less intuitive. In this paper we move a first step towards a compositional semantics of the RML trace calculus, by interpreting its basic operators as operations on sets of instantiated event traces and by proving that such an interpretation is equivalent to the operational semantics of the calculus. △ Less

Submitted 17 August, 2020; v1 submitted 14 August, 2020; originally announced August 2020.

Proceedings of the First Workshop on Agents and Robots for reliable Engineered Autonomy

Authors: Rafael C. Cardoso, Angelo Ferrando, Daniela Briola, Claudio Menghi, Tobias Ahlbrecht

Abstract: This volume contains the proceedings of the First Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2020), co-located with the 24th European Conference on Artificial Intelligence (ECAI 2020). AREA brings together researchers from autonomous agents, software engineering and robotic communities, as combining knowledge coming from these research areas may lead to innovative approac… ▽ More This volume contains the proceedings of the First Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2020), co-located with the 24th European Conference on Artificial Intelligence (ECAI 2020). AREA brings together researchers from autonomous agents, software engineering and robotic communities, as combining knowledge coming from these research areas may lead to innovative approaches that solve complex problems related with the verification and validation of autonomous robotic systems. △ Less

Submitted 22 July, 2020; originally announced July 2020.

Journal ref: EPTCS 319, 2020

Heterogeneous Verification of an Autonomous Curiosity Rover

Authors: Rafael C. Cardoso, Marie Farrell, Matt Luckcuck, Angelo Ferrando, Michael Fisher

Abstract: The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to th… ▽ More The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4--24 minutes for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance. △ Less

Submitted 20 July, 2020; originally announced July 2020.

Nonlinear higher-order polariton topological insulator

Authors: Yiqi Zhang, Y. V. Kartashov, L. Torner, Yongdong Li, A. Ferrando

Abstract: We address the resonant response and bistability of the exciton-polariton corner states in a higher-order nonlinear topological insulator realized with kagome arrangement of microcavity pillars. Such states are resonantly excited and exist due to the balance between pump and losses, on the one hand, and between nonlinearity and dispersion in inhomogeneous potential landscape, on the other hand, fo… ▽ More We address the resonant response and bistability of the exciton-polariton corner states in a higher-order nonlinear topological insulator realized with kagome arrangement of microcavity pillars. Such states are resonantly excited and exist due to the balance between pump and losses, on the one hand, and between nonlinearity and dispersion in inhomogeneous potential landscape, on the other hand, for pump energy around eigen-energies of corresponding linear localized modes. Localization of the nonlinear corner states in a higher-order topological insulator can be efficiently controlled by tuning pump energy. We link the mechanism of corner state formation with symmetry of the truncated kagome array. Corner states coexist with densely packed edge states, but are well-isolated from them in energy. Nonlinear corner states persist even in the presence of perturbations in corner microcavity pillar. △ Less

Submitted 17 July, 2020; originally announced July 2020.

Comments: 6 pages, 5 figures

Journal ref: Opt. Lett. 45, 4710-4713(2020)

LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest

Authors: Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini

Abstract: The 2019 Multi-Agent Programming Contest introduced a new scenario, Agents Assemble, where two teams of agents move around a 2D grid and compete to assemble complex block structures. In this paper, we describe the strategies used by our team that led us to achieve first place in the contest. Our strategies tackle some of the major challenges in the 2019 contest: how to explore and build a map when… ▽ More The 2019 Multi-Agent Programming Contest introduced a new scenario, Agents Assemble, where two teams of agents move around a 2D grid and compete to assemble complex block structures. In this paper, we describe the strategies used by our team that led us to achieve first place in the contest. Our strategies tackle some of the major challenges in the 2019 contest: how to explore and build a map when agents only have access to local vision and no global coordinates; how to move around the map efficiently even though there are dynamic events that can change the cells in the grid; and how to assemble and submit complex block structures given that the opposing team may try to sabotage us. To implement our strategies, we use the multi-agent systems development platform JaCaMo to program our agents and the Fast Downward planner to plan the movement of the agent in the grid. We also provide a brief discussion of our matches in the contest and give our analysis of how our team performed in each match. △ Less

Submitted 4 June, 2020; originally announced June 2020.

Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management

Authors: Xingyu Zhao, Matt Osborne, Jenny Lantair, Valentin Robu, David Flynn, Xiaowei Huang, Michael Fisher, Fabio Papacchini, Angelo Ferrando

Abstract: The battery is a key component of autonomous robots. Its performance limits the robot's safety and reliability. Unlike liquid-fuel, a battery, as a chemical device, exhibits complicated features, including (i) capacity fade over successive recharges and (ii) increasing discharge rate as the state of charge (SOC) goes down for a given power demand. Existing formal verification studies of autonomous… ▽ More The battery is a key component of autonomous robots. Its performance limits the robot's safety and reliability. Unlike liquid-fuel, a battery, as a chemical device, exhibits complicated features, including (i) capacity fade over successive recharges and (ii) increasing discharge rate as the state of charge (SOC) goes down for a given power demand. Existing formal verification studies of autonomous robots, when considering energy constraints, formalise the energy component in a generic manner such that the battery features are overlooked. In this paper, we model an unmanned aerial vehicle (UAV) inspection mission on a wind farm and via probabilistic model checking in PRISM show (i) how the battery features may affect the verification results significantly in practical cases; and (ii) how the battery features, together with dynamic environments and battery safety strategies, jointly affect the verification results. Potential solutions to explicitly integrate battery prognostics and health management (PHM) with formal verification of autonomous robots are also discussed to motivate future work. △ Less

Submitted 22 August, 2019; originally announced September 2019.

Journal ref: Proceedings of 17th International Conference on Software Engineering and Formal Methods (SEFM 2019), Oslo, Norway (September 2019)

Interface states in polariton topological insulators

Authors: Yiqi Zhang, Yaroslav V. Kartashov, Albert Ferrando

Abstract: We address linear and nonlinear topological interface states in polariton condensates excited at the interface of the honeycomb and Lieb arrays of microcavity pillars in the presence of spin-orbit coupling and Zeeman splitting in the external magnetic field. Such interface states appear only in total energy gaps of the composite structure when parameters of the honeycomb and Lieb arrays are select… ▽ More We address linear and nonlinear topological interface states in polariton condensates excited at the interface of the honeycomb and Lieb arrays of microcavity pillars in the presence of spin-orbit coupling and Zeeman splitting in the external magnetic field. Such interface states appear only in total energy gaps of the composite structure when parameters of the honeycomb and Lieb arrays are selected such that some topological gaps in the spectrum of one of the arrays overlap with topological or nontopological gaps in the spectrum of the other array. This is in contrast to conventional edge states at the interface of periodic topological and uniform trivial insulators, whose behavior is determined exclusively by the spectrum of the topological medium. The number of emerging interface states is determined by the difference of the Chern numbers of the overlap** gaps. Illustrative examples with one or two coexisting unidirectional interface states are provided. The representative feature of the system is the possibility of wide tuning of the concentration of power of the interface states between two limiting cases when practically all power is concentrated either in the Lieb or the honeycomb array. Localization of the interface states and their penetration depth into arrays drastically vary with Bloch momentum or upon modification of the amplitude of the interface state in the nonlinear regime. We illustrate topological protection of the interface states manifested in the absence of backscattering on interface defects, and study their modulation instability in the nonlinear regime. The latter leads to formation of quasisolitons whose penetration into different arrays also depends on Bloch momentum. In addition, we discuss the impact of losses and coherent pump leading to bistability of the interface states. △ Less

Submitted 23 May, 2019; originally announced May 2019.

Comments: 9 pages, 8 figures, 60 references

Journal ref: Phys. Rev. A 99, 053836(2019)

Graded-index optical fiber emulator of an interacting three-atom system: illumination control of particle statistics and classical non-separability

Authors: M. A. Garcia-March, N. L. Harshman, H. da Silva, T. Fogarty, Th. Busch, M. Lewenstein, A. Ferrando

Abstract: We show that a system of three trapped ultracold and strongly interacting atoms in one-dimension can be emulated using an optical fiber with a graded-index profile and thin metallic slabs. While the wave-nature of single quantum particles leads to direct and well known analogies with classical optics, for interacting many-particle systems with unrestricted statistics such analoga are not straightf… ▽ More We show that a system of three trapped ultracold and strongly interacting atoms in one-dimension can be emulated using an optical fiber with a graded-index profile and thin metallic slabs. While the wave-nature of single quantum particles leads to direct and well known analogies with classical optics, for interacting many-particle systems with unrestricted statistics such analoga are not straightforward. Here we study the symmetries present in the fiber eigenstates by using discrete group theory and show that, by spatially modulating the incident field, one can select the atomic statistics, i.e., emulate a system of three bosons, fermions or two bosons or fermions plus an additional distinguishable particle. We also show that the optical system is able to produce classical non-separability resembling that found in the analogous atomic system. △ Less

Submitted 2 December, 2019; v1 submitted 5 February, 2019; originally announced February 2019.

Comments: 14 pages, 5 figures

Journal ref: Quantum 3, 210 (2019)

On the Enactability of Agent Interaction Protocols: Toward a Unified Approach

Authors: Angelo Ferrando, Michael Winikoff, Stephen Cranefield, Frank Dignum, Viviana Mascardi

Abstract: Interactions between agents are usually designed from a global viewpoint. However, the implementation of a multi-agent interaction is distributed. This difference can introduce issues. For instance, it is possible to specify protocols from a global viewpoint that cannot be implemented as a collection of individual agents. This leads naturally to the question of whether a given (global) protocol is… ▽ More Interactions between agents are usually designed from a global viewpoint. However, the implementation of a multi-agent interaction is distributed. This difference can introduce issues. For instance, it is possible to specify protocols from a global viewpoint that cannot be implemented as a collection of individual agents. This leads naturally to the question of whether a given (global) protocol is enactable. We consider this question in a powerful setting (trace expression), considering a range of message ordering interpretations (what does it mean to say that an interaction step occurs before another), and a range of possible constraints on the semantics of message delivery, corresponding to different properties of underlying communication middleware. △ Less

Submitted 13 February, 2019; v1 submitted 4 February, 2019; originally announced February 2019.

Lieb polariton topological insulators

Authors: Chunyan Li, Fangwei Ye, Xianfeng Chen, Yaroslav V. Kartashov, Albert Ferrando, Lluis Torner, Dmitry V. Skryabin

Abstract: We predict that the interplay between the spin-orbit coupling, stemming from the TE-TM energy splitting, and the Zeeman effect in semiconductor microcavities supporting exci- ton-polariton quasi-particles results in the appearance of unidirectional linear topological edge states when the top microcavity mirror is patterned to form a truncated dislocated Lieb lattice of cylindrical pillars. Periodi… ▽ More We predict that the interplay between the spin-orbit coupling, stemming from the TE-TM energy splitting, and the Zeeman effect in semiconductor microcavities supporting exci- ton-polariton quasi-particles results in the appearance of unidirectional linear topological edge states when the top microcavity mirror is patterned to form a truncated dislocated Lieb lattice of cylindrical pillars. Periodic nonlinear edge states are found to emerge from the linear ones. They are strongly localized across the interface and they are remarkably robust in comparison to their counterparts in hexagonal lattices. Such robustness makes possible the existence of nested unidirectional dark solitons that move steadily along the lattice edge. △ Less

Submitted 4 February, 2018; originally announced February 2018.

Comments: 27 pages, 7 figures, to appear in Phys. Rev. B as a Rapid Communications

Photonic Nambu-Goldstone bosons

Authors: Miguel Ángel García-March, Ángel Paredes, Mario Zacarés, Humberto Michinel, Albert Ferrando

Abstract: We study numerically the spatial dynamics of light in periodic square lattices in the presence of a Kerr term, emphasizing the peculiarities stemming from the nonlinearity. We find that, under rather general circumstances, the phase pattern of the stable ground state depends on the character of the nonlinearity: the phase is spatially uniform if it is defocusing whereas in the focusing case, it pr… ▽ More We study numerically the spatial dynamics of light in periodic square lattices in the presence of a Kerr term, emphasizing the peculiarities stemming from the nonlinearity. We find that, under rather general circumstances, the phase pattern of the stable ground state depends on the character of the nonlinearity: the phase is spatially uniform if it is defocusing whereas in the focusing case, it presents a chess board pattern, with a difference of $π$ between neighboring sites. We show that the lowest lying perturbative excitations can be described as perturbations of the phase and that finite-sized structures can act as tunable metawaveguides for them. The tuning is made by varying the intensity of the light that, because of the nonlinearity, affects the dynamics of the phase fluctuations. We interpret the results using methods of condensed matter physics, based on an effective description of the optical system. This interpretation sheds new light on the phenomena, facilitating the understanding of individual systems and leading to a framework for relating different problems with the same symmetry. In this context, we show that the perturbative excitations of the phase are Nambu-Goldstone bosons of a spontaneously broken $U(1)$ symmetry. △ Less

Submitted 8 November, 2017; v1 submitted 7 July, 2017; originally announced July 2017.

Comments: References added. One figure added. Abstract, discussions and structure of the paper improved. Conclusions unchanged

Journal ref: Phys. Rev. A 96, 053848 (2017)

Nonequilibrium quantum dynamics of partial symmetry breaking for ultracold bosons in an optical lattice ring trap

Authors: Xinxin Zhao, Marie A. McLain, J. Vijande, A. Ferrando, Lincoln D. Carr, M. Á. García-March

Abstract: A vortex in a Bose-Einstein condensate on a ring undergoes quantum dynamics in response to a quantum quench in terms of partial symmetry breaking from a uniform lattice to a biperiodic one. Neither the current, a macroscopic measure, nor fidelity, a microscopic measure, exhibit critical behavior. Instead, the symmetry memory succeeds in identifying the point at which the system begins to forget it… ▽ More A vortex in a Bose-Einstein condensate on a ring undergoes quantum dynamics in response to a quantum quench in terms of partial symmetry breaking from a uniform lattice to a biperiodic one. Neither the current, a macroscopic measure, nor fidelity, a microscopic measure, exhibit critical behavior. Instead, the symmetry memory succeeds in identifying the point at which the system begins to forget its initial symmetry state. We further identify a symmetry energy difference in the low lying excited states which trends with the symmetry memory. △ Less

Submitted 13 February, 2019; v1 submitted 4 May, 2017; originally announced May 2017.

Nonlinear plasmonic amplification via dissipative soliplasmons

Authors: Albert Ferrando

Abstract: In this contribution we introduce a new strategy for the compensation of plasmonic losses based on a recently proposed nonlinear mechanism: the resonant interaction between surface plasmon polaritons and spatial solitons propagating in parallel along a metal/dielectric/Kerr structure. This mechanism naturally leads to the generation of a quasi-particle excitation, the so-called soliplasmon resonan… ▽ More In this contribution we introduce a new strategy for the compensation of plasmonic losses based on a recently proposed nonlinear mechanism: the resonant interaction between surface plasmon polaritons and spatial solitons propagating in parallel along a metal/dielectric/Kerr structure. This mechanism naturally leads to the generation of a quasi-particle excitation, the so-called soliplasmon resonance. We analyze the role played by the effective nonlinear coupling inherent to this system and how this can be used to provide a new mechanism of quasi-resonant nonlinear excitation of surface plasmon polaritons. We will pay particular attention to the introduction of asymmetric linear gain in the Kerr medium. The unique combination of nonlinear propagation, nonlinear coupling and gain give rise to a new scenario for the excitation of long- range surface plasmon polaritons with distinguishing characteristics. The connection between plasmonic losses and soliplasmon resonances in the presence of gain will be discussed. △ Less

Submitted 7 November, 2016; originally announced November 2016.

Comments: 20 pages, 7 figures

Analytical solution for multisingular vortex Gaussian beams: The mathematical theory of scattering modes

Authors: A. Ferrando, M. A. Garcia-March

Abstract: We present a novel procedure to solve the Schrödinger equation, which in optics is the paraxial wave equation, with an initial multisingular vortex Gaussian beam. This initial condition has a number of singularities in a plane transversal to propagation embedded in a Gaussian beam. We use the scattering modes, which are solutions of the paraxial wave equation that can be combined straightforwardly… ▽ More We present a novel procedure to solve the Schrödinger equation, which in optics is the paraxial wave equation, with an initial multisingular vortex Gaussian beam. This initial condition has a number of singularities in a plane transversal to propagation embedded in a Gaussian beam. We use the scattering modes, which are solutions of the paraxial wave equation that can be combined straightforwardly to express the initial condition and therefore permit to solve the problem. To construct the scattering modes one needs to obtain a particular set of polynomials, which play an analogous role than Laguerre polynomials for Laguerre-Gaussian modes. We demonstrate here the recurrence relations needed to determine these polynomials. To stress the utility and strength of the method we solve first the problem of an initial Gaussian beam with two positive singularities and a negative one embedded in. We show that the solution permits one to obtain analytical expressions. These can used to obtain closed expressions for meaningful quantities, like the distance at which the positive and negative singularities merge, closing the loop of a vortex line. Furthermore, we present an example of calculation of an specific discrete-Gauss state, which is the solution of the diffraction of a Laguerre-Gauss state showing definite angular momentum (that is, a highly charged vortex) by a thin diffractive element showing certain discrete symmetry. We show that thereby this problem is solved in a much simpler way than using the previous procedure based in the integral Fresnel diffraction method. △ Less

Submitted 11 March, 2016; v1 submitted 1 February, 2016; originally announced February 2016.

Comments: 19 pages, 2 tables, 1 figure

Supercontinuum optimization for dual-soliton based light sources using genetic algorithms in a Grid platform

Authors: F. R. Arteaga-Sierra, C. Milián, I. Torres-Gómez, M. Torres-Cisneros, G. Moltó, A. Ferrando

Abstract: We present a numerical strategy to design fiber based dual pulse light sources exhibiting two predefined spectral peaks in the anomalous group velocity dispersion regime. The frequency conversion is based on the soliton fission and soliton self-frequency shift occurring during supercontinuum generation. The optimization process is carried out by a genetic algorithm that provides the optimum input… ▽ More We present a numerical strategy to design fiber based dual pulse light sources exhibiting two predefined spectral peaks in the anomalous group velocity dispersion regime. The frequency conversion is based on the soliton fission and soliton self-frequency shift occurring during supercontinuum generation. The optimization process is carried out by a genetic algorithm that provides the optimum input pulse parameters: wavelength, temporal width and peak power. This algorithm is implemented in a Grid platform in order to take advantage of distributed computing. These results are useful for optical coherence tomography applications where bell-shaped pulses located in the second near-infrared window are needed. △ Less

Submitted 4 August, 2014; originally announced August 2014.

Comments: This paper was published in Opt. Express and is made available as an electronic reprint with the permission of OSA. The paper can be found at the following url on the OSA website: \url{http://www.opticsinfobase.org/oe}. Systematic or multiple reproduction or distribution to multiple locations via electronic or other means is prohibited and is subject to penalties under law

Discrete-Gauss states and the generation of focussing dark beams

Authors: Albert Ferrando

Abstract: Discrete-Gauss states are a new class of gaussian solutions of the free Schrödinger equation owning discrete rotational symmetry. They are obtained by acting with a discrete deformation operator onto Laguerre-Gauss modes. We present a general analytical construction of these states and show the necessary and sufficient condition for them to host embedded dark beams structures. We unveil the intima… ▽ More Discrete-Gauss states are a new class of gaussian solutions of the free Schrödinger equation owning discrete rotational symmetry. They are obtained by acting with a discrete deformation operator onto Laguerre-Gauss modes. We present a general analytical construction of these states and show the necessary and sufficient condition for them to host embedded dark beams structures. We unveil the intimate connection between discrete rotational symmetry, orbital angular momentum, and the generation of focussing dark beams. The distinguishing features of focussing dark beams are discussed. The potential applications of Discrete-Gauss states in advanced optical trap** and quantum information processing are also briefly discussed. △ Less

Submitted 25 March, 2014; v1 submitted 11 March, 2014; originally announced March 2014.

Comments: 11 pages, 4 figures

Journal ref: Phys. Rev. A 90, 023844 (2014)

The key role of off-axis singularities in free-space vortex transmutation

Authors: David Novoa, Iñigo J. Sola, Miguel Angel Garcia-March, Albert Ferrando

Abstract: We experimentally demonstrate the generation of off-axis phase singularities in a vortex transmutation process induced by the breaking of rotational symmetry. The process takes place in free space by launching a highly-charged vortex, owning full rotational symmetry, into a linear thin diffractive element presenting discrete rotational symmetry. It is shown that off-axis phase singularities follow… ▽ More We experimentally demonstrate the generation of off-axis phase singularities in a vortex transmutation process induced by the breaking of rotational symmetry. The process takes place in free space by launching a highly-charged vortex, owning full rotational symmetry, into a linear thin diffractive element presenting discrete rotational symmetry. It is shown that off-axis phase singularities follow straight dark rays bifurcating from the symmetry axis. This phenomenon may provide new routes towards the spatial control of multiple phase singularities for applications in atom trap** and particle manipulation. △ Less

Submitted 8 January, 2014; v1 submitted 26 June, 2013; originally announced June 2013.

Comments: 4 pages, 4 figures, to appear in Applied Physics B: Lasers and Optics

Journal ref: Applied Physics B: Lasers and Optics (2014)

Variational theory of soliplasmon resonances

Authors: A. Ferrando, C. Milián, D. V. Skryabin

Abstract: We present a first-principles derivation of the variational equations describing the dynamics of the interaction of a spatial soliton and a surface plasmon polariton (SPP) propagating along a metal/dielectric interface. The variational ansatz is based on the existence of solutions exhibiting differentiated and spatially resolvable localized soliton and SPP components. These states, referred to as… ▽ More We present a first-principles derivation of the variational equations describing the dynamics of the interaction of a spatial soliton and a surface plasmon polariton (SPP) propagating along a metal/dielectric interface. The variational ansatz is based on the existence of solutions exhibiting differentiated and spatially resolvable localized soliton and SPP components. These states, referred to as soliplasmons, can be physically understood as bound states of a soliton and a SPP. Their respective dispersion relations permit the existence of a resonant interaction between them, as pointed out in Ref.[1]. The existence of soliplasmon states and their interesting nonlinear resonant behavior has been validated already by full-vector simulations of the nonlinear Maxwell's equations, as reported in Ref.[2]. Here, we provide the theoretical demonstration of the nonlinear resonator model previously introduced in our previous work and analyze all the approximations needed to obtain it. We also provide some extensions of the model to improve its applicability. △ Less

Submitted 18 January, 2013; originally announced January 2013.

Maxwell's equations approach to soliton excitations of surface plasmonic resonances

Authors: Carles Milián, Daniel E. Ceballos-Herrera, Dmitry V. Skryabin, Albert Ferrando

Abstract: We demonstrate that soliton-plasmon bound states appear naturally as propagating eigenmodes of nonlinear Maxwell's equations for a metal/dielectric/Kerr interface. By means of a variational method, we give an explicit and simplified expression for the full-vector nonlinear operator of the system. Soliplasmon states (propagating surface soliton-plasmon modes) can be then analytically calculated as… ▽ More We demonstrate that soliton-plasmon bound states appear naturally as propagating eigenmodes of nonlinear Maxwell's equations for a metal/dielectric/Kerr interface. By means of a variational method, we give an explicit and simplified expression for the full-vector nonlinear operator of the system. Soliplasmon states (propagating surface soliton-plasmon modes) can be then analytically calculated as eigenmodes of this non-selfadjoint operator. The theoretical treatment of the system predicts the key features of the stationary solutions and gives physical insight to understand the inherent stability and dynamics observed by means of finite element numerical modeling of the time independent nonlinear Maxwell equations. Our results contribute with a new theory for the development of power-tunable photonic nanocircuits based on nonlinear plasmonic waveguides. △ Less

Submitted 11 May, 2012; originally announced May 2012.

Symmetry breaking and singularity structure in Bose-Einstein condensates

Authors: K. A. Commeford, M. A. Garcia-March, A. Ferrando, Lincoln D. Carr

Abstract: We determine the trajectories of vortex singularities that arise after a single vortex is broken by a discretely symmetric impulse in the context of Bose-Einstein condensates in a harmonic trap. The dynamics of these singularities are analyzed to determine the form of the imprinted motion. We find that the symmetry-breaking process introduces two effective forces: a repulsive harmonic force that c… ▽ More We determine the trajectories of vortex singularities that arise after a single vortex is broken by a discretely symmetric impulse in the context of Bose-Einstein condensates in a harmonic trap. The dynamics of these singularities are analyzed to determine the form of the imprinted motion. We find that the symmetry-breaking process introduces two effective forces: a repulsive harmonic force that causes the daughter trajectories to be ejected from the parent singularity, and a Magnus force that introduces a torque about the axis of symmetry. For the analytical non-interacting case we find that the parent singularity is reconstructed from the daughter singularities after one period of the trap** frequency. The interactions between singularities in the weakly interacting system do not allow the parent vortex to be reconstructed. Analytic trajectories were compared to the actual minima of the wavefunction, showing less 0.5% error for impulse strength of (v=0.00005). We show that these solutions are valid within the impulse regime for various impulse strengths using numerical integration of the Gross-Pitaevskii equation. We also show that the actual duration of the symmetry breaking potential does not significantly change the dynamics of the system as long as the strength is below (v=0.0005). △ Less

Submitted 11 April, 2012; v1 submitted 3 April, 2012; originally announced April 2012.

Comments: 14 pages, 10 figures

Journal ref: Phys. Rev. A 86, 023627 (2012)

Precision tests of QED and non-standard models by searching photon-photon scattering in vacuum with high power lasers

Authors: Daniele Tommasini, Albert Ferrando, Humberto Michinel, Marcos Seco

Abstract: We study how to search for photon-photon scattering in vacuum at present petawatt laser facilities such as HERCULES, and test Quantum Electrodynamics and non-standard models like Born-Infeld theory or scenarios involving minicharged particles or axion-like bosons. First, we compute the phase shift that is produced when an ultra-intense laser beam crosses a low power beam, in the case of arbitrar… ▽ More We study how to search for photon-photon scattering in vacuum at present petawatt laser facilities such as HERCULES, and test Quantum Electrodynamics and non-standard models like Born-Infeld theory or scenarios involving minicharged particles or axion-like bosons. First, we compute the phase shift that is produced when an ultra-intense laser beam crosses a low power beam, in the case of arbitrary polarisations. This result is then used in order to design a complete test of all the parameters appearing in the low energy effective photonic Lagrangian. In fact, we propose a set of experiments that can be performed at HERCULES, eventually allowing either to detect photon-photon scattering as due to new physics, or to set new limits on the relevant parameters, improving by several orders of magnitude the current constraints obtained recently by PVLAS collaboration. We also describe a multi-cross optical mechanism that can further enhance the sensitivity, enabling HERCULES to detect photon-photon scattering even at a rate as small as that predicted by QED. Finally, we discuss how these results can be improved at future exawatt facilities such as ELI, thus providing a new class of precision tests of the Standard Model and beyond. △ Less

Submitted 11 November, 2009; v1 submitted 25 September, 2009; originally announced September 2009.

Comments: 15 pages, 2 figures. Corrected few mistakes in section and 4. Results unchanged. Added a reference

Journal ref: JHEP 0911:043,2009

Continuum generation by dark solitons

Authors: C. Milian, D. V. Skryabin, A. Ferrando

Abstract: We demonstrate that the dark soliton trains in optical fibers with a zero of the group velocity dispersion can generate broad spectral distribution (continuum) associated with the resonant dispersive radiation emitted by solitons. This radiation is either enhanced or suppressed by the Raman scattering depending on the sign of the third order dispersion. We demonstrate that the dark soliton trains in optical fibers with a zero of the group velocity dispersion can generate broad spectral distribution (continuum) associated with the resonant dispersive radiation emitted by solitons. This radiation is either enhanced or suppressed by the Raman scattering depending on the sign of the third order dispersion. △ Less

Submitted 28 August, 2009; originally announced August 2009.

Journal ref: Optics Letters., July, 2009. Vol. 14, pp. 2096-2098

A topological charge selection rule for phase singularities

Authors: M. Zacares, M. A. Garcia-March, J. Vijande, A. Ferrando, E. Merino

Abstract: We present an study of the dynamics and decay pattern of phase singularities due to the action of a system with a discrete rotational symmetry of finite order. A topological charge conservation rule is identified. The role played by the underlying symmetry is emphasized. An effective model describing the short range dynamics of the vortex clusters has been designed. A method to engineer any desi… ▽ More We present an study of the dynamics and decay pattern of phase singularities due to the action of a system with a discrete rotational symmetry of finite order. A topological charge conservation rule is identified. The role played by the underlying symmetry is emphasized. An effective model describing the short range dynamics of the vortex clusters has been designed. A method to engineer any desired configuration of clusters of phase singularities is proposed. Its flexibility to create and control clusters of vortices is discussed. △ Less

Submitted 5 November, 2008; originally announced November 2008.

Comments: 4 pages, 3 figures

Symmetry, winding number and topological charge of vortex solitons in discrete-symmetry media

Authors: Miguel-Ángel García-March, Albert Ferrando, Mario Zacarés, Sarira Sahu, Daniel E. Ceballos-Herrera

Abstract: We determine the functional behavior near the discrete rotational symmetry axis of discrete vortices of the nonlinear Schrödinger equation. We show that these solutions present a central phase singularity whose charge is restricted by symmetry arguments. Consequently, we demonstrate that the existence of high-charged discrete vortices is related to the presence of other off-axis phase singularit… ▽ More We determine the functional behavior near the discrete rotational symmetry axis of discrete vortices of the nonlinear Schrödinger equation. We show that these solutions present a central phase singularity whose charge is restricted by symmetry arguments. Consequently, we demonstrate that the existence of high-charged discrete vortices is related to the presence of other off-axis phase singularities, whose positions and charges are also restricted by symmetry arguments. To illustrate our theoretical results, we offer two numerical examples of high-charged discrete vortices in photonic crystal fibers showing hexagonal discrete rotational invariance. △ Less

Submitted 2 November, 2008; originally announced November 2008.

Comments: 6 pages, 2 figures

Nonlinear Propagation of Crossing Electromagnetic Waves in Vacuum due to Photon-Photon Scattering

Authors: Daniele Tommasini, Albert Ferrando, Humberto Michinel, Marcos Seco

Abstract: We review the theory for photon-photon scattering in vacuum, and some of the proposals for its experimental search, including the results of our recent works on the subject. We then describe a very simple and sensitive proposal of an experiment and discuss how it can be used at the present (HERCULES) and the future (ELI) ultrahigh power laser facilities either to find the first evidence of photo… ▽ More We review the theory for photon-photon scattering in vacuum, and some of the proposals for its experimental search, including the results of our recent works on the subject. We then describe a very simple and sensitive proposal of an experiment and discuss how it can be used at the present (HERCULES) and the future (ELI) ultrahigh power laser facilities either to find the first evidence of photon-photon scattering in vacuum, or to significantly improve the current experimental limits. △ Less

Submitted 2 September, 2008; originally announced September 2008.

Comments: Talk delivered (by D.T.) at the International Workshop on the Frontiers of Modern Plasma Physics, Trieste, 2008. To appear in the proceedings

Journal ref: AIP Conference Proceedings 1061 (2008), p.292-301

Supersolid behavior of nonlinear light

Authors: Albert Ferrando, Miguel Ángel García-March, Mario Zacarés

Abstract: We present a formal demonstration that light can simultaneously exhibit a superfluid behavior and spatial long-range order when propagating in a photonic crystal with self-focussing nonlinearity. In this way, light presents the distinguishing features of matter in a "supersolid" phase. We show that this supersolid phase provides the stability conditions for nonlinear Bloch waves and, at the same t… ▽ More We present a formal demonstration that light can simultaneously exhibit a superfluid behavior and spatial long-range order when propagating in a photonic crystal with self-focussing nonlinearity. In this way, light presents the distinguishing features of matter in a "supersolid" phase. We show that this supersolid phase provides the stability conditions for nonlinear Bloch waves and, at the same time, permits the existence of topological solitons or defects for the envelope of these waves. We use a condensed matter analysis instead of a standard nonlinear optics approach and provide numerical evidence of these theoretical findings. △ Less

Submitted 10 July, 2017; v1 submitted 7 August, 2008; originally announced August 2008.

Comments: The contents of this paper have been extended and completed, and part of them are now included in the new larger and more detailed paper arXiv:1707.02213

Resonant Plasmon-Soliton Interaction

Authors: K. Y. Bliokh, Y. P. Bliokh, A. Ferrando

Abstract: We describe an effective resonant interaction between two localized wave modes of different nature: a plasmon-polariton at a metal surface and a self-focusing beam (spatial soliton) in a non-linear dielectric medium. Propagating in the same direction, they represent an exotic coupled-waveguide system, where the resonant interaction is controlled by the soliton amplitude. This non-linear system m… ▽ More We describe an effective resonant interaction between two localized wave modes of different nature: a plasmon-polariton at a metal surface and a self-focusing beam (spatial soliton) in a non-linear dielectric medium. Propagating in the same direction, they represent an exotic coupled-waveguide system, where the resonant interaction is controlled by the soliton amplitude. This non-linear system manifests hybridized plasmon-soliton eigenmodes, mutual conversion, and non-adiabatic switching, which offer exciting opportunities for manipulation of plasmons via spatial solitons. △ Less

Submitted 11 March, 2009; v1 submitted 13 June, 2008; originally announced June 2008.

Comments: 5 pages, 4 figures, to appear in Phys. Rev. A

Angular Pseudomomentum Theory for the Generalized Nonlinear Schrödinger Equation in Discrete Rotational Symmetry Media

Authors: M. -Á. García-March, A. Ferrando, M. Zacarés, J. Vijande, L. D. Carr

Abstract: We develop a complete mathematical theory for the symmetrical solutions of the generalized nonlinear Schrödinger equation based on the new concept of angular pseudomomentum. We consider the symmetric solitons of a generalized nonlinear Schrödinger equation with a nonlinearity depending on the modulus of the field. We provide a rigorous proof of a set of mathematical results justifying that these… ▽ More We develop a complete mathematical theory for the symmetrical solutions of the generalized nonlinear Schrödinger equation based on the new concept of angular pseudomomentum. We consider the symmetric solitons of a generalized nonlinear Schrödinger equation with a nonlinearity depending on the modulus of the field. We provide a rigorous proof of a set of mathematical results justifying that these solitons can be classified according to the irreducible representations of a discrete group. Then we extend this theory to non-stationary solutions and study the relationship between angular momentum and pseudomomentum. We illustrate these theoretical results with numerical examples. Finally, we explore the possibilities of the generalization of the previous framework to the quantum limit. △ Less

Submitted 5 June, 2008; originally announced June 2008.

Comments: 18 pages; submitted to Physica D

Journal ref: PHYSICA D-NONLINEAR PHENOMENA 238, 1432 (2009)

Noncommutative space and the low-energy physics of quasicrystals

Authors: L. Monreal, P. Fernandez de Cordoba, A. Ferrando, J. M. Isidro

Abstract: We prove that the effective low-energy, nonlinear Schroedinger equation for a particle in the presence of a quasiperiodic potential is the potential-free, nonlinear Schroedinger equation on noncommutative space. Thus quasiperiodicity of the potential can be traded for space noncommutativity when describing the envelope wave of the initial quasiperiodic wave. We prove that the effective low-energy, nonlinear Schroedinger equation for a particle in the presence of a quasiperiodic potential is the potential-free, nonlinear Schroedinger equation on noncommutative space. Thus quasiperiodicity of the potential can be traded for space noncommutativity when describing the envelope wave of the initial quasiperiodic wave. △ Less

Submitted 23 April, 2008; v1 submitted 17 April, 2008; originally announced April 2008.

Comments: 9 pages, some refs added

Journal ref: Int.J.Mod.Phys.A23:2037-2045,2008

Detecting photon-photon scattering in vacuum at exawatt lasers

Authors: Daniele Tommasini, Albert Ferrando, Humberto Michinel, Marcos Seco

Abstract: In a recent paper, we have shown that the QED nonlinear corrections imply a phase correction to the linear evolution of crossing electromagnetic waves in vacuum. Here, we provide a more complete analysis, including a full numerical solution of the QED nonlinear wave equations for short-distance propagation in a symmetric configuration. The excellent agreement of such a solution with the result t… ▽ More In a recent paper, we have shown that the QED nonlinear corrections imply a phase correction to the linear evolution of crossing electromagnetic waves in vacuum. Here, we provide a more complete analysis, including a full numerical solution of the QED nonlinear wave equations for short-distance propagation in a symmetric configuration. The excellent agreement of such a solution with the result that we obtain using our perturbatively-motivated Variational Approach is then used to justify an analytical approximation that can be applied in a more general case. This allows us to find the most promising configuration for the search of photon-photon scattering in optics experiments. In particular, we show that our previous requirement of phase coherence between the two crossing beams can be released. We then propose a very simple experiment that can be performed at future exawatt laser facilities, such as ELI, by bombarding a low power laser beam with the exawatt bump. △ Less

Submitted 1 February, 2008; originally announced February 2008.

Comments: 8 pages, 6 figures

Journal ref: Phys. Rev. A 77, 042101 (2008)

Nonlinear phase shift from photon-photon scattering in vacuum

Authors: Albert Ferrando, Humberto Michinel, Marcos Seco, Daniele Tommasini

Abstract: We show that QED nonlinear effects imply a phase correction to the linear evolution of electromagnetic waves in vacuum. We provide explicit solutions of the modified Maxwell's equations for the propagation of a superposition of two plane waves, and calculate analytically and numerically the corresponding phase shift. This provides a new framework for the search of all-optical signatures of photo… ▽ More We show that QED nonlinear effects imply a phase correction to the linear evolution of electromagnetic waves in vacuum. We provide explicit solutions of the modified Maxwell's equations for the propagation of a superposition of two plane waves, and calculate analytically and numerically the corresponding phase shift. This provides a new framework for the search of all-optical signatures of photon-photon scattering in vacuum. In particular, we propose an experiment for measuring the phase shift in projected high-power laser facilities. △ Less

Submitted 15 October, 2007; v1 submitted 23 March, 2007; originally announced March 2007.

Comments: 4 pages, 1 figure. Some references were added, and the comparison with AC Kerr effect has been improved

Journal ref: Phys. Rev. Lett. 99 (2007) 150404