-
Multi-Target Acquisition in Multistatic MIMO-OFDM Joint Sensing and Communication
Authors:
Elisabetta Matricardi,
Lorenzo Pucci,
Elia Favarelli,
Enrico Paolini,
Andrea Giorgetti
Abstract:
In this work, we investigate a multistatic MIMO-OFDM joint sensing and communication (JSC) system that leverages cooperation among spatially distributed base stations (BSs) to detect and localize multiple targets through soft fusion of range-angle maps. We propose an innovative selective data fusion strategy that combines only the most reliable regions of range-angle maps from each bistatic pair,…
▽ More
In this work, we investigate a multistatic MIMO-OFDM joint sensing and communication (JSC) system that leverages cooperation among spatially distributed base stations (BSs) to detect and localize multiple targets through soft fusion of range-angle maps. We propose an innovative selective data fusion strategy that combines only the most reliable regions of range-angle maps from each bistatic pair, mitigating the adverse effects of residual clutter and target smearing inherent to bistatic configurations. To further enhance multi-view perception, we introduce a round-robin transmitter role strategy, enabling BSs to cooperate and exploit target spatial diversity. Finally, we assess the system performance in a cluttered environment using the generalized optimal subpattern assignment (GOSPA) and root mean squared error (RMSE) metrics, demonstrating the effectiveness of our approaches in improving detection and localization.
△ Less
Submitted 28 March, 2025;
originally announced March 2025.
-
Cooperative Maximum Likelihood Target Position Estimation for MIMO-ISAC Networks
Authors:
Lorenzo Pucci,
Tommaso Bacchielli,
Andrea Giorgetti
Abstract:
This letter investigates target position estimation in integrated sensing and communication networks composed of multiple cooperating monostatic base stations (BSs). Each BS employs a MIMO-orthogonal time-frequency space (OTFS) scheme, enabling the coexistence of communication and sensing. A general cooperative maximum likelihood (ML) framework is derived, directly estimating the target position i…
▽ More
This letter investigates target position estimation in integrated sensing and communication networks composed of multiple cooperating monostatic base stations (BSs). Each BS employs a MIMO-orthogonal time-frequency space (OTFS) scheme, enabling the coexistence of communication and sensing. A general cooperative maximum likelihood (ML) framework is derived, directly estimating the target position in a common reference system rather than relying on local range and angle estimates at each BS. Positioning accuracy is evaluated in single-target scenarios by varying the number of collaborating BSs, using root mean square error (RMSE), and comparing against the square root of the Cramér-Rao lower bound. Numerical results demonstrate that the ML framework significantly reduces the position RMSE as the number of cooperating BSs increases.
△ Less
Submitted 3 March, 2025; v1 submitted 7 November, 2024;
originally announced November 2024.
-
An abstract structure determines the contextuality degree of observable-based Kochen-Specker proofs
Authors:
Axel Muller,
Alain Giorgetti
Abstract:
This article delves into the concept of quantum contextuality, specifically focusing on proofs of the Kochen-Specker theorem obtained by assigning Pauli observables to hypergraph vertices satisfying a given commutation relation. The abstract structure composed of this hypergraph and the graph of anticommutations is named a hypergram. Its labelings with Pauli observables generalize the well-known m…
▽ More
This article delves into the concept of quantum contextuality, specifically focusing on proofs of the Kochen-Specker theorem obtained by assigning Pauli observables to hypergraph vertices satisfying a given commutation relation. The abstract structure composed of this hypergraph and the graph of anticommutations is named a hypergram. Its labelings with Pauli observables generalize the well-known magic sets. A first result is that all these quantum labelings satisfying the conditions of a given hypergram inherently possess the same degree of contextuality. Then we provide a necessary and sufficient algebraic condition for the existence of such quantum labelings and an efficient algorithm to find one of them. We finally attach to each assignable hypergram an abstract notion of contextuality degree. By presenting the study of observable-based Kochen-Specker proofs from the perspective of graphs and matrices, this abstraction opens the way to new methods to search for original contextual configurations.
△ Less
Submitted 18 October, 2024;
originally announced October 2024.
-
Jamming Detection in MIMO-OFDM ISAC Systems Using Variational Autoencoders
Authors:
Luca Arcangeloni,
Enrico Testi,
Andrea Giorgetti
Abstract:
This paper introduces a novel unsupervised jamming detection framework designed specifically for monostatic multiple-input multiple-output (MIMO)-orthogonal frequency-division multiplexing (OFDM) radar systems. The framework leverages echo signals captured at the base station (BS) and employs the latent data representation learning capability of variational autoencoders (VAEs). The VAE-based detec…
▽ More
This paper introduces a novel unsupervised jamming detection framework designed specifically for monostatic multiple-input multiple-output (MIMO)-orthogonal frequency-division multiplexing (OFDM) radar systems. The framework leverages echo signals captured at the base station (BS) and employs the latent data representation learning capability of variational autoencoders (VAEs). The VAE-based detector is trained on echo signals received from a real target in the absence of jamming, enabling it to learn an optimal latent representation of normal network operation. During testing, in the presence of a jammer, the detector identifies anomalous signals by their inability to conform to the learned latent space. We assess the performance of the proposed method in a typical integrated sensing and communication (ISAC)-enabled 5G wireless network, even comparing it with a conventional autoencoder.
△ Less
Submitted 2 October, 2024;
originally announced October 2024.
-
A new heuristic approach for contextuality degree estimates and its four- to six-qubit portrayals
Authors:
Axel Muller,
Metod Saniga,
Alain Giorgetti,
Frédéric Holweck,
Colm Kelleher
Abstract:
We introduce and describe a new heuristic method for finding an upper bound on the degree of contextuality and the corresponding unsatisfied part of a quantum contextual configuration with three-element contexts (i.e., lines) located in a multi-qubit symplectic polar space of order two. While the previously used method based on a SAT solver was limited to three qubits, this new method is much fast…
▽ More
We introduce and describe a new heuristic method for finding an upper bound on the degree of contextuality and the corresponding unsatisfied part of a quantum contextual configuration with three-element contexts (i.e., lines) located in a multi-qubit symplectic polar space of order two. While the previously used method based on a SAT solver was limited to three qubits, this new method is much faster and more versatile, enabling us to also handle four- to six-qubit cases. The four-qubit unsatisfied configurations we found are quite remarkable. That of an elliptic quadric features 315 lines and has in its core three copies of the split Cayley hexagon of order two having a Heawood-graph-underpinned geometry in common. That of a hyperbolic quadric also has 315 lines but, as a point-line incidence structure, is isomorphic to the dual $\mathcal{DW}(5,2)$ of $\mathcal{W}(5,2)$. Finally, an unsatisfied configuration with 1575 lines associated with all the lines/contexts of the four-qubit space contains a distinguished $\mathcal{DW}(5,2)$ centered on a point-plane incidence graph of PG$(3,2)$. The corresponding configurations found in the five-qubit space exhibit a considerably higher degree of complexity, except for a hyperbolic quadric, whose 6975 unsatisfied contexts are compactified around the point-hyperplane incidence graph of PG$(4,2)$. The most remarkable unsatisfied patterns discovered in the six-qubit space are a couple of disjoint split Cayley hexagons (for the full space) and a subgeometry underpinned by the complete bipartite graph $K_{7,7}$ (for a hyperbolic quadric).
△ Less
Submitted 3 July, 2024;
originally announced July 2024.
-
Position Error Bound for Cooperative Sensing in MIMO-OFDM Networks
Authors:
Lorenzo Pucci,
Andrea Giorgetti
Abstract:
Only the chairs can edit This paper investigates the fundamental limits of target position estimation accuracy of joint sensing and communication (JSC) networks comprising several monostatic base stations (BSs) that cooperate to localize targets. Specifically, each BS adopts a multiple-input multiple-output (MIMO)-orthogonal frequency division multiplexing (OFDM) scheme with a multi-beam radiation…
▽ More
Only the chairs can edit This paper investigates the fundamental limits of target position estimation accuracy of joint sensing and communication (JSC) networks comprising several monostatic base stations (BSs) that cooperate to localize targets. Specifically, each BS adopts a multiple-input multiple-output (MIMO)-orthogonal frequency division multiplexing (OFDM) scheme with a multi-beam radiation pattern to partition power between communication and sensing tasks. Building on prior works, we derive a general framework to evaluate the positioning accuracy of a target in networks with an arbitrary number of cooperating BSs and arbitrary geometrical configurations using Fisher information. Numerical results demonstrate the benefits of cooperation between BSs in improving target localization accuracy and provide insights into the relationships between various system parameters, which may aid in designing JSC networks.
△ Less
Submitted 30 May, 2024;
originally announced May 2024.
-
Bistatic Sensing at THz Frequencies via a Two-Stage Ultra-Wideband MIMO-OFDM System
Authors:
Tommaso Bacchielli,
Lorenzo Pucci,
Davide Dardari,
Andrea Giorgetti
Abstract:
Only the chairs can edit The availability of abundant bandwidth at terahertz (THz) frequencies holds promise for significantly enhancing the sensing performance of integrated sensing and communication (ISAC) systems in the next-generation wireless systems, enabling high accuracy and resolution for precise target localization. In orthogonal frequency-division multiplexing (OFDM) systems, wide bandw…
▽ More
Only the chairs can edit The availability of abundant bandwidth at terahertz (THz) frequencies holds promise for significantly enhancing the sensing performance of integrated sensing and communication (ISAC) systems in the next-generation wireless systems, enabling high accuracy and resolution for precise target localization. In orthogonal frequency-division multiplexing (OFDM) systems, wide bandwidth can be achieved by increasing the subcarrier spacing rather than the number of subcarriers, thereby keeping the complexity of the sensing system low. However, this approach may lead to an ambiguity problem in target range estimation. To address this issue, this work proposes a two-stage maximum likelihood method for estimating target position in an ultra-wideband bistatic multiple-antenna OFDM-based ISAC system operating at THz frequencies. Numerical results show that the proposed estimation approach effectively resolves the ambiguity problem while achieving high resolution and accuracy target position estimation at a very low signal-to-noise ratio regime.
△ Less
Submitted 28 May, 2024;
originally announced May 2024.
-
Fundamental Trade-Offs in Monostatic ISAC: A Holistic Investigation Towards 6G
Authors:
Musa Furkan Keskin,
Mohammad Mahdi Mojahedian,
Jesus O. Lacruz,
Carina Marcus,
Olof Eriksson,
Andrea Giorgetti,
Joerg Widmer,
Henk Wymeersch
Abstract:
This paper undertakes a holistic investigation of two fundamental trade-offs in monostatic OFDM integrated sensing and communication (ISAC) systems-namely, the time-frequency trade-off and the spatial trade-off, originating from the choice of modulation order for random data and the design of beamforming strategies, respectively. To counteract the elevated side-lobe levels induced by varying-ampli…
▽ More
This paper undertakes a holistic investigation of two fundamental trade-offs in monostatic OFDM integrated sensing and communication (ISAC) systems-namely, the time-frequency trade-off and the spatial trade-off, originating from the choice of modulation order for random data and the design of beamforming strategies, respectively. To counteract the elevated side-lobe levels induced by varying-amplitude data in high-order QAM signaling, we propose a novel linear minimum mean-squared-error (LMMSE) estimator, capable of maintaining robust sensing performance across a wide range of SNRs. Moreover, we explore spatial domain trade-offs through two ISAC transmission strategies: concurrent, employing joint beams, and time-sharing, using separate, time-non-overlapping beams for sensing and communications. Simulations demonstrate superior performance of the LMMSE estimator, especially in detecting weak targets in the presence of strong ones with high-order QAM, consistently yielding more favorable ISAC trade-offs than existing baselines under various modulation schemes, SNR conditions, RCS levels and transmission strategies. We also provide experimental results to validate the effectiveness of the LMMSE estimator in reducing side-lobe levels, based on real-world measurements.
△ Less
Submitted 29 August, 2024; v1 submitted 31 January, 2024;
originally announced January 2024.
-
Hexagons govern three-qubit contextuality
Authors:
Metod Saniga,
Frédéric Holweck,
Colm Kelleher,
Axel Muller,
Alain Giorgetti,
Henri de Boutray
Abstract:
Split Cayley hexagons of order two are distinguished finite geometries living in the three-qubit symplectic polar space in two different forms, called classical and skew. Although neither of the two yields observable-based contextual configurations of their own, {\it classically}-embedded copies are found to fully encode contextuality properties of the most prominent three-qubit contextual configu…
▽ More
Split Cayley hexagons of order two are distinguished finite geometries living in the three-qubit symplectic polar space in two different forms, called classical and skew. Although neither of the two yields observable-based contextual configurations of their own, {\it classically}-embedded copies are found to fully encode contextuality properties of the most prominent three-qubit contextual configurations in the following sense: for each set of unsatisfiable contexts of such a contextual configuration there exists some classically-embedded hexagon sharing with the configuration exactly this set of contexts and nothing else. We demonstrate this fascinating property first on the configuration comprising all 315 contexts of the space and then on doilies, both types of quadrics as well as on complements of skew-embedded hexagons. In connection with the last-mentioned case and elliptic quadrics we also conducted some experimental tests on a Noisy Intermediate Scale Quantum (NISQ) computer to substantiate our theoretical findings.
△ Less
Submitted 22 January, 2025; v1 submitted 12 December, 2023;
originally announced December 2023.
-
Sensor Fusion and Resource Management in MIMO-OFDM Joint Sensing and Communication
Authors:
Elia Favarelli,
Elisabetta Matricardi,
Lorenzo Pucci,
Wen Xu,
Enrico Paolini,
Andrea Giorgetti
Abstract:
This study explores the promising potential of integrating sensing capabilities into multiple-input multiple-output (MIMO)-orthogonal frequency division multiplexing (OFDM)-based networks through innovative multi-sensor fusion techniques, tracking algorithms, and resource management. A novel data fusion technique is proposed within the MIMO-OFDM system, which promotes cooperative sensing among mon…
▽ More
This study explores the promising potential of integrating sensing capabilities into multiple-input multiple-output (MIMO)-orthogonal frequency division multiplexing (OFDM)-based networks through innovative multi-sensor fusion techniques, tracking algorithms, and resource management. A novel data fusion technique is proposed within the MIMO-OFDM system, which promotes cooperative sensing among monostatic joint sensing and communication (JSC) base stations by sharing range-angle maps with a central fusion center. To manage data sharing and control network overhead introduced by cooperation, an excision filter is introduced at each base station. After data fusion, the framework employs a three-step clustering procedure combined with a tracking algorithm to effectively handle point-like and extended targets. Delving into the sensing/communication trade-off, resources such as transmit power, frequency, and time are varied, providing valuable insights into their impact on the overall system performance. Additionally, a sophisticated channel model is proposed, accounting for complex urban propagation scenarios and addressing multipath effects and multiple reflection points for extended targets like vehicles. Evaluation metrics, including optimal sub-pattern assignment (OSPA), downlink sum rate, and bit rate, offer a comprehensive assessment of the system's localization and communication capabilities, as well as network overhead.
△ Less
Submitted 12 December, 2023;
originally announced December 2023.
-
Multi-Base Station Cooperative Sensing with AI-Aided Tracking
Authors:
Elia Favarelli,
Elisabetta Matricardi,
Lorenzo Pucci,
Enrico Paolini,
Wen Xu,
Andrea Giorgetti
Abstract:
In this work, we investigate the performance of a joint sensing and communication (JSC) network consisting of multiple base stations (BSs) that cooperate through a fusion center (FC) to exchange information about the sensed environment while concurrently establishing communication links with a set of user equipments (UEs). Each BS within the network operates as a monostatic radar system, enabling…
▽ More
In this work, we investigate the performance of a joint sensing and communication (JSC) network consisting of multiple base stations (BSs) that cooperate through a fusion center (FC) to exchange information about the sensed environment while concurrently establishing communication links with a set of user equipments (UEs). Each BS within the network operates as a monostatic radar system, enabling comprehensive scanning of the monitored area and generating range-angle maps that provide information regarding the position of a group of heterogeneous objects. The acquired maps are subsequently fused in the FC. Then, a convolutional neural network (CNN) is employed to infer the category of the targets, e.g., pedestrians or vehicles, and such information is exploited by an adaptive clustering algorithm to group the detections originating from the same target more effectively. Finally, two multi-target tracking algorithms, the probability hypothesis density (PHD) filter and multi-Bernoulli mixture (MBM) filter, are applied to estimate the state of the targets. Numerical results demonstrated that our framework could provide remarkable sensing performance, achieving an optimal sub-pattern assignment (OSPA) less than 60 cm, while keeping communication services to UEs with a reduction of the communication capacity in the order of 10% to 20%. The impact of the number of BSs engaged in sensing is also examined, and we show that in the specific case study, 3 BSs ensure a localization error below 1 m.
△ Less
Submitted 31 October, 2023;
originally announced October 2023.
-
Performance Analysis of a Low-Complexity OTFS Integrated Sensing and Communication System
Authors:
Tommaso Bacchielli,
Lorenzo Pucci,
Enrico Paolini,
Andrea Giorgetti
Abstract:
This work proposes a low-complexity estimation approach for an orthogonal time frequency space (OTFS)-based integrated sensing and communication (ISAC) system. In particular, we first define four low-dimensional matrices used to compute the channel matrix through simple algebraic manipulations. Secondly, we establish an analytical criterion, independent of system parameters, to identify the most i…
▽ More
This work proposes a low-complexity estimation approach for an orthogonal time frequency space (OTFS)-based integrated sensing and communication (ISAC) system. In particular, we first define four low-dimensional matrices used to compute the channel matrix through simple algebraic manipulations. Secondly, we establish an analytical criterion, independent of system parameters, to identify the most informative elements within these derived matrices, leveraging the properties of the Dirichlet kernel. This allows the distilling of such matrices, keeping only those entries that are essential for detection, resulting in an efficient, low-complexity implementation of the sensing receiver. Numerical results, which refer to a vehicular scenario, demonstrate that the proposed approximation technique effectively preserves the sensing performance, evaluated in terms of root mean square error (RMSE) of the range and velocity estimation, while concurrently reducing the computational effort enormously.
△ Less
Submitted 16 October, 2023;
originally announced October 2023.
-
Multi-static Parameter Estimation in the Near/Far Field Beam Space for Integrated Sensing and Communication Applications
Authors:
Saeid K. Dehkordi,
Lorenzo Pucci,
Peter Jung,
Andrea Giorgetti,
Enrico Paolini,
Giuseppe Caire
Abstract:
This work proposes a maximum likelihood (ML)-based parameter estimation framework for a millimeter wave (mmWave) integrated sensing and communication (ISAC) system in a multi-static configuration using energy-efficient hybrid digital-analog arrays. Due to the typically large arrays deployed in the higher frequency bands to mitigate isotropic path loss, such arrays may operate in the near-field reg…
▽ More
This work proposes a maximum likelihood (ML)-based parameter estimation framework for a millimeter wave (mmWave) integrated sensing and communication (ISAC) system in a multi-static configuration using energy-efficient hybrid digital-analog arrays. Due to the typically large arrays deployed in the higher frequency bands to mitigate isotropic path loss, such arrays may operate in the near-field regime. The proposed parameter estimation in this work consists of a two-stage estimation process, where the first stage is based on far-field assumptions, and is used to obtain a first estimate of the target parameters. In cases where the target is determined to be in the near-field of the arrays, a second estimation based on near-field assumptions is carried out to obtain more accurate estimates. In particular, we select beamfocusing array weights designed to achieve a constant gain over an extended spatial region and re-estimate the target parameters at the receivers. We evaluate the effectiveness of the proposed framework in numerous scenarios through numerical simulations and demonstrate the impact of the custom-designed flat-gain beamfocusing codewords in increasing the communication performance of the system.
△ Less
Submitted 26 September, 2023;
originally announced September 2023.
-
New and improved bounds on the contextuality degree of multi-qubit configurations
Authors:
Axel Muller,
Metod Saniga,
Alain Giorgetti,
Henri de Boutray,
Frédéric Holweck
Abstract:
We present algorithms and a C code to reveal quantum contextuality and evaluate the contextuality degree (a way to quantify contextuality) for a variety of point-line geometries located in binary symplectic polar spaces of small rank. With this code we were not only able to recover, in a more efficient way, all the results of a recent paper by de Boutray et al [(2022). Journal of Physics A: Mathem…
▽ More
We present algorithms and a C code to reveal quantum contextuality and evaluate the contextuality degree (a way to quantify contextuality) for a variety of point-line geometries located in binary symplectic polar spaces of small rank. With this code we were not only able to recover, in a more efficient way, all the results of a recent paper by de Boutray et al [(2022). Journal of Physics A: Mathematical and Theoretical 55 475301], but also arrived at a bunch of new noteworthy results. The paper first describes the algorithms and the C code. Then it illustrates its power on a number of subspaces of symplectic polar spaces whose rank ranges from 2 to 7. The most interesting new results include: (i) non-contextuality of configurations whose contexts are subspaces of dimension 2 and higher, (ii) non-existence of negative subspaces of dimension 3 and higher, (iii) considerably improved bounds for the contextuality degree of both elliptic and hyperbolic quadrics for rank 4, as well as for a particular subgeometry of the three-qubit space whose contexts are the lines of this space, (iv) proof for the non-contextuality of perpsets and, last but not least, (v) contextual nature of a distinguished subgeometry of a multi-qubit doily, called a two-spread, and computation of its contextuality degree. Finally, in the three-qubit polar space we correct and improve the contextuality degree of the full configuration and also describe finite geometric configurations formed by unsatisfiable/invalid constraints for both types of quadrics as well as for the geometry whose contexts are all 315 lines of the space.
△ Less
Submitted 31 May, 2024; v1 submitted 17 May, 2023;
originally announced May 2023.
-
Experimental Demonstration of Partially Disaggregated Optical Network Control Using the Physical Layer Digital Twin
Authors:
Giacomo Borraccini,
Stefano Straullu,
Alessio Giorgetti,
Renato Ambrosone,
Emanuele Virgillito,
Andrea D'Amico,
Rocco D'Ingillo,
Francesco Aquilino,
Antonino Nespola,
Nicola Sambo,
Filippo Cugini,
Vittorio Curri
Abstract:
Optical communications and networking are fast becoming the solution to support ever-increasing data traffic across all segments of the network, expanding from core/metro networks to 5G/6G front-hauling. Therefore, optical networks need to evolve towards an efficient exploitation of the infrastructure by overcoming the closed and aggregated paradigm, to enable apparatus sharing together with the s…
▽ More
Optical communications and networking are fast becoming the solution to support ever-increasing data traffic across all segments of the network, expanding from core/metro networks to 5G/6G front-hauling. Therefore, optical networks need to evolve towards an efficient exploitation of the infrastructure by overcoming the closed and aggregated paradigm, to enable apparatus sharing together with the slicing and separation of the optical data plane from the optical control. In addition to the advantages in terms of efficiency and cost reduction, this evolution will increase the network reliability, also allowing for a fine trade-off between robustness and maximum capacity exploitation. In this work, an optical network architecture is presented based on the physical layer digital twin of the optical transport used within a multi-layer hierarchical control operated by an intent-based network operating system. An experimental proof of concept is performed on a three node network including up to 1000 km optical transmission, open re-configurable optical add & drop multiplexers (ROADMs) and white-box transponders hosting pluggable multi-rate transceivers. The proposed solution is based on GNPy as optical physical layer digital twin and ONOS as intent-based network operating system. The reliability of the optical control decoupled by the data plane functioning is experimentally demonstrated exploiting GNPy as open lightpath computation engine and software optical amplifier models derived from the component characterization. Besides the lightpath deployment exploiting the modulation format evaluation given a generic traffic request, the architecture reliability is tested mimicking the use case of an automatic failure recovery from a fiber cut.
△ Less
Submitted 22 December, 2022;
originally announced December 2022.
-
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families
Authors:
Catherine Dubois,
Nicolas Magaud,
Alain Giorgetti
Abstract:
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are very compact ones and usually rely on the use of dependent types, but they tend to be difficult to handle in practice. On the contrary, implementations based on a larger (and simpler) data structure combined with a restrict…
▽ More
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are very compact ones and usually rely on the use of dependent types, but they tend to be difficult to handle in practice. On the contrary, implementations based on a larger (and simpler) data structure combined with a restriction property are much easier to deal with.
In this work, we study several families related to lambda terms, among which Motzkin trees, seen as lambda term skeletons, closable Motzkin trees, corresponding to closed lambda terms, and a parameterized family of open lambda terms. For each of these families, we define two different representations, show that they are isomorphic and provide tools to switch from one representation to another. All these datatypes and their associated transformations are implemented in the Coq proof assistant. Furthermore we implement random generators for each representation, using the QuickChick plugin.
△ Less
Submitted 20 December, 2022;
originally announced December 2022.
-
Multi-qubit doilies: enumeration for all ranks and classification for ranks four and five
Authors:
Axel Muller,
Metod Saniga,
Alain Giorgetti,
Henri De Boutray,
Frédéric Holweck
Abstract:
For $N \geq 2$, an $N$-qubit doily is a doily living in the $N$-qubit symplectic polar space. These doilies are related to operator-based proofs of quantum contextuality. Following and extending the strategy of Saniga et al. (Mathematics 9 (2021) 2272) that focused exclusively on three-qubit doilies, we first bring forth several formulas giving the number of both linear and quadratic doilies for a…
▽ More
For $N \geq 2$, an $N$-qubit doily is a doily living in the $N$-qubit symplectic polar space. These doilies are related to operator-based proofs of quantum contextuality. Following and extending the strategy of Saniga et al. (Mathematics 9 (2021) 2272) that focused exclusively on three-qubit doilies, we first bring forth several formulas giving the number of both linear and quadratic doilies for any $N > 2$. Then we present an effective algorithm for the generation of all $N$-qubit doilies. Using this algorithm for $N=4$ and $N=5$, we provide a classification of $N$-qubit doilies in terms of types of observables they feature and number of negative lines they are endowed with. We also list several distinguished findings about $N$-qubit doilies that are absent in the three-qubit case, point out a couple of specific features exhibited by linear doilies and outline some prospective extensions of our approach.
△ Less
Submitted 25 November, 2022; v1 submitted 7 June, 2022;
originally announced June 2022.
-
Demonstration of latency-aware 5G network slicing on optical metro networks
Authors:
B. Shariati,
L. Velasco,
J. -J. Pedreño-Manresa,
A. Dochhan,
R. Casellas,
A. Muqaddas,
O. González de Dios,
L. Luque Canto,
B. Lent,
J. E. López de Vergara,
S. López-Buedo,
F. Moreno,
P. Pavón,
M. Ruiz,
S. K. Patri,
A. Giorgetti,
F. Cugini,
A. Sgambelluri,
R. Nejabati,
D. Simeonidou,
R. -P. Braun,
A. Autenrieth,
J. -P. Elbers,
J. K. Fischer,
R. Freund
Abstract:
The H2020 METRO-HAUL European project has architected a latency-aware, cost-effective, agile, and programmable optical metro network. This includes the design of semidisaggregated metro nodes with compute and storage capabilities, which interface effectively with both 5G access and multi-Tbit/s elastic optical networks in the core. In this paper, we report the automated deployment of 5G services,…
▽ More
The H2020 METRO-HAUL European project has architected a latency-aware, cost-effective, agile, and programmable optical metro network. This includes the design of semidisaggregated metro nodes with compute and storage capabilities, which interface effectively with both 5G access and multi-Tbit/s elastic optical networks in the core. In this paper, we report the automated deployment of 5G services, in particular, a public safety video surveillance use case employing low-latency object detection and tracking using on-camera and on-the-edge analytics. The demonstration features flexible deployment of network slice instances, implemented in terms of European Telecommunications Standards Institute (ETSI) network function virtualization network services. We summarize the key findings in a detailed analysis of end-to-end quality of service, service setup time, and soft-failure detection time. The results show that the round-trip time over an 80 km link is under 800s and the service deployment time is under 180s.
△ Less
Submitted 21 February, 2022;
originally announced February 2022.
-
System-Level Analysis of Joint Sensing and Communication based on 5G New Radio
Authors:
Lorenzo Pucci,
Enrico Paolini,
Andrea Giorgetti
Abstract:
This work investigates a multibeam system for joint sensing and communication (JSC) based on multiple-input multiple-output (MIMO) 5G new radio (NR) waveforms. In particular, we consider a base station (BS) acting as a monostatic sensor that estimates the range, speed, and direction of arrival (DoA) of multiple targets via beam scanning using a fraction of the transmitted power. The target positio…
▽ More
This work investigates a multibeam system for joint sensing and communication (JSC) based on multiple-input multiple-output (MIMO) 5G new radio (NR) waveforms. In particular, we consider a base station (BS) acting as a monostatic sensor that estimates the range, speed, and direction of arrival (DoA) of multiple targets via beam scanning using a fraction of the transmitted power. The target position is then obtained via range and DoA estimation. We derive the sensing performance in terms of probability of detection and root mean squared error (RMSE) of position and velocity estimation of a target under line-of-sight (LOS) conditions. Furthermore, we evaluate the system performance when multiple targets are present, using the optimal sub-pattern assignment (OSPA) metric. Finally, we provide an in-depth investigation of the dominant factors that affect performance, including the fraction of power reserved for sensing.
△ Less
Submitted 28 January, 2022;
originally announced January 2022.
-
A Track-Before-Detect Algorithm for UWB Radar Sensor Networks
Authors:
B. Yan,
A. Giorgetti,
E. Paolini
Abstract:
Precise localization and tracking of moving non-collaborative persons and objects using a network of ultra-wideband (UWB) radar nodes has been shown to represent a practical and effective approach. In UWB radar sensor networks (RSNs), existence of strong clutter, weak target echoes, and closely spaced targets are obstacles to achieving a satisfactory tracking performance. Using a track-before-dete…
▽ More
Precise localization and tracking of moving non-collaborative persons and objects using a network of ultra-wideband (UWB) radar nodes has been shown to represent a practical and effective approach. In UWB radar sensor networks (RSNs), existence of strong clutter, weak target echoes, and closely spaced targets are obstacles to achieving a satisfactory tracking performance. Using a track-before-detect (TBD) approach, the waveform obtained by each node during a time period are jointly processed. Both spatial information and temporal relationship between measurements are exploited in generating all possible candidate trajectories and only the best trajectories are selected as the outcome. The effectiveness of the developed TBD technique for UWB RSNs is confirmed by numerical simulations and by two experimental results, both carried out with actual UWB signals. In the first experiment, a human target is tracked by a monostatic radar network with an average localization error of 41.9 cm with no false alarm trajectory in a cluttered outdoor environment. In the second experiment, two targets are detected by multistatic radar network with localization errors of 25.4 cm and 19.7 cm, and detection rate of the two targets is 88.75%, and no false alarm trajectory.
△ Less
Submitted 1 August, 2021;
originally announced August 2021.
-
A Latency-Aware Real-Time Video Surveillance Demo: Network Slicing for Improving Public Safety
Authors:
B. Shariati,
J. J. Pedreno-Manresa,
A. Dochhan,
A. S. Muqaddas,
R. Casellas,
O. González de Dios,
L. L. Canto,
B. Lent,
J. E. López de Vergara,
S. López-Buedo,
F. J. Moreno,
P. Pavón,
L. Velasco,
S. Patri,
A. Giorgetti,
F. Cugini,
A. Sgambelluri,
R. Nejabati,
D. Simeonidou,
R,
-P,
Braun,
A. Autenrieth,
J. -P. Elbers,
J. K. Fischer
, et al. (1 additional authors not shown)
Abstract:
We report the automated deployment of 5G services across a latency-aware, semidisaggregated, and virtualized metro network. We summarize the key findings in a detailed analysis of end-to-end latency, service setup time, and soft-failure detection time.
We report the automated deployment of 5G services across a latency-aware, semidisaggregated, and virtualized metro network. We summarize the key findings in a detailed analysis of end-to-end latency, service setup time, and soft-failure detection time.
△ Less
Submitted 6 July, 2021;
originally announced July 2021.
-
Contextuality degree of quadrics in multi-qubit symplectic polar spaces
Authors:
Henri de Boutray,
Frédéric Holweck,
Alain Giorgetti,
Pierre-Alain Masson,
Metod Saniga
Abstract:
Quantum contextuality takes an important place amongst the concepts of quantum computing that bring an advantage over its classical counterpart. For a large class of contextuality proofs, aka. observable-based proofs of the Kochen-Specker Theorem, we formulate the contextuality property as the absence of solutions to a linear system and define for a contextual configuration its degree of contextua…
▽ More
Quantum contextuality takes an important place amongst the concepts of quantum computing that bring an advantage over its classical counterpart. For a large class of contextuality proofs, aka. observable-based proofs of the Kochen-Specker Theorem, we formulate the contextuality property as the absence of solutions to a linear system and define for a contextual configuration its degree of contextuality. Then we explain why subgeometries of binary symplectic polar spaces are candidates for contextuality proofs. We report the results of a software that generates these subgeometries, decides their contextuality and computes their contextuality degree for some small symplectic polar spaces. We show that quadrics in the symplectic polar space $W_n$ are contextual for $n=3,4,5$. The proofs we consider involve more contexts and observables than the smallest known proofs. This intermediate size property of those proofs is interesting for experimental tests, but could also be interesting in quantum game theory.
△ Less
Submitted 20 March, 2023; v1 submitted 28 May, 2021;
originally announced May 2021.
-
Taxonomy of Polar Subspaces of Multi-Qubit Symplectic Polar Spaces of Small Rank
Authors:
Metod Saniga,
Henri de Boutray,
Frederic Holweck,
Alain Giorgetti
Abstract:
We study certain physically-relevant subgeometries of binary symplectic polar spaces $W(2N-1,2)$ of small rank $N$, when the points of these spaces canonically encode $N$-qubit observables. Key characteristics of a subspace of such a space $W(2N-1,2)$ are: the number of its negative lines, the distribution of types of observables, the character of the geometric hyperplane the subspace shares with…
▽ More
We study certain physically-relevant subgeometries of binary symplectic polar spaces $W(2N-1,2)$ of small rank $N$, when the points of these spaces canonically encode $N$-qubit observables. Key characteristics of a subspace of such a space $W(2N-1,2)$ are: the number of its negative lines, the distribution of types of observables, the character of the geometric hyperplane the subspace shares with the distinguished (non-singular) quadric of $W(2N-1,2)$ and the structure of its Veldkamp space. In particular, we classify and count polar subspaces of $W(2N-1,2)$ whose rank is $N-1$. $W(3,2)$ features three negative lines of the same type and its $W(1,2)$'s are of five different types. $W(5,2)$ is endowed with 90 negative lines of two types and its $W(3,2)$'s split into 13 types. 279 out of 480 $W(3,2)$'s with three negative lines are composite, i.\,e. they all originate from the two-qubit $W(3,2)$. Given a three-qubit $W(3,2)$ and any of its geometric hyperplanes, there are three other $W(3,2)$'s possessing the same hyperplane. The same holds if a geometric hyperplane is replaced by a `planar' tricentric triad. A hyperbolic quadric of $W(5,2)$ is found to host particular sets of seven $W(3,2)$'s, each of them being uniquely tied to a Conwell heptad with respect to the quadric. There is also a particular type of $W(3,2)$'s, a representative of which features a point each line through which is negative. Finally, $W(7,2)$ is found to possess 1908 negative lines of five types and its $W(5,2)$'s fall into as many as 29 types. 1524 out of 1560 $W(5,2)$'s with 90 negative lines originate from the three-qubit $W(5,2)$. Remarkably, the difference in the number of negative lines for any two distinct types of four-qubit $W(5,2)$'s is a multiple of four.
△ Less
Submitted 25 July, 2021; v1 submitted 8 May, 2021;
originally announced May 2021.
-
Mermin Polynomials for Entanglement Evaluation in Grover's algorithm and Quantum Fourier Transform
Authors:
Henri de Boutray,
Hamza Jaffali,
Frédéric Holweck,
Alain Giorgetti,
Pierre-Alain Masson
Abstract:
The entanglement of a quantum system can be valuated using Mermin polynomials. This gives us a means to study entanglement evolution during the execution of quantum algorithms. We first consider Grover's quantum search algorithm, noticing that states during the algorithm are maximally entangled in the direction of a single constant state, which allows us to search for a single optimal Mermin opera…
▽ More
The entanglement of a quantum system can be valuated using Mermin polynomials. This gives us a means to study entanglement evolution during the execution of quantum algorithms. We first consider Grover's quantum search algorithm, noticing that states during the algorithm are maximally entangled in the direction of a single constant state, which allows us to search for a single optimal Mermin operator and use it to evaluate entanglement through the whole execution of Grover's algorithm. Then the Quantum Fourier Transform is also studied with Mermin polynomials. A different optimal Mermin operator is searched at each execution step, since in this case there is no single direction of evolution. The results for the Quantum Fourier Transform are compared to results from a previous study of entanglement with Cayley hyperdeterminant. All our computations can be replayed thanks to a structured and documented open-source code that we provide.
△ Less
Submitted 15 January, 2020;
originally announced January 2020.
-
Model Order Selection Based on Information Theoretic Criteria: Design of the Penalty
Authors:
Andrea Mariani,
Andrea Giorgetti,
Marco Chiani
Abstract:
Information theoretic criteria (ITC) have been widely adopted in engineering and statistics for selecting, among an ordered set of candidate models, the one that better fits the observed sample data. The selected model minimizes a penalized likelihood metric, where the penalty is determined by the criterion adopted. While rules for choosing a penalty that guarantees a consistent estimate of the mo…
▽ More
Information theoretic criteria (ITC) have been widely adopted in engineering and statistics for selecting, among an ordered set of candidate models, the one that better fits the observed sample data. The selected model minimizes a penalized likelihood metric, where the penalty is determined by the criterion adopted. While rules for choosing a penalty that guarantees a consistent estimate of the model order are known, theoretical tools for its design with finite samples have never been provided in a general setting. In this paper, we study model order selection for finite samples under a design perspective, focusing on the generalized information criterion (GIC), which embraces the most common ITC. The theory is general, and as case studies we consider: a) the problem of estimating the number of signals embedded in additive white Gaussian noise (AWGN) by using multiple sensors; b) model selection for the general linear model (GLM), which includes e.g. the problem of estimating the number of sinusoids in AWGN. The analysis reveals a trade-off between the probabilities of overestimating and underestimating the order of the model. We then propose to design the GIC penalty to minimize underestimation while keeping the overestimation probability below a specified level. For the considered problems, this method leads to analytical derivation of the optimal penalty for a given sample size. A performance comparison between the penalty optimized GIC and common AIC and BIC is provided, demonstrating the effectiveness of the proposed design strategy.
△ Less
Submitted 4 October, 2019;
originally announced October 2019.
-
On Oversampling-Based Signal Detection
Authors:
Andrea Mariani,
Andrea Giorgetti,
Marco Chiani
Abstract:
The availability of inexpensive devices allows nowadays to implement cognitive radio functionalities in large-scale networks such as the internet-of-things and future mobile cellular systems. In this paper, we focus on wideband spectrum sensing in the presence of oversampling, i.e., the sampling frequency of a digital receiver is larger than the signal bandwidth, where signal detection must take i…
▽ More
The availability of inexpensive devices allows nowadays to implement cognitive radio functionalities in large-scale networks such as the internet-of-things and future mobile cellular systems. In this paper, we focus on wideband spectrum sensing in the presence of oversampling, i.e., the sampling frequency of a digital receiver is larger than the signal bandwidth, where signal detection must take into account the front-end impairments of low-cost devices. Based on the noise model of a software-defined radio dongle, we address the problem of robust signal detection in the presence of noise power uncertainty and non-flat noise power spectral density (PSD). In particular, we analyze the receiver operating characteristic of several detectors in the presence of such front-end impairments, to assess the performance attainable in a real-world scenario. We propose new frequency-domain detectors, some of which are proven to outperform previously proposed spectrum sensing techniques such as, e.g., eigenvalue-based tests. The study shows that the best performance is provided by a noise-uncertainty immune energy detector (ED) and, for the colored noise case, by tests that match the PSD of the receiver noise.
△ Less
Submitted 31 July, 2019;
originally announced July 2019.
-
Limits on Sparse Data Acquisition: RIC Analysis of Finite Gaussian Matrices
Authors:
Ahmed Elzanaty,
Andrea Giorgetti,
Marco Chiani
Abstract:
One of the key issues in the acquisition of sparse data by means of compressed sensing (CS) is the design of the measurement matrix. Gaussian matrices have been proven to be information-theoretically optimal in terms of minimizing the required number of measurements for sparse recovery. In this paper we provide a new approach for the analysis of the restricted isometry constant (RIC) of finite dim…
▽ More
One of the key issues in the acquisition of sparse data by means of compressed sensing (CS) is the design of the measurement matrix. Gaussian matrices have been proven to be information-theoretically optimal in terms of minimizing the required number of measurements for sparse recovery. In this paper we provide a new approach for the analysis of the restricted isometry constant (RIC) of finite dimensional Gaussian measurement matrices. The proposed method relies on the exact distributions of the extreme eigenvalues for Wishart matrices. First, we derive the probability that the restricted isometry property is satisfied for a given sufficient recovery condition on the RIC, and propose a probabilistic framework to study both the symmetric and asymmetric RICs. Then, we analyze the recovery of compressible signals in noise through the statistical characterization of stability and robustness. The presented framework determines limits on various sparse recovery algorithms for finite size problems. In particular, it provides a tight lower bound on the maximum sparsity order of the acquired data allowing signal recovery with a given target probability. Also, we derive simple approximations for the RICs based on the Tracy-Widom distribution.
△ Less
Submitted 22 November, 2018; v1 submitted 9 February, 2018;
originally announced February 2018.
-
Open Boundary Simulations of Proteins and Their Hydration Shells by Hamiltonian Adaptive Resolution Scheme
Authors:
Thomas Tarenzi,
Vania Calandrini,
Raffaello Potestio,
Alejandro Giorgetti,
Paolo Carloni
Abstract:
The recently proposed Hamiltonian Adaptive Resolution Scheme (H-AdResS) allows to perform molecular simulations in an open boundary framework. It allows to change on the fly the resolution of specific subset of molecules (usually the solvent), which are free to diffuse between the atomistic region and the coarse-grained reservoir. So far, the method has been successfully applied to pure liquids. C…
▽ More
The recently proposed Hamiltonian Adaptive Resolution Scheme (H-AdResS) allows to perform molecular simulations in an open boundary framework. It allows to change on the fly the resolution of specific subset of molecules (usually the solvent), which are free to diffuse between the atomistic region and the coarse-grained reservoir. So far, the method has been successfully applied to pure liquids. Coupling the H-AdResS methodology to hybrid models of proteins, such as the Molecular Mechanics/Coarse-Grained (MM/CG) scheme, is a promising approach for rigorous calculations of ligand binding free energies in low-resolution protein models. Towards this goal, here we apply for the first time H-AdResS to two atomistic proteins in dual-resolution solvent, proving its ability to reproduce structural and dynamic properties of both the proteins and the solvent, as obtained from atomistic simulations.
△ Less
Submitted 15 November, 2017;
originally announced November 2017.
-
Enumeration of Hypermaps of a Given Genus
Authors:
Alain Giorgetti,
Timothy R. S. Walsh
Abstract:
This paper addresses the enumeration of rooted and unrooted hypermaps of a given genus. For rooted hypermaps the enumeration method consists of considering the more general family of multirooted hypermaps, in which darts other than the root dart are distinguished. We give functional equations for the generating series counting multirooted hypermaps of a given genus by number of darts, vertices, ed…
▽ More
This paper addresses the enumeration of rooted and unrooted hypermaps of a given genus. For rooted hypermaps the enumeration method consists of considering the more general family of multirooted hypermaps, in which darts other than the root dart are distinguished. We give functional equations for the generating series counting multirooted hypermaps of a given genus by number of darts, vertices, edges, faces and the degrees of the vertices containing the distinguished darts. We solve these equations to get parametric expressions of the generating functions of rooted hypermaps of low genus. We also count unrooted hypermaps of given genus by number of darts, vertices, hyperedges and faces.
△ Less
Submitted 21 June, 2018; v1 submitted 30 October, 2015;
originally announced October 2015.
-
Your Proof Fails? Testing Helps to Find the Reason
Authors:
Guillaume Petiot,
Nikolai Kosmatov,
Bernard Botella,
Alain Giorgetti,
Jacques Julliand
Abstract:
Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification…
▽ More
Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a new methodology where test generation helps to identify the reason of a proof failure and to exhibit a counter-example clearly illustrating the issue. We describe how to transform an annotated C program into C code suitable for testing and illustrate the benefits of the method on comprehensive examples. The method has been implemented in STADY, a plugin of the software analysis platform FRAMA-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures.
△ Less
Submitted 7 August, 2015;
originally announced August 2015.
-
A correspondence between rooted planar maps and normal planar lambda terms
Authors:
Noam Zeilberger,
Alain Giorgetti
Abstract:
A rooted planar map is a connected graph embedded in the 2-sphere, with one edge marked and assigned an orientation. A term of the pure lambda calculus is said to be linear if every variable is used exactly once, normal if it contains no beta-redexes, and planar if it is linear and the use of variables moreover follows a deterministic stack discipline. We begin by showing that the sequence countin…
▽ More
A rooted planar map is a connected graph embedded in the 2-sphere, with one edge marked and assigned an orientation. A term of the pure lambda calculus is said to be linear if every variable is used exactly once, normal if it contains no beta-redexes, and planar if it is linear and the use of variables moreover follows a deterministic stack discipline. We begin by showing that the sequence counting normal planar lambda terms by a natural notion of size coincides with the sequence (originally computed by Tutte) counting rooted planar maps by number of edges. Next, we explain how to apply the machinery of string diagrams to derive a graphical language for normal planar lambda terms, extracted from the semantics of linear lambda calculus in symmetric monoidal closed categories equipped with a linear reflexive object or a linear reflexive pair. Finally, our main result is a size-preserving bijection between rooted planar maps and normal planar lambda terms, which we establish by explaining how Tutte decomposition of rooted planar maps (into vertex maps, maps with an isthmic root, and maps with a non-isthmic root) may be naturally replayed in linear lambda calculus, as certain surgeries on the string diagrams of normal planar lambda terms.
△ Less
Submitted 25 September, 2015; v1 submitted 21 August, 2014;
originally announced August 2014.
-
Constructing large tables of numbers of maps by orientable genus
Authors:
Alain Giorgetti,
Timothy R. S. Walsh
Abstract:
The Carrell-Chapuy recurrence formulas dramatically improve the efficiency of counting orientable rooted maps by genus, either by number of edges alone or by number of edges and vertices. This paper presents an implementation of these formulas with three applications: the computation of an explicit rational expression for the ordinary generating functions of rooted map numbers with a given positiv…
▽ More
The Carrell-Chapuy recurrence formulas dramatically improve the efficiency of counting orientable rooted maps by genus, either by number of edges alone or by number of edges and vertices. This paper presents an implementation of these formulas with three applications: the computation of an explicit rational expression for the ordinary generating functions of rooted map numbers with a given positive genus, the construction of large tables of rooted map numbers, and the use of these tables, together with the method of A. Mednykh and R. Nedela, to count unrooted maps by genus and number of edges and vertices.
△ Less
Submitted 3 May, 2014;
originally announced May 2014.
-
Quantum contextual finite geometries from dessins d'enfants
Authors:
Michel Planat,
Alain Giorgetti,
Frédéric Holweck,
Metod Saniga
Abstract:
We point out an explicit connection between graphs drawn on compact Riemann surfaces defined over the field $\bar{\mathbb{Q}}$ of algebraic numbers --- so-called Grothendieck's {\it dessins d'enfants} --- and a wealth of distinguished point-line configurations. These include simplices, cross-polytopes, several notable projective configurations, a number of multipartite graphs and some 'exotic' geo…
▽ More
We point out an explicit connection between graphs drawn on compact Riemann surfaces defined over the field $\bar{\mathbb{Q}}$ of algebraic numbers --- so-called Grothendieck's {\it dessins d'enfants} --- and a wealth of distinguished point-line configurations. These include simplices, cross-polytopes, several notable projective configurations, a number of multipartite graphs and some 'exotic' geometries. Among them, remarkably, we find not only those underlying Mermin's magic square and magic pentagram, but also those related to the geometry of two- and three-qubit Pauli groups. Of particular interest is the occurrence of all the three types of slim generalized quadrangles, namely GQ(2,1), GQ(2,2) and GQ(2,4), and a couple of closely related graphs, namely the Schläfli and Clebsch ones. These findings seem to indicate that {\it dessins d'enfants} may provide us with a new powerful tool for gaining deeper insight into the nature of finite-dimensional Hilbert spaces and their associated groups, with a special emphasis on contextuality.
△ Less
Submitted 4 September, 2015; v1 submitted 16 October, 2013;
originally announced October 2013.
-
Lazy AC-Pattern Matching for Rewriting
Authors:
Walid Belkhir,
Alain Giorgetti
Abstract:
We define a lazy pattern-matching mechanism modulo associativity and commutativity. The solutions of a pattern-matching problem are stored in a lazy list composed of a first substitution at the head and a non-evaluated object that encodes the remaining computations. We integrate the lazy AC-matching in a strategy language: rewriting rule and strategy application produce a lazy list of terms.
We define a lazy pattern-matching mechanism modulo associativity and commutativity. The solutions of a pattern-matching problem are stored in a lazy list composed of a first substitution at the head and a non-evaluated object that encodes the remaining computations. We integrate the lazy AC-matching in a strategy language: rewriting rule and strategy application produce a lazy list of terms.
△ Less
Submitted 24 April, 2012;
originally announced April 2012.
-
A Symbolic Transformation Language and its Application to a Multiscale Method
Authors:
Walid Belkhir,
Alain Giorgetti,
Michel Lenczner
Abstract:
The context of this work is the design of a software, called MEMSALab, dedicated to the automatic derivation of multiscale models of arrays of micro- and nanosystems. In this domain a model is a partial differential equation. Multiscale methods approximate it by another partial differential equation which can be numerically simulated in a reasonable time. The challenge consists in taking into acco…
▽ More
The context of this work is the design of a software, called MEMSALab, dedicated to the automatic derivation of multiscale models of arrays of micro- and nanosystems. In this domain a model is a partial differential equation. Multiscale methods approximate it by another partial differential equation which can be numerically simulated in a reasonable time. The challenge consists in taking into account a wide range of geometries combining thin and periodic structures with the possibility of multiple nested scales.
In this paper we present a transformation language that will make the development of MEMSALab more feasible. It is proposed as a Maple package for rule-based programming, rewriting strategies and their combination with standard Maple code. We illustrate the practical interest of this language by using it to encode two examples of multiscale derivations, namely the two-scale limit of the derivative operator and the two-scale model of the stationary heat equation.
△ Less
Submitted 10 December, 2013; v1 submitted 17 January, 2011;
originally announced January 2011.
-
Graph Based Reduction of Program Verification Conditions
Authors:
Jean-François Couchot,
Alain Giorgetti,
Nicolas Stouls
Abstract:
Increasing the automaticity of proofs in deductive verification of C programs is a challenging task. When applied to industrial C programs known heuristics to generate simpler verification conditions are not efficient enough. This is mainly due to their size and a high number of irrelevant hypotheses. This work presents a strategy to reduce program verification conditions by selecting their rele…
▽ More
Increasing the automaticity of proofs in deductive verification of C programs is a challenging task. When applied to industrial C programs known heuristics to generate simpler verification conditions are not efficient enough. This is mainly due to their size and a high number of irrelevant hypotheses. This work presents a strategy to reduce program verification conditions by selecting their relevant hypotheses. The relevance of a hypothesis is determined by the combination of a syntactic analysis and two graph traversals. The first graph is labeled by constants and the second one by the predicates in the axioms. The approach is applied on a benchmark arising in industrial program verification.
△ Less
Submitted 8 July, 2009;
originally announced July 2009.