-
Algorithm for AGC index management against crowded radio environment
Authors:
Morgane Joly,
Fabian Rivière,
Éric Renault
Abstract:
This paper describes a receiver that uses an innovative method to predict, according to history of receiver operating metrics (packet lost/well received), the optimum automatic gain control (AGC) index or most appropriate variable gain range to be used for next packet reception, anticipating an interferer appearing during the payload reception. This allows the receiver to have higher immunity to i…
▽ More
This paper describes a receiver that uses an innovative method to predict, according to history of receiver operating metrics (packet lost/well received), the optimum automatic gain control (AGC) index or most appropriate variable gain range to be used for next packet reception, anticipating an interferer appearing during the payload reception. This allows the receiver to have higher immunity to interferers even if they occur during the gain frozen payload reception period whilst still ensuring an optimum sensitivity level. As a result, the method allows setting the receiver gain to get an optimum trade-off between reception sensitivity and random interferer immunity.
△ Less
Submitted 19 March, 2024;
originally announced April 2024.
-
Structural Reductions and Stutter Sensitive Properties
Authors:
Emmanuel Paviot-Adet,
Denis Poitrenaud,
Etienne Renault,
Yann Thierry-Mieg
Abstract:
Verification of properties expressed as $ω$-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a w…
▽ More
Verification of properties expressed as $ω$-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a \emph{reduction} of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. We also present an approach that can reason using a partition of a property language into its stutter insensitive, shortening insensitive, lengthening insensitive and length sensitive parts to still use structural reductions even when working with arbitrary properties. An implementation and experimental evidence is provided showing most non-random properties sensitive to stutter are actually shortening or lengthening insensitive.
△ Less
Submitted 26 February, 2024; v1 submitted 8 December, 2022;
originally announced December 2022.
-
From Spot 2.0 to Spot 2.10: What's New?
Authors:
Alexandre Duret-Lutz,
Etienne Renault,
Maximilien Colange,
Florian Renkin,
Alexandre Gbaguidi,
Philipp Schlehuber-Caissier,
Thomas Medioni,
Antoine Martin,
Jérôme Dubois,
Clément Gillard,
Henrich Lauko
Abstract:
Spot is a C ++ 17 library for LTL and $ω$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $ω$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several feature…
▽ More
Spot is a C ++ 17 library for LTL and $ω$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $ω$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more. We also shed some lights on the data-structure used to store automata.
△ Less
Submitted 20 June, 2022;
originally announced June 2022.
-
LTL under reductions with weaker conditions than stutter-invariance
Authors:
Emmanuel Paviot-Adet,
Denis Poitrenaud,
Etienne Renault,
Yann Thierry-Mieg
Abstract:
Verification of properties expressed as-regular languages such as LTL can benefit hugely from stutter-insensitivity, using a diverse set of reduction strategies. However properties that are not stutter-insensitive, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a wea…
▽ More
Verification of properties expressed as-regular languages such as LTL can benefit hugely from stutter-insensitivity, using a diverse set of reduction strategies. However properties that are not stutter-insensitive, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter-insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most nonrandom properties sensitive to stutter are actually shortening or lengthening insensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision procedure, the approach can still improve state of the art verification tools.
△ Less
Submitted 6 January, 2023; v1 submitted 5 November, 2021;
originally announced November 2021.
-
Information Centric Networking based Handover Support for QoS Maintenance in Cooperative Heterogeneous Wireless Networks
Authors:
Muhammad Shoaib Saleem,
Eric Renault,
Djamal Zeghlache
Abstract:
Network of Information (NetInf) is a term coined for networks which unlike contemporary network are not node centric. As the name indicates, information supersedes nodes in the network. In this report, we propose an architecture of mobile node for NetInf. We call it NetInf Mobile Node. It is an extension of the basic node architecture proposed for NetInf. It is compatible to NetInf and TCP/IP base…
▽ More
Network of Information (NetInf) is a term coined for networks which unlike contemporary network are not node centric. As the name indicates, information supersedes nodes in the network. In this report, we propose an architecture of mobile node for NetInf. We call it NetInf Mobile Node. It is an extension of the basic node architecture proposed for NetInf. It is compatible to NetInf and TCP/IP based networks. The Virtual Node Layer modules in the architecture provide support for managing mobility, power consumption of the node as well data relaying/storing services. In- ner/Outer Locator Construction Routers (I/O LCTR) are two functions introduced in NetInf mobile nodes to operate between NetInf and non- NetInf sites. The basic purpose of NetInf mobile node is to maintain the QoS during mobility events. The handoff/handover are critical situations during mobility where chances of QoS degradation of an ongoing session are high. This report presents one such scenario in which QoS of an appli- cation is maintained during a handoff situations in heterogeneous wireless network environment through our proposed algorithm.
△ Less
Submitted 16 August, 2011;
originally announced August 2011.
-
NetInf Mobile Node Architecture and Mobility Management based on LISP Mobile Node
Authors:
Muhammad Shoaib Saleem,
Éric Renault,
Djamal Zeghlache
Abstract:
In this paper, we propose an architecture for Network of Information mobile node (NetInf MN). It bears characteristics and features of basic NetInf node architecture with features introduced in the LISP MN architecture. We also introduce a virtual node layer for mobility management in the Network of Information. Therefore, by adopting this architecture no major changes in the contemporary network…
▽ More
In this paper, we propose an architecture for Network of Information mobile node (NetInf MN). It bears characteristics and features of basic NetInf node architecture with features introduced in the LISP MN architecture. We also introduce a virtual node layer for mobility management in the Network of Information. Therefore, by adopting this architecture no major changes in the contemporary network topologies is required. Thus, making our approach more practical.
△ Less
Submitted 16 August, 2011; v1 submitted 30 September, 2010;
originally announced September 2010.
-
Hierarchical Location Service with Prediction in Mobile Ad-Hoc Networks
Authors:
Ebtisam Amar,
Selma Boumerdassi,
Éric Renault
Abstract:
Position-based routing protocols take advantage of location information to perform a stateless and efficient routing. To enable position-based routing, a node must be able to discover the location of the messages' destination node. This task is typically accomplished by a location service. Recently, several location service protocols have been developed for ad hoc networks. In this paper we propos…
▽ More
Position-based routing protocols take advantage of location information to perform a stateless and efficient routing. To enable position-based routing, a node must be able to discover the location of the messages' destination node. This task is typically accomplished by a location service. Recently, several location service protocols have been developed for ad hoc networks. In this paper we propose a novel location service called PHLS: Predictive Hierarchical Location Service. In PHLS, the entire network is partitioned into a hierarchy of smaller and smaller regions. For each node, one node in each-level region of the hierarchy is chosen as its local location server. When the network initializes or when a node attaches the network, nodes contact their local location server with their current location information (ie. position and velocity). Then, they only need to update their location server when they move away from their current region. Finally, nodes query their location servers and get the exact or predicted location of destination nodes.
△ Less
Submitted 16 March, 2010;
originally announced March 2010.
