Author: "Japanese French Laboratory for Informatics (JFLI)" - Searchworks@Jio Institute Digital Library Search Results

Your search keyword '"Japanese French Laboratory for Informatics (JFLI)"' showing total 111 results

Start Over Author "Japanese French Laboratory for Informatics (JFLI)"

111 results on '"Japanese French Laboratory for Informatics (JFLI)"'

1. Efficient Energy-Compensated VPLs using Photon Splatting

Author: Jamorn Sriwasansak, Adrien Gruson, Toshiya Hachisuka, The University of Tokyo (UTokyo), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-Université Pierre et Marie Curie - Paris 6 (UPMC)-The University of Tokyo (UTokyo)-Centre National de la Recherche Scientifique (CNRS), The University of Tokyo, Japanese French Laboratory for Informatics ( JFLI ), and National Institute of Informatics ( NII ) -Université Pierre et Marie Curie - Paris 6 ( UPMC ) -Keio University-The University of Tokyo-Centre National de la Recherche Scientifique ( CNRS )
Subjects: Many lights, Density Estimation, Computer science, Global illumination, Process (computing), ComputingMethodologies_IMAGEPROCESSINGANDCOMPUTERVISION, 020207 software engineering, 02 engineering and technology, [ INFO.INFO-GR ] Computer Science [cs]/Graphics [cs.GR], Computer Graphics and Computer-Aided Design, [INFO.INFO-GR]Computer Science [cs]/Graphics [cs.GR], Computer Science Applications, Rendering (computer graphics), Computational science, Computer graphics, Path (graph theory), 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Point (geometry), Importance sampling, Efficient energy use, ComputingMethodologies_COMPUTERGRAPHICS
Abstract: International audience; Efficient light transport simulation is important for many applications in computer graphics. Many-light methods based on virtual point lights (VPLs) especially work well for scenes consist mainly of diffuse materials. Rendered images with VPLs, however, are known to suffer from energy loss due to clamping of the VPL contributions. Removing this clamping, unfortunately, introduces significant variance in images due to the singularities of VPLs. We propose an efficient and practical algorithm which compensates energy loss of VPLs using yet another efficient rendering method – photon splatting. Recent unified path sampling frameworks show that VPLs are in fact photons. Based on this unified formulation, we propose to reuse VPLs as photons to compensate missing energy of clamped VPLs. This combination is very natural: the singularities of VPLs happen if a shading point is too close to VPLs, but such VPLs can also be seen as neighboring photons that are indeed useful for photon density estimation. We formulate this energy compensation process using multiple importance sampling to combine rendering with VPLs and photon splatting optimally. Our algorithm can be efficiently implemented on GPUs since rendering with VPLs and photon splatting are both suitable for GPUs. The results demonstrate that our method produces more accurate images in the same rendering time than the existing methods. For common use cases of rendering mostly diffuse scenes, our work leads to an efficient, accurate, and practical rendering algorithm based on VPLs.
Published: 2018
Full Text: View/download PDF

2. Optimality and Approximation Ratios of Demodulator Allocation Strategies in LoRa Multi-Gateway Networks

Author: Guitton, Alexandre, Kaneko, Megumi, Rachkidy, Nancy, Université Clermont Auvergne (UCA), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne (UCA)-Institut national polytechnique Clermont Auvergne (INP Clermont Auvergne), Université Clermont Auvergne (UCA)-Université Clermont Auvergne (UCA), AlGorithmes et Optimisation pour Réseaux Autonomes (AGORA), CITI Centre of Innovation in Telecommunications and Integration of services (CITI), Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], demodulator allocation, multi-gateway, LoRa, Internet of Things (IoT), LoRaWAN
Abstract: Long Range (LoRa) is a wireless modulation used to provide longrange connectivity to low-power devices of the Internet of Things (IoT). LoRa gateways use hardware chips called demodulators in order to demodulate concurrent frames on different channels or spreading factors. In this paper, we establish several theoretical results on the performance of fundamental demodulator allocating strategies. In the single gateway scenario, we first prove the optimality of the basic preemptive allocation strategy. Next, in the multi-gateway scenario, the greedy non-collaborative strategy, which is currently implemented in LoRa gateways, is shown to achieve a very large approximation ratio. As an alternative, we demonstrate that a preemptive non-collaborative strategy has an approximation ratio of 2, and furthermore, that a preemptive smartcollaborative strategy reaches an approximation ratio of 3/2, for two gateways. These seminal results imply that the current performance of multi-gateway LoRa deployments can be largely improved by the proposed collaborative demodulator allocation strategies.
Published: 2023

3. An Auction-based Assignment Method for LoRa Multi-Gateway Networks

Author: Chen, Jen-Tse, Kaneko, Megumi, Guitton, Alexandre, National Tsing Hua University [Hsinchu] (NTHU), National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), AlGorithmes et Optimisation pour Réseaux Autonomes (AGORA), CITI Centre of Innovation in Telecommunications and Integration of services (CITI), Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), Université Clermont Auvergne (UCA), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne (UCA)-Institut national polytechnique Clermont Auvergne (INP Clermont Auvergne), Université Clermont Auvergne (UCA)-Université Clermont Auvergne (UCA), and IEEE
Subjects: Optimization, LoRa Multi-gateway Optimization Auction, [INFO]Computer Science [cs], Multi-gateway, LoRa, Auction
Abstract: International audience; Long Range (LoRa) technology constitutes one of the major enablers of future Internet-of-Things (IoT) applications, such as monitoring of challenged environments and smart buildings. However, crucial issues in the context of multi-gateway LoRa networks have been overlooked. In particular, most existing methods did not consider the stringent constraint of limited number of demodulators at each gateway. Therefore, we devise a gateway selection method for uplink LoRa transmissions, where this limited availability of demodulators is fully considered. We propose an optimization approach based on the auction mechanism, where each IoT device is pre-assigned to a unique gateway, so as to maximize the total amount of demodulated transmissions without redundancy at the network server. Furthermore, a low complexity method is also designed, where devices are partitioned into groups and where auctions are parallelized. Numerical results show that the proposed methods largely outperform benchmark algorithms in terms of the network utility function and sum-rate, while approaching the upper bound performance. The proposed methods are particularly suited to cope with the inherent dynamics of mobile LoRa IoT networks, as highest gains are attained for demodulation latencies in the order of tens to hundreds of milliseconds.
Published: 2023

4. Outcome determinism in measurement-based quantum computation with qudits

Author: Robert I Booth, Aleks Kissinger, Damian Markham, Clément Meignant, Simon Perdrix, Designing the Future of Computational Models (MOCQUA), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratory for the Foundations of Computer Science [Edinburgh] (LFCS), University of Edinburgh, Department of Computer Science [Oxford], University of Oxford, Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), and University of Oxford [Oxford]
Subjects: Statistics and Probability, Quantum Physics, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Modeling and Simulation, FOS: Physical sciences, General Physics and Astronomy, Statistical and Nonlinear Physics, Quantum Physics (quant-ph), Mathematical Physics
Abstract: In measurement-based quantum computing (MBQC), computation is carried out by a sequence of measurements and corrections on an entangled state. Flow, and related concepts, are powerful techniques for characterising the dependence of the corrections on previous measurement outcomes. We introduce flow-based methods for MBQC with qudit graph states, which we call Zd-flow, when the local dimension is an odd prime. Our main results are proofs that Zd-flow is a necessary and sufficient condition for a strong form of outcome determinism. Along the way, we find a suitable generalisation of the concept of measurement planes to this setting and characterise the allowed measurements in a qudit MBQC. We also provide a polynomial-time algorithm for finding an optimal Zd-flow whenever one exists., Comment: 16 pages + 10 pages of appendices, 1 figure
Published: 2023
Full Text: View/download PDF

5. A coalgebraic view on reachability

Author: Shin-ya Katsumata, Stefan Milius, Thorsten Wißmann, Jérémy Dubut, Friedrich-Alexander Universität Erlangen-Nürnberg (FAU), National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Functor, Computer science, General Mathematics, Coalgebra, Mathematics::Rings and Algebras, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Mathematics - Category Theory, State (functional analysis), Base (topology), Kleisli category, Algebra, Range (mathematics), Mathematics::K-Theory and Homology, Reachability, Mathematics::Quantum Algebra, Computer Science::Logic in Computer Science, Mathematics::Category Theory, FOS: Mathematics, Graph (abstract data type), Category Theory (math.CT), ComputingMilieux_MISCELLANEOUS, [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT]
Abstract: Coalgebras for an endofunctor provide a category-theoretic framework for modeling a wide range of state-based systems of various types. We provide an iterative construction of the reachable part of a given pointed coalgebra that is inspired by and resembles the standard breadth-first search procedure to compute the reachable part of a graph. We also study coalgebras in Kleisli categories: for a functor extending a functor on the base category, we show that the reachable part of a given pointed coalgebra can be computed in that base category.
Published: 2020
Full Text: View/download PDF

6. Cryptographic approach to quantum metrology

Author: Shettell, Nathan, Kashefi, Elham, Markham, Damian, Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), and University of Edinburgh
Subjects: Quantum Physics, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], 0103 physical sciences, FOS: Physical sciences, 010306 general physics, Quantum Physics (quant-ph), 01 natural sciences, 010305 fluids & plasmas, Computer Science::Cryptography and Security
Abstract: We consider a cryptographically motivated framework for quantum metrology in the presence of a malicious adversary. We begin by devising an estimation strategy for a (potentially) altered resource (due to a malicious adversary) and quantify the amount of bias and the loss in precision as a function of the introduced uncertainty in the resource. By incorporating an appropriate cryptographic protocol, the uncertainty in the resource can be bounded with respect to the soundness of the cryptographic protocol. Thus the effectiveness of the quantum metrology problem can be directly related to the effectiveness of the cryptography protocol. As an example, we consider a quantum metrology problem in which resources are exchanged through an unsecured quantum channel. We then construct two protocols for this task which offer a trade-off between difficulty of implementation and efficiency., Comment: 3 figures, appendix
Published: 2022
Full Text: View/download PDF

7. Classical-quantum network coding: a story about tensor

Author: Meignant, Clément, Grosshans, Frédéric, Markham, Damian, Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: 81P45 (Primary) 94A15 (Secondary), Quantum Physics, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Computer Science - Information Theory
Abstract: We study here the conditions to perform the distribution of a pure state on a quantum network using quantum operations which can succeed with a non-zero probability, the Stochastic Local Operation and Classical Communication (SLOCC) operations. In their pioneering 2010 work, Kobayashi et al. showed how to convert any classical network coding protocol into a quantum network coding protocol. However, they left open whether the existence of a quantum network coding protocol implied the existence of a classical one. Motivated by this question, we characterize the set of distribution tasks achievable with non zero probability for both classical and quantum networks. We develop a formalism which encompasses both types of distribution protocols by reducing the solving of a distribution task to the factorization of a tensor with complex coefficients or real positive ones. Using this formalism, we examine the equivalences and differences between both types of distribution protocols exhibiting several elementary and fundamental relations between them as well as concrete examples of both convergence and divergence. We answer by the negative to the issue previously left open: some tasks are achievable in the quantum setting, but not in the classical one. We believe this formalism to be a useful tool for studying the extent of quantum network ability to perform multipartite distribution tasks., Comment: 11 pages, 6 figures
Published: 2021

8. Encoding constraint satisfaction problems as QUBO(abstract)

Author: Codognet, Philippe, Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: [INFO]Computer Science [cs], ComputingMilieux_MISCELLANEOUS
Abstract: International audience
Published: 2021

9. Learning Interpretable Error Functions for Combinatorial Optimization Problem Modeling

Author: Richoux, Florian, Baffier, Jean-François, Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), National Institute of Advanced Industrial Science and Technology (AIST), and The University of Tokyo (UTokyo)
Subjects: FOS: Computer and information sciences, Artificial Intelligence (cs.AI), Computer Science - Artificial Intelligence, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
Abstract: International audience; In Constraint Programming, constraints are usually represented as predicates allowing or forbidding combinations of values. However, some algorithms exploit a finer representation: error functions. Their usage comes with a price though: it makes problem modeling significantly harder. Here, we propose a method to automatically learn an error function corresponding to a constraint, given a function deciding if assignments are valid or not. This is, to the best of our knowledge, the first attempt to automatically learn error functions for hard constraints. Our method uses a variant of neural networks we named Interpretable Compositional Networks, allowing us to get interpretable results, unlike regular artificial neural networks. Experiments on 5 different constraints show that our system can learn functions that scale to high dimensions, and can learn fairly good functions over incomplete spaces.
Published: 2021

10. Interpretable Utility-based Models Applied to the FightingICE Platform

Author: Chen, Tianyu, Richoux, Florian, Torres, Javier, Inoue, Katsumi, Richoux, Florian, The Graduate University for Advanced Studies, japan (SOKENDAI), National Institute of Advanced Industrial Science and Technology (AIST), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Chercheur indépendant, and National Institute of Informatics (NII)
Subjects: Machine Learning, [INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI], ComputingMilieux_PERSONALCOMPUTING, Interpretable Results, Fighting Games, Utility-based AI, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
Abstract: International audience; One task of game designers is to give NPCs fun behaviors, where "fun" can have many different manifestations. Several classic methods exist in Game AI to model NPCs' behaviors; one of them is utilitybased AI. Utility functions constitute a powerful tool to define behaviors but can be tedious and timeconsuming to make and tune correctly until the desired behavior is achieved. Here, we propose a method to learn utility functions from data collected after some human-played games, to recreate a target behavior. Utility functions are modeled using Interpretable Compositional Networks, allowing us to get interpretable results, unlike regular neural networks. We show our method can handle noisy data and learn utility functions able to credibly reproduce different target behaviors, with a median accuracy from 64.5% to 83.7%, using the FightingICE platform, an environment for AI agent competitions. We believe our method can be useful to game designers to quickly prototype NPCs' behaviors, and even to define their final utility functions.
Published: 2021
Full Text: View/download PDF

11. Constraint Solving by Quantum Annealing

Author: Philippe Codognet, Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), and Codognet, Philippe
Subjects: Quadratic assignment problem, Computer science, Quantum annealing, MathematicsofComputing_NUMERICALANALYSIS, 0102 computer and information sciences, [INFO] Computer Science [cs], 01 natural sciences, Constraint (information theory), 010201 computation theory & mathematics, 0103 physical sciences, Combinatorial optimization, Quadratic unconstrained binary optimization, [INFO]Computer Science [cs], 010306 general physics, Algorithm, Constraint satisfaction problem, ComputingMilieux_MISCELLANEOUS, Costas array, Quantum computer
Abstract: We present experiments in solving combinatorial optimization and constraint satisfaction problems by means of Quantum Annealing. We describe how to model classic constraint problems such as N-queens and Magic Square as well as hard combinatorial problems such as the Costas Array Problem or the Quadratic Assignment Problem in terms of QUBO (Quadratic Unconstrained Binary Optimization). QUBO is the input language of quantum computers based on quantum annealing such as the D-Wave systems and of the ”quantum-inspired” but classical devices such as Fujitsu’s Digital Annealing Unit or Hitachi’s CMOS Annealing Machine. We present preliminary results for solving these combinatorial optimization and constraint satisfaction problems by implementation on the D-Wave quantum computer.
Published: 2021

12. Quantum machine learning with adaptive linear optics

Author: Adel Sohbi, Ulysse Chabaud, Damian Markham, California Institute of Technology (CALTECH), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), and Korea Institute for Advanced Study (KIAS)
Subjects: FOS: Computer and information sciences, Computer Science - Machine Learning, Photon, Physics and Astronomy (miscellaneous), Quantum machine learning, Computer science, QC1-999, Subroutine, FOS: Physical sciences, 01 natural sciences, Machine Learning (cs.LG), 010305 fluids & plasmas, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], [INFO.INFO-LG]Computer Science [cs]/Machine Learning [cs.LG], Quantum state, 0103 physical sciences, 010306 general physics, Quantum, Boson, Quantum Physics, Physics, Atomic and Molecular Physics, and Optics, Kernel (statistics), Quantum algorithm, Quantum Physics (quant-ph), Algorithm
Abstract: We study supervised learning algorithms in which a quantum device is used to perform a computational subroutine - either for prediction via probability estimation, or to compute a kernel via estimation of quantum states overlap. We design implementations of these quantum subroutines using Boson Sampling architectures in linear optics, supplemented by adaptive measurements. We then challenge these quantum algorithms by deriving classical simulation algorithms for the tasks of output probability estimation and overlap estimation. We obtain different classical simulability regimes for these two computational tasks in terms of the number of adaptive measurements and input photons. In both cases, our results set explicit limits to the range of parameters for which a quantum advantage can be envisaged with adaptive linear optics compared to classical machine learning algorithms: we show that the number of input photons and the number of adaptive measurements cannot be simultaneously small compared to the number of modes. Interestingly, our analysis leaves open the possibility of a near-term quantum advantage with a single adaptive measurement., 16 + 5 pages, presented at AQIS2020, accepted in Quantum
Published: 2021
Full Text: View/download PDF

13. Certifying dimension of quantum systems by sequential projective measurements

Author: Adel Sohbi, Jaewan Kim, Damian Markham, Marco Túlio Quintino, Korea Institute for Advanced Study (KIAS), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), University of Vienna [Vienna], Institute for Quantum Optics and Quantum Information [Innsbruck] (IQOQI), and Austrian Academy of Sciences (OeAW)
Subjects: High probability, Quantum Physics, Physics and Astronomy (miscellaneous), Computer science, Numerical analysis, Physics, QC1-999, FOS: Physical sciences, Computer Science::Digital Libraries, 01 natural sciences, Atomic and Molecular Physics, and Optics, 010305 fluids & plasmas, Dimension (vector space), Robustness (computer science), 0103 physical sciences, Computer Science::Mathematical Software, Qutrit, Projective test, [MATH]Mathematics [math], 010306 general physics, Quantum Physics (quant-ph), Algorithm, Quantum
Abstract: This work analyzes correlations arising from quantum systems subject to sequential projective measurements to certify that the system in question has a quantum dimension greater than somed. We refine previous known methods and show that dimension greater than two can be certified in scenarios which are considerably simpler than the ones presented before and, for the first time in this sequential projective scenario, we certify quantum systems with dimension strictly greater than three. We also perform a systematic numerical analysis in terms of robustness and conclude that performing random projective measurements on random pure qutrit states allows a robust certification of quantum dimensions with very high probability.
Published: 2021
Full Text: View/download PDF

14. Certification of Non-Gaussian States with Operational Measurements

Author: Ganaël Roeland, Mattia Walschaers, Ulysse Chabaud, Valentina Parigi, Damian Markham, Nicolas Treps, Frédéric Grosshans, Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Kastler Brossel (LKB (Jussieu)), Fédération de recherche du Département de physique de l'Ecole Normale Supérieure - ENS Paris (FRDPENS), Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Quantum Physics, Rank (linear algebra), Gaussian, General Engineering, FOS: Physical sciences, Negativity effect, Certification, 01 natural sciences, 010305 fluids & plasmas, symbols.namesake, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Homodyne detection, 0103 physical sciences, symbols, General Earth and Planetary Sciences, Statistical physics, Quantum Physics (quant-ph), 010306 general physics, General Environmental Science, Mathematics
Abstract: We derive a theoretical framework for the experimental certification of non-Gaussian features of quantum states using double homodyne detection. We rank experimental non-Gaussian states according to the recently defined stellar hierarchy and we propose practical Wigner negativity witnesses. We simulate various use-cases ranging from fidelity estimation to witnessing Wigner negativity. Moreover, we extend results on the robustness of the stellar hierarchy of non-Gaussian states. Our results illustrate the usefulness of double homodyne detection as a practical measurement scheme for retrieving information about continuous variable quantum states., 9+9 pages, comments welcome
Published: 2021
Full Text: View/download PDF

15. Practical Limits of Error Correction for Quantum Metrology

Author: Kae Nemoto, William J. Munro, Damian Markham, Nathan Shettell, Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), NTT Basic Research Laboratories [Tokio], NTT Basic Research Laboratories, Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), and National Institute of Informatics (NII)
Subjects: Physics, Quantum Physics, General Physics and Astronomy, FOS: Physical sciences, 01 natural sciences, Noise (electronics), 010305 fluids & plasmas, Quantum technology, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Quantum error correction, Obstacle, 0103 physical sciences, Electronic engineering, Quantum metrology, Heisenberg limit, Sensitivity (control systems), 010306 general physics, Error detection and correction, Quantum Physics (quant-ph)
Abstract: Noise is the greatest obstacle in quantum metrology that limits it achievable precision and sensitivity. There are many techniques to mitigate the effect of noise, but this can never be done completely. One commonly proposed technique is to repeatedly apply quantum error correction. Unfortunately, the required repetition frequency needed to recover the Heisenberg limit is unachievable with the existing quantum technologies. In this article we explore the discrete application of quantum error correction with current technological limitations in mind. We establish that quantum error correction can be beneficial and highlight the factors which need to be improved so one can reliably reach the Heisenberg limit level precision., Comment: 22 pages, 4 Figures, Appendix
Published: 2021
Full Text: View/download PDF

16. Flow conditions for continuous variable measurement-based quantum computing

Author: Booth, Robert, Markham, Damian, Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Designing the Future of Computational Models (MOCQUA), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Quantum Physics, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], FOS: Physical sciences, Quantum Physics (quant-ph)
Abstract: In measurement-based quantum computing (MBQC), computation is carried out by a sequence of measurements and corrections on an entangled state. Flow, and related concepts, are powerful techniques for characterising the dependence of the corrections on previous measurement results. We introduce flow-based methods for quantum computation with continuous-variable graph states, which we call CV-flow. These are inspired by, but not equivalent to, the notions of causal flow and g-flow for qubit MBQC. We also show that an MBQC with CV-flow approximates a unitary arbitrarily well in the infinite-squeezing limit, addressing issues of convergence which are unavoidable in the infinite-dimensional setting. In developing our proofs, we provide a method for converting a CV-MBQC computation into a circuit form, analogous to the circuit extraction method of Miyazaki et al, and an efficient algorithm for finding CV-flow when it exists based on the qubit version by Mhalla and Perdrix. Our results and techniques naturally extend to the cases of MBQC for quantum computation with qudits of prime local dimension., 31 pages + 10 pages of appendices, 5 figures; accepted to Quantum
Published: 2021

17. A model of anytime algorithm performance for bi-objective optimization

Author: Luís Paquete, Alexandre D. Jesus, Arnaud Liefooghe, Centre for Informatics and Systems (CISUC), Departamento de Engenharia Informática / Department of Informatics Engineering (DEI), University of Coimbra [Portugal] (UC)-Universidade de Coimbra [Coimbra]-University of Coimbra [Portugal] (UC)-Universidade de Coimbra [Coimbra], Optimisation de grande taille et calcul large échelle (BONUS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), and This work was partially supported by COST Action CA15140 (STSM n. 39531), and by the PICS project MOCO-SEARCH cofunded by the French National Center for Scientific Research (CNRS) and the Portuguese Foundation for Science and Technology (FCT). The first author acknowledges the FCT for Ph.D. studentship SFRH/BD/132275/2017, co-funded by the European Social Fund and by the State Budget of the Portuguese Ministry of Education and Science. This work was partially funded by national funds through the FCT - Foundation for Science and Technology, I.P. within the scope of the project CISUC - UID/CEC/00326/2020 and by the European Social Fund, through the Regional Operational Program Centro 2020.
Subjects: Anytime algorithms, Mathematical optimization, 021103 operations research, Control and Optimization, Combinatorial optimization, Bi objective optimization, Applied Mathematics, media_common.quotation_subject, 0211 other engineering and technologies, ε-constraint, 02 engineering and technology, Management Science and Operations Research, Multi-objective optimization, Computer Science Applications, Anytime behavior, Set (abstract data type), Constraint algorithm, Anytime algorithm, Superellipse, Quality (business), [INFO]Computer Science [cs], media_common, Mathematics
Abstract: Anytime algorithms allow a practitioner to trade-off runtime for solution quality. This is of particular interest in multi-objective combinatorial optimization since it can be infeasible to identify all efficient solutions in a reasonable amount of time. We present a theoretical model that, under some mild assumptions, characterizes the “optimal” trade-off between runtime and solution quality, measured in terms of relative hypervolume, of anytime algorithms for bi-objective optimization. In particular, we assume that efficient solutions are collected sequentially such that the collected solution at each iteration maximizes the hypervolume indicator, and that the non-dominated set can be well approximated by a quadrant of a superellipse. We validate our model against an “optimal” model that has complete knowledge of the non-dominated set. The empirical results suggest that our theoretical model approximates the behavior of this optimal model quite well. We also analyze the anytime behavior of an $$\varepsilon $$ -constraint algorithm, and show that our model can be used to guide the algorithm and improve its anytime behavior.
Published: 2021
Full Text: View/download PDF

18. Simulating complex quantum networks with time crystals

Author: Kaoru Sanaka, Benjamin Renoust, William J. Munro, Tomo Osada, Marta P. Estarellas, Kae Nemoto, Victor M. Bastidas, National Institute of Informatics (NII), Tokyo University of Science [Tokyo], NTT Basic Research Laboratories [Tokio], NTT Basic Research Laboratories, Institute for Datability Science, Osaka University [Osaka], Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Quantum network, Quantum Physics, Multidisciplinary, Computer science, Physics, Quantum simulator, FOS: Physical sciences, SciAdv r-articles, Graph theory, Disordered Systems and Neural Networks (cond-mat.dis-nn), Condensed Matter - Disordered Systems and Neural Networks, Preferential attachment, 01 natural sciences, [INFO.INFO-SI]Computer Science [cs]/Social and Information Networks [cs.SI], 010305 fluids & plasmas, Minimal model, Discrete time and continuous time, 0103 physical sciences, Quantum system, Statistical physics, 010306 general physics, Translational symmetry, Quantum Physics (quant-ph), Research Articles, Research Article
Abstract: Crystals arise as the result of the breaking of a spatial translation symmetry. Similarly, translation symmetries can also be broken in time so that discrete time crystals appear. Here, we introduce a method to describe, characterize, and explore the physical phenomena related to this phase of matter using tools from graph theory. The analysis of the graphs allows to visualizing time-crystalline order and to analyze features of the quantum system. For example, we explore in detail the melting process of a minimal model of a period-2 discrete time crystal and describe it in terms of the evolution of the associated graph structure. We show that during the melting process, the network evolution exhibits an emergent preferential attachment mechanism, directly associated with the existence of scale-free networks. Thus, our strategy allows us to propose a previously unexplored far-reaching application of time crystals as a quantum simulator of complex quantum networks., Comment: 17 pages, 8 figures
Published: 2020
Full Text: View/download PDF

19. Dominance, indicator and decomposition based search for multi-objective QAP: landscape analysis and automated algorithm selection

Author: Sébastien Verel, Bilel Derbel, Kiyoshi Tanaka, Arnaud Liefooghe, Hernán Aguirre, Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Optimisation de grande taille et calcul large échelle (BONUS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique Signal et Image de la Côte d'Opale (LISIC), Université du Littoral Côte d'Opale (ULCO), Faculty of Engineering [Nagano], Shinshu University [Nagano], This research was conducted in the scope of the French/Japanese MODŌ international lab, and was partially supported by the French national research agency under Project ANR-16-CE23-0013-01., Bäck, Thomas, and ANR-16-CE23-0013,BigMO,Optimisation Multiobjectif Big(2016)
Subjects: 050101 languages & linguistics, Computer science, 05 social sciences, Evolutionary algorithm, Sample (statistics), [INFO.INFO-RO]Computer Science [cs]/Operations Research [cs.RO], 02 engineering and technology, Recommender system, computer.software_genre, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Quadratic equation, Search algorithm, 0202 electrical engineering, electronic engineering, information engineering, Decomposition (computer science), Feature (machine learning), 020201 artificial intelligence & image processing, 0501 psychology and cognitive sciences, Data mining, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], computer, Selection (genetic algorithm)
Abstract: International audience; We investigate the properties of large-scale multi-objective quadratic assignment problems (mQAP) and how they impact the performance of multi-objective evolutionary algorithms. The landscape of a diversified dataset of bi-, multi-, and many-objective mQAP instances is characterized by means of previously-identified features. These features measure complementary facets of problem difficulty based on a sample of solutions collected along random and adaptive walks over the landscape. The strengths and weaknesses of a dominance-based, an indicator-based, and a decomposition-based search algorithm are then highlighted by relating their expected approximation quality in view of landscape features. We also discriminate between algorithms by revealing the most suitable one for subsets of instances. At last, we investigate the performance of a feature-based automated algorithm selection approach. By relying on low- cost features, we show that our recommendation system performs best in more than of the considered mQAP instances.
Published: 2020
Full Text: View/download PDF

20. An ensemble indicator-based density estimator for evolutionary multi-objective optimization

Author: Carlos A. Coello Coello, Arnaud Liefooghe, Jesús Guillermo Falcón-Cardona, Centro de Investigacion y de Estudios Avanzados del Instituto Politécnico Nacional (CINVESTAV), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Optimisation de grande taille et calcul large échelle (BONUS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), and Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)
Subjects: 050101 languages & linguistics, Optimization problem, 05 social sciences, Evolutionary algorithm, Process (computing), Estimator, 02 engineering and technology, [INFO.INFO-RO]Computer Science [cs]/Operations Research [cs.RO], Ensemble learning, Multi-objective optimization, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, 0501 psychology and cognitive sciences, AdaBoost, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Algorithm, Mathematics
Abstract: Ensemble learning is one of the most employed methods in machine learning. Its main ground is the construction of stronger mechanisms based on the combination of elementary ones. In this paper, we employ AdaBoost, which is one of the most well-known ensemble methods, to generate an ensemble indicator-based density estimator for multi-objective optimization. It combines the search properties of five density estimators, based on the hypervolume, R2, IGD$^+$, $\epsilon ^+$, and $\varDelta _p$ quality indicators. Through the multi-objective evolutionary search process, the proposed ensemble mechanism adapts itself using a learning process that takes the preferences of the underlying quality indicators into account. The proposed method gives rise to the ensemble indicator-based multi-objective evolutionary algorithm (EIB-MOEA) that shows a robust performance on different multi-objective optimization problems when compared with respect to several existing indicator-based multi-objective evolutionary algorithms.
Published: 2020
Full Text: View/download PDF

21. Designing parallelism in surrogate-assisted multiobjective optimization based on decomposition

Author: Hernán Aguirre, Nicolas Berveglieri, Kiyoshi Tanaka, Arnaud Liefooghe, Qingfu Zhang, Bilel Derbel, Optimisation de grande taille et calcul large échelle (BONUS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Shinshu University [Nagano], City University of Hong Kong [Hong Kong] (CUHK), This work was supported by the French national research agency (ANR-16-CE23-0013-01) and the Research Grants Council of Hong Kong (RGC Project No. A-CityU101/16)., and ANR-16-CE23-0013,BigMO,Optimisation Multiobjectif Big(2016)
Subjects: Optimization problem, Computer science, Supervised learning, Evolutionary algorithm, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Multi-objective optimization, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Computer engineering, 010201 computation theory & mathematics, Scalability, 0202 electrical engineering, electronic engineering, information engineering, Parallelism (grammar), Decomposition (computer science), 020201 artificial intelligence & image processing
Abstract: International audience; On the one hand, surrogate-assisted evolutionary algorithms are established as a method of choice for expensive black-box optimization problems. On the other hand, the growth in computing facilities has seen a massive increase in potential computational power, granted the users accommodate their approaches with the offered parallelism. While a number of studies acknowledge the impact of parallelism for single-objective expensive optimization assisted by surrogates, extending such techniques to the multi-objective setting has not yet been properly investigated, especially within the state-of-the-art decomposition framework. We first highlight the different degrees of parallelism in existing surrogate-assisted multi-objective evolutionary algorithms based on decomposition (S-MOEA/D). We then provide a comprehensive analysis of the key steps towards a successful parallel S-MOEA/D approach. Through an extensive benchmarking effort relying on the well-established bbob-biobj test functions, we analyze the performance of the different algorithm designs with respect to the problem dimensionality and difficulty, the amount of parallel cores available, and the supervised learning models considered. In particular, we show the difference in algorithm scalability based on the selected surrogate-assisted approaches, the performance impact of distributing the model training task and the efficacy of the designed parallel-surrogate methods.
Published: 2020
Full Text: View/download PDF

22. Algorithm selection of anytime algorithms

Author: Luís Paquete, Alexandre D. Jesus, Bilel Derbel, Arnaud Liefooghe, Optimisation de grande taille et calcul large échelle (BONUS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Centre for Informatics and Systems (CISUC), Departamento de Engenharia Informática / Department of Informatics Engineering (DEI), University of Coimbra [Portugal] (UC)-Universidade de Coimbra [Coimbra]-University of Coimbra [Portugal] (UC)-Universidade de Coimbra [Coimbra], Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Optimization problem, Computer science, Heuristic (computer science), media_common.quotation_subject, Algorithm Selection, Context (language use), 0102 computer and information sciences, 02 engineering and technology, Function (mathematics), 01 natural sciences, Measure (mathematics), Anytime Algorithms, 010201 computation theory & mathematics, Knapsack problem, Anytime Performance, Anytime algorithm, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Quality (business), [INFO]Computer Science [cs], Algorithm, Selection (genetic algorithm), media_common
Abstract: International audience; Anytime algorithms for optimization problems are of particular interest since they allow to trade off execution time with result quality. However, the selection of the best anytime algorithm for a given problem instance has been focused on a particular budget for execution time or particular target result quality. Moreover, it is often assumed that these anytime preferences are known when developing or training the algorithm selection methodology. In this work, we study the algorithm selection problem in a context where the decision maker's anytime preferences are defined by a general utility function, and only known at the time of selection. To this end, we first examine how to measure the performance of an anytime algorithm with respect to this utility function. Then, we discuss approaches for the development of selection methodologies that receive a utility function as an argument at the time of selection. Then, to illustrate one of the discussed approaches, we present a preliminary study on the selection between an exact and a heuristic algorithm for a bi-objective knapsack problem. The results show that the proposed methodology has an accuracy greater than 96% in the selected scenarios, but we identify room for improvement.
Published: 2020
Full Text: View/download PDF

23. Surrogate-assisted Multi-objective Combinatorial Optimization based on Decomposition and Walsh Basis

Author: Arnaud Liefooghe, Sébastien Verel, Geoffrey Pruvost, Bilel Derbel, Qingfu Zhang, Optimisation de grande taille et calcul large échelle (BONUS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique Signal et Image de la Côte d'Opale (LISIC), Université du Littoral Côte d'Opale (ULCO), City University of Hong Kong [Hong Kong] (CUHK), and ANR-16-CE23-0013,BigMO,Optimisation Multiobjectif Big(2016)
Subjects: Mathematical optimization, Computer science, Offspring, MathematicsofComputing_NUMERICALANALYSIS, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, Combinatorial optimization, Leverage (statistics), 020201 artificial intelligence & image processing, [INFO]Computer Science [cs]
Abstract: International audience; We consider the design and analysis of surrogate-assisted algorithms for expensive multi-objective combinatorial optimization. Focusing on pseudo-boolean functions, we leverage existing techniques based on Walsh basis to operate under the decomposition framework of MOEA/D. We investigate two design components for the cheap generation of a promising pool of offspring and the actual selection of one solution for expensive evaluation. We propose different variants, ranging from a filtering approach that selects the most promising solution at each iteration by using the constructed Walsh surrogates to discriminate between a pool of offspring generated by variation, to a substitution approach that selects a solution to evaluate by optimizing the Walsh surrogates in a multi-objective manner. Considering bi-objective NK landscapes as benchmark problems offering different degree of non-linearity, we conduct a comprehensive empirical analysis including the properties of the achievable approximation sets, the anytime performance, and the impact of the order used to train the Walsh surrogates. Our empirical findings show that, although our surrogate-assisted design is effective, the optimal integration of Walsh models within a multi-objective evolutionary search process gives rise to particular questions for which different trade-off answers can be obtained.
Published: 2020
Full Text: View/download PDF

24. microPhantom: Playing microRTS under uncertainty and chaos

Author: Florian Richoux, Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: FOS: Computer and information sciences, Source code, Computer science, Computer Science - Artificial Intelligence, media_common.quotation_subject, Decision theory, Chaotic, 02 engineering and technology, Track (rail transport), Constraint Programming, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Competition (economics), 0202 electrical engineering, electronic engineering, information engineering, Constraint programming, Production (economics), media_common, Focus (computing), Competition, Resilience, business.industry, Uncertainty, RTS Games, Artificial Intelligence (cs.AI), 020201 artificial intelligence & image processing, Artificial intelligence, business, Decision-making
Abstract: International audience; This competition paper presents microPhantom, a bot playing microRTS and participating in the 2020 microRTS AI competition. microPhantom is based on our previous bot POAdaptive which won the partially observable track of the 2018 and 2019 microRTS AI competitions. In this paper, we focus on decision-making under uncertainty, by tackling the Unit Production Problem with a method based on a combination of Constraint Programming and decision theory. We show that using our method to decide which units to train improves significantly the win rate against the second-best microRTS bot from the partially observable track. We also show that our method is resilient in chaotic environments, with a very small loss of efficiency only. To allow replicability and to facilitate further research, the source code of microPhantom is available, as well as the Constraint Programming toolkit it uses.
Published: 2020

25. Relational Differential Dynamic Logic

Author: Shin-ya Katsumata, Akihisa Yamada, Ichiro Hasuo, David Sprunger, Juraj Kolčák, Jérémy Dubut, Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), and The Graduate University for Advanced Studies (SOKENDAI)
Subjects: FOS: Computer and information sciences, 0209 industrial biotechnology, Computer Science - Logic in Computer Science, Theoretical computer science, Computer science, Cyber-physical system, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 02 engineering and technology, Article, cyber-physical system, Logic in Computer Science (cs.LO), Automated theorem proving, dynamic logic, 020901 industrial engineering & automation, theorem proving, Hybrid system, Differential invariant, hybrid system, 0202 electrical engineering, electronic engineering, information engineering, Dynamic logic (modal logic), 020201 artificial intelligence & image processing, Lie derivative, Rule of inference, formal verification, Formal verification
Abstract: International audience; In the field of quality assurance of hybrid systems (that combine continuous physical dynamics and discrete digital control), Platzer's differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by benchmarks provided by our industry partner , we study a relational extension of dL, aiming to formally prove statements such as "an earlier deployment of the emergency brake decreases the collision speed." A main technical challenge here is to relate two states of two dynamics at different time points. Our main contribution is a theory of suitable relational differential invariants (a relational extension of differential invariants that are central proof methods in dL), and a derived technique of time stretching. The latter features particularly high applicability, since the user does not have to synthesize a relational differential invariant out of the air. We derive new inference rules for dL from these notions, and demonstrate their use over a couple of automotive case studies.
Published: 2020

26. FusionMLS: Highly dynamic 3D reconstruction with consumer-grade RGB-D cameras

Author: Siim Meerits, Vincent Nozick, Diego Thomas, Hideo Saito, hyper vision research lab (hvrl), Kyushu University [Fukuoka], Laboratoire d'Informatique Gaspard-Monge (LIGM), Centre National de la Recherche Scientifique (CNRS)-Fédération de Recherche Bézout-ESIEE Paris-École des Ponts ParisTech (ENPC)-Université Paris-Est Marne-la-Vallée (UPEM), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-Université Pierre et Marie Curie - Paris 6 (UPMC)-The University of Tokyo (UTokyo)-Centre National de la Recherche Scientifique (CNRS), and Université Paris-Est Marne-la-Vallée (UPEM)-École des Ponts ParisTech (ENPC)-ESIEE Paris-Fédération de Recherche Bézout-Centre National de la Recherche Scientifique (CNRS)
Subjects: Computer science, Automatic identification and data capture, GPU, ComputingMethodologies_IMAGEPROCESSINGANDCOMPUTERVISION, 02 engineering and technology, Motion capture, lcsh:QA75.5-76.95, Computer graphics, Artificial Intelligence, motion capture, 0202 electrical engineering, electronic engineering, information engineering, Polygon mesh, Computer vision, 3D reconstruction, ComputingMethodologies_COMPUTERGRAPHICS, business.industry, RGB-D cameras, [INFO.INFO-CV]Computer Science [cs]/Computer Vision and Pattern Recognition [cs.CV], 020207 software engineering, Computer Graphics and Computer-Aided Design, [INFO.INFO-TI]Computer Science [cs]/Image Processing [eess.IV], RGB color model, 020201 artificial intelligence & image processing, lcsh:Electronic computers. Computer science, Computer Vision and Pattern Recognition, Artificial intelligence, Motion interpolation, Moving least squares, business
Abstract: International audience; Multi-view dynamic three-dimensional reconstruction has typically required the use of custom shutter-synchronized camera rigs in order to capture scenes containing rapid movements or complex topology changes. In this paper, we demonstrate that multiple unsynchronized low-cost RGB-D cameras can be used for the same purpose. To alleviate issues caused by unsynchronized shutters, we propose a novel depth frame interpolation technique that allows synchronized data capture from highly dynamic 3D scenes. To manage the resulting huge number of input depth images, we also introduce an efficient moving least squares-based volumetric reconstruction method that generates triangle meshes of the scene. Our approach does not store the reconstruction volume in memory, making it memory-efficient and scalable to large scenes. Our implementation is completely GPU based and works in real time. The results shown herein, obtained with real data, demonstrate the effectiveness of our proposed method and its advantages compared to state-of-the-art approaches.
Published: 2018
Full Text: View/download PDF

27. A Geometric Algebra Implementation using Binary Tree

Author: Vincent Nozick, Laurent Fuchs, Stéphane Breuils, Laboratoire d'Informatique Gaspard-Monge (LIGM), Centre National de la Recherche Scientifique (CNRS)-Fédération de Recherche Bézout-ESIEE Paris-École des Ponts ParisTech (ENPC)-Université Paris-Est Marne-la-Vallée (UPEM), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-Université Pierre et Marie Curie - Paris 6 (UPMC)-The University of Tokyo (UTokyo)-Centre National de la Recherche Scientifique (CNRS), Synthèse et analyse d'images (XLIM-ASALI), XLIM (XLIM), Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS)-Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS), and Université Paris-Est Marne-la-Vallée (UPEM)-École des Ponts ParisTech (ENPC)-ESIEE Paris-Fédération de Recherche Bézout-Centre National de la Recherche Scientifique (CNRS)
Subjects: Binary tree, Applied Mathematics, Two-element Boolean algebra, 010102 general mathematics, Universal geometric algebra, Conformal geometric algebra, [INFO.INFO-CV]Computer Science [cs]/Computer Vision and Pattern Recognition [cs.CV], geometric algebra, 01 natural sciences, Term algebra, Boolean algebra, Algebra, symbols.namesake, Geometric algebra, 0103 physical sciences, binary trees, symbols, 010307 mathematical physics, 0101 mathematics, implementation, Time complexity, [INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS], Mathematics
Abstract: International audience; This paper presents an efficient implementation of geometric algebra, based on a recursive representation of the algebra elements using binary trees. The proposed approach consists in restructuring a state of the art recursive algorithm to handle parallel optimizations. The resulting algorithm is described for the outer product and the geometric product. The proposed implementation is usable for any dimensions, including high dimension (e.g. algebra of dimension 15). The method is compared with the main state of the art geometric algebra implementations , with a time complexity study as well as a practical benchmark. The tests show that our implementation is at least as fast as the main geometric algebra implementations.
Published: 2017
Full Text: View/download PDF

28. On the Design of a Partition Crossover for the Quadratic Assignment Problem

Author: Omar Abdelkafi, Bilel Derbel, Arnaud Liefooghe, Darrell Whitley, Optimisation de grande taille et calcul large échelle (BONUS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Colorado State University [Fort Collins] (CSU), The three first authors are supported by the French national research agency (ANR-16-CE23-0013-01) and the Research Grants Council of Hong Kong (RGC Project No. A-CityU101/16)., and ANR-16-CE23-0013,BigMO,Optimisation Multiobjectif Big(2016)
Subjects: 050101 languages & linguistics, Quadratic assignment problem, Computer science, 05 social sciences, Crossover, 02 engineering and technology, Partition (database), Execution time, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Fast evaluation, 0202 electrical engineering, electronic engineering, information engineering, Bipartite graph, Preprocessor, 020201 artificial intelligence & image processing, 0501 psychology and cognitive sciences, Algorithm, Formal description
Abstract: International audience; We conduct a study on the design of a partition crossover for the QAP. On the basis of a bipartite graph representation, we propose to recombine the unshared components from parents, while enabling their fast evaluation using a preprocessing step for objective function decomposition. Besides a formal description and complexity analysis of the proposed crossover, we conduct an empirical analysis on its relative behavior using a number of large-size QAP instances, and a number of baseline crossovers. The proposed operator is shown to have a relatively high intensification ability, while keeping execution time relatively low.
Published: 2020
Full Text: View/download PDF

29. Instance space analysis of combinatorial multi-objective optimization problems

Author: Kate Smith-Miles, Arnaud Liefooghe, Estefania Yap, Mario A. Muñoz, University of Melbourne, Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Optimisation de grande taille et calcul large échelle (BONUS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), The University of Melbourne, and Université de Lille-Centrale Lille-Centre National de la Recherche Scientifique (CNRS)-Université de Lille-Centrale Lille-Centre National de la Recherche Scientifique (CNRS)
Subjects: Optimization problem, landscape analysis, Computer science, Feature extraction, 0211 other engineering and technologies, Decision tree, Feature selection, 02 engineering and technology, Space (commercial competition), Machine learning, computer.software_genre, Multi-objective optimization, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], 0202 electrical engineering, electronic engineering, information engineering, black-box combinatorial optimization, Cluster analysis, 021103 operations research, business.industry, [INFO.INFO-RO]Computer Science [cs]/Operations Research [cs.RO], Visualization, 020201 artificial intelligence & image processing, Artificial intelligence, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], business, computer, feature-based performance prediction
Abstract: International audience; In recent years, there has been a continuous stream of development in evolutionary multi-objective optimization (EMO) algorithms. The large quantity of existing algorithms introduces difficulty in selecting suitable algorithms for a given problem instance. In this paper, we perform instance space analysis on discrete multi-objective optimization problems (MOPs) for the first time under three different conditions. We create visualizations of the relationship between problem instances and algorithm performance for instance features previously identified using decision trees, as well an independent feature selection. The suitability of these features in discriminating between algorithm performance and understanding strengths and weaknesses is investigated. Furthermore, we explore the impact of various definitions of “good” performance. The visualization of the instance space provides an alternative method of algorithm discrimination by showing clusters of instances where algorithms perform well across the instance space. We validate the suitability of existing features and identify opportunities for future development.
Published: 2020
Full Text: View/download PDF

30. Efficient verification of Boson Sampling

Author: Damian Markham, Frédéric Grosshans, Ulysse Chabaud, Elham Kashefi, Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), School of Informatics [Edimbourg], University of Edinburgh, Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Speedup, Physics and Astronomy (miscellaneous), Field (physics), Computer science, Gaussian, QC1-999, Optical computing, FOS: Physical sciences, 01 natural sciences, 010305 fluids & plasmas, Computational science, symbols.namesake, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Quantum state, 0103 physical sciences, 010306 general physics, Quantum, Boson, Quantum computer, Quantum Physics, Physics, TheoryofComputation_GENERAL, Atomic and Molecular Physics, and Optics, ComputerSystemsOrganization_MISCELLANEOUS, symbols, Quantum Physics (quant-ph)
Abstract: The demonstration of quantum speedup, also known as quantum computational supremacy, that is the ability of quantum computers to outperform dramatically their classical counterparts, is an important milestone in the field of quantum computing. While quantum speedup experiments are gradually escaping the regime of classical simulation, they still lack efficient verification protocols and rely on partial validation. Here we derive an efficient protocol for verifying with single-mode Gaussian measurements the output states of a large class of continuous-variable quantum circuits demonstrating quantum speedup, including Boson Sampling experiments, thus enabling a convincing demonstration of quantum speedup with photonic computing. Beyond the quantum speedup milestone, our results also enable the efficient and reliable certification of a large class of intractable continuous-variable multimode quantum states., Comment: 15+21 pages, 4 figures. Comments welcome!
Published: 2020
Full Text: View/download PDF

31. Fault-tolerant quantum speedup from constant depth quantum circuits

Author: Damian Markham, Joseph Dgheim, Joe Ghalbouni, Rawad Mezher, University of Edinburgh, Information Quantique [LIP6] (QI), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Quantum Physics, Speedup, Computer science, Quantum noise, Magic (programming), FOS: Physical sciences, Topology, 01 natural sciences, 010305 fluids & plasmas, Quantum circuit, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Qubit, 0103 physical sciences, 010306 general physics, Quantum Physics (quant-ph), Quantum, Quantum computer, Electronic circuit
Abstract: A defining feature in the field of quantum computing is the potential of a quantum device to outperform its classical counterpart for a specific computational task. By now, several proposals exist showing that certain sampling problems can be done efficiently quantumly, but are not possible efficiently classically, assuming strongly held conjectures in complexity theory. A feature dubbed quantum speedup. However, the effect of noise on these proposals is not well understood in general, and in certain cases it is known that simple noise can destroy the quantum speedup. Here we develop a fault-tolerant version of one family of these sampling problems, which we show can be implemented using quantum circuits of constant depth. We present two constructions, each taking $poly(n)$ physical qubits, some of which are prepared in noisy magic states. The first of our constructions is a constant depth quantum circuit composed of single and two-qubit nearest neighbour Clifford gates in four dimensions. This circuit has one layer of interaction with a classical computer before final measurements. Our second construction is a constant depth quantum circuit with single and two-qubit nearest neighbour Clifford gates in three dimensions, but with two layers of interaction with a classical computer before the final measurements. For each of these constructions, we show that there is no classical algorithm which can sample according to its output distribution in $poly(n)$ time, assuming two standard complexity theoretic conjectures hold. The noise model we assume is the so-called local stochastic quantum noise. Along the way, we introduce various new concepts such as constant depth magic state distillation (MSD), and constant depth output routing, which arise naturally in measurement based quantum computation (MBQC), but have no constant-depth analogue in the circuit model., Comment: 26 pages, 6 figures, comments are welcome, new references added
Published: 2020
Full Text: View/download PDF

32. Parametric Timed Model Checking for Guaranteeing Timed Opacity

Author: Jun Sun, Étienne André, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Singapore Management University (SIS), Singapore Management University, This work is partially supported by the ANR national research pro-gram PACS (ANR-14-CE28-0002) and by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST., Ming-Hsien Tsai, Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza, ANR PACS (ANR-14-CE28-0002), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, and ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014)
Subjects: Model checking, Opacity, Computer Science - Logic in Computer Science, 050101 languages & linguistics, Computer Science - Cryptography and Security, Theoretical computer science, Computer science, 05 social sciences, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 02 engineering and technology, Execution time, Automaton, Decidability, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Program analysis, Information leakage, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, 0501 psychology and cognitive sciences, Timed automata, Parametric statistics, Parameter synthesis
Abstract: Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time. We address the following problem: given a timed system, synthesize the execution times for which one cannot deduce whether the system performed some secret behavior. We solve this problem in the setting of timed automata (TAs). We first provide a general solution, and then extend the problem to parametric TAs, by synthesizing internal timings making the TA secure. We study decidability, devise algorithms, and show that our method can also apply to program analysis., Comment: This is the author (and extended) version of the manuscript of the same name published in the proceedings of ATVA 2019. This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002), the ANR-NRF research program (ProMiS) and by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
Published: 2019

33. Complete Non-Orders and Fixed Points

Author: Yamada, Akihisa, Dubut, Jérémy, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, Grant-in-aid No. 19K20215, JSPS, John Harrison, John O'Leary, and Andrew Tolmach
Subjects: 000 Computer science, knowledge, general works, 020204 information systems, 0502 economics and business, 05 social sciences, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 050211 marketing, Order Theory, 02 engineering and technology, Fixed-Points, Lattice Theory, Isabelle/HOL
Abstract: International audience; In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster–Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition – attractivity – which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points.
Published: 2019
Full Text: View/download PDF

34. Garamon: A Geometric Algebra Library Generator

Author: Vincent Nozick, Stéphane Breuils, Laurent Fuchs, Laboratoire d'Informatique Gaspard-Monge (LIGM), Centre National de la Recherche Scientifique (CNRS)-Fédération de Recherche Bézout-ESIEE Paris-École des Ponts ParisTech (ENPC)-Université Paris-Est Marne-la-Vallée (UPEM), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), SIC, XLIM (XLIM), and Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS)-Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS)-Université de Poitiers
Subjects: Multivector, Prefix tree, Applied Mathematics, 010102 general mathematics, Clifford algebra, Geometric Algebra, Python (programming language), Data structure, 01 natural sciences, Software implementation, Algebra, Clifford Algebra, Geometric algebra, 0103 physical sciences, Trie, 010307 mathematical physics, 0101 mathematics, computer, Vector space, Mathematics, computer.programming_language, [INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS]
Abstract: International audience; This paper presents both a recursive scheme to perform Geometric Algebra operations over a prefix tree, and Garamon, a C++ library generator implementing these recursive operations. While for low dimension vector spaces, precomputing all the Geometric Algebra products is an efficient strategy, it fails for higher dimensions where the operation should be computed at run time. This paper describes how a prefix tree can be a support for a recursive formulation of Geometric Algebra operations. This recursive approach presents a much better complexity than the usual run time methods. This paper also details how a prefix tree can represent efficiently the dual of a multivector. These results constitute the foundations for Garamon, a C++ library generator synthesizing efficient C++ / Python libraries implementing Geometric Algebra in both low and higher dimensions, with any arbitrary metric. Garamon takes advantage of the prefix tree formulation to implement Geometric Algebra operations on high dimensions hardly accessible with state-of-the-art software implementations. Garamon is designed to produce easy to install , easy to use, effective and numerically stable libraries. The design of the libraries is based on a data structure using precomputed functions for low dimensions and a smooth transition to the new recursive products for higher dimensions. Mathematics Subject Classification (2010). Primary 99Z99; Secondary 00A00.
Published: 2019
Full Text: View/download PDF

35. Modular Convolutional Neural Network for Discriminating between Computer-Generated Images and Photographic Images

Author: Isao Echizen, T. Ngoc-Dung Tieu, Junichi Yamagishi, Huy H. Nguyen, Hoang-Quoc Nguyen-Son, Vincent Nozick, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-Université Pierre et Marie Curie - Paris 6 (UPMC)-The University of Tokyo (UTokyo)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Discriminator, Spoofing attack, Computer science, business.industry, Computer-generated imagery, Probabilistic logic, ComputingMethodologies_IMAGEPROCESSINGANDCOMPUTERVISION, convolutional neural network, digital image forensics, [INFO.INFO-CV]Computer Science [cs]/Computer Vision and Pattern Recognition [cs.CV], 020207 software engineering, Pattern recognition, 02 engineering and technology, Modular design, 16. Peace & justice, Convolutional neural network, computer-generated image, photographic image, [INFO.INFO-TI]Computer Science [cs]/Image Processing [eess.IV], 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Digital image forensics, Artificial intelligence, business, Transformer (machine learning model)
Abstract: International audience; Discriminating between computer-generated images (CGIs) and photographic images (PIs) is not a new problem in digital image forensics. However, with advances in rendering techniques supported by strong hardware and in genera-tive adversarial networks, CGIs are becoming indistinguishable from PIs in both human and computer perception. This means that malicious actors can use CGIs for spoofing facial authentication systems, impersonating other people, and creating fake news to be spread on social networks. The methods developed for discriminating between CGIs and PIs quickly become outdated and must be regularly enhanced to be able to reduce these attack surfaces. Leveraging recent advances in deep convolutional networks, we have built a modular CGI-PI discriminator with a customized VGG-19 network as the feature extractor, statistical convolutional neural networks as the feature transformers, and a discriminator. We also devised a probabilistic patch aggregation strategy to deal with high-resolution images. This proposed method outper-formed a state-of-the-art method and achieved accuracy up to 100%.
Published: 2019
Full Text: View/download PDF

36. Time4sys2imi: A tool to formalize real-time system models under uncertainty

Author: Étienne André, Jawher Jerray, Sahar Mhiri, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), This work is supported by the ASTREI project funded by the Paris Île-de-France Region, with the additional support of the ANR national research program PACS (ANR-14-CE28-0002) and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, Robert M. Hierons, Mohamed Mosbah, ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014), André, Étienne, and Appel à projets générique - Analyses paramétrées de systèmes concurrents - - PACS2014 - ANR-14-CE28-0002 - Appel à projets générique - VALID
Subjects: Model checking, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], parameter synthesis, Computer science, Formal semantics (linguistics), 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Computer Science - Software Engineering, 0202 electrical engineering, electronic engineering, information engineering, Graphical specification, scheduling, Real-time operating system, Real-time systems, Parametric statistics, Programming language, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, parametric timed automata, Input language, model checking, Automaton, Logic in Computer Science (cs.LO), [INFO.INFO-ES] Computer Science [cs]/Embedded Systems, Software Engineering (cs.SE), 010201 computation theory & mathematics, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, computer
Abstract: Time4sys is a formalism developed by Thales, realizing a graphical specification for real-time systems. However, this formalism does not allow to perform formal analyses for real-time systems. So a translation of this tool to a formalism equipped with a formal semantics is needed. We present here Time4sys2imi, a tool translating Time4sys models into parametric timed automata in the input language of IMITATOR. This translation allows not only to check the schedulability of real-time systems, but also to infer some timing constraints (e.g., deadlines, offsets) guaranteeing schedulability. We successfully applied Time4sys2imi to various examples., This is the author (and extended) version of the manuscript of the same name published in the proceedings of ICTAC 2019. This work is supported by the ASTREI project funded by the Paris \^Ile-de-France Region, with the additional support of the ANR national research program PACS (ANR-14-CE28-0002) and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
Published: 2019

37. Formalizing Time4sys using parametric timed automata

Author: Étienne André, Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), National Institute of Informatics (NII), This work is supported by the ASTREI project funded by the Paris Île-de-France Region, with the additional support of the ANR national research program PACS (ANR-14-CE28-0002) and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST., Dominique Mery, Shengchao Qin, ANR PACS (ANR-14-CE28-0002), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, ASTREI project funded by the Paris Île-de-France Region, ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014), André, Étienne, and Appel à projets générique - Analyses paramétrées de systèmes concurrents - - PACS2014 - ANR-14-CE28-0002 - Appel à projets générique - VALID
Subjects: FOS: Computer and information sciences, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Formal Languages and Automata Theory (cs.FL), Programming language, Computer science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science - Formal Languages and Automata Theory, 020207 software engineering, 02 engineering and technology, computer.software_genre, Formal reasoning, [INFO.INFO-ES] Computer Science [cs]/Embedded Systems, Automaton, Software Engineering (cs.SE), Computer Science - Software Engineering, Formalism (philosophy of mathematics), 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Formal verification, computer, Parametric statistics
Abstract: Critical real-time systems must be verified to avoid the risk of dramatic consequences in case of failure. Thales developed an open formalism Time4sys to model real-time systems, with expressive features such as periodic or sporadic tasks, task dependencies, distributed systems, etc. However, Time4sys does not natively allow for a formal reasoning. In this work, we present a translation from Time4sys to (parametric) timed automata, so as to allow for a formal verification., Comment: This is the author (and slightly extended) version of the manuscript of the same name published in the proceedings of the 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019)
Published: 2019

38. Computing a Lattice Basis Revisited

Author: Phong Q. Nguyen, Jianwei Li, Centre for Quantum Technologies [Singapore] (CQT), National University of Singapore (NUS), Key Laboratory of Mathematics Mechanization (KLMM), Chinese Academy of Sciences [Changchun Branch] (CAS)-Institute of Systems Science (ISS), China-Academy of Mathematics and Systems Science [Beijing], Construction and Analysis of Systems for Confidentiality and Authenticity of Data and Entities (CASCADE), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), and Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris)
Subjects: XGCD, 010102 general mathematics, 010103 numerical & computational mathematics, 01 natural sciences, Combinatorics, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], HNF, Lattice (order), Lattice algorithms, Integer quadratic forms, 0101 mathematics, Z-basis, Lattice basis, ComputingMilieux_MISCELLANEOUS, Mathematics
Abstract: Given (a,b) \in \mZ^2, Euclid's algorithm outputs the generator \gcd(a,b) of the ideal a\mZ + b\mZ. Computing a lattice basis is a high-dimensional generalization: given \mathbfa _1,\dots,\veca _n \in \mZ^m, find a \mZ-basis of the lattice L=\ \sum_i=1 ^n x_i \veca _i, x_i \in \mZ\ generated by the \veca _i's. The fastest algorithms known are HNF algorithms, but are not adapted to all applications, such as when the output should not be much longer than the input. We present an algorithm which extracts such a short basis within the same time as an HNF, by reduction to HNF. We also present an HNF-less algorithm, which reduces to Euclid's extended algorithm and can be generalized to quadratic forms. Both algorithms can extend primitive sets into bases.
Published: 2019
Full Text: View/download PDF

39. Parametric schedulability analysis of a launcher flight control system under reactivity constraints

Author: Étienne André, David Lesens, Laurent Fribourg, Emmanuel Coquard, Jawher Jerray, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), ArianeGroup SAS, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Wil van der Aalst, Jörg Keller, Wojciech Penczek, ANR PACS (ANR-14-CE28-0002), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, Paris Île-de-France Region (project DIM RFSI ASTREI), ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), ArianeGroup, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord, This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002) and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST., ANR-14-CE28-0002, André, Étienne, Appel à projets générique - Analyses paramétrées de systèmes concurrents - - PACS2014 - ANR-14-CE28-0002 - Appel à projets générique - VALID, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, 050101 languages & linguistics, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], parameter synthesis, Computer science, Control (management), Scheduling (production processes), 0102 computer and information sciences, 02 engineering and technology, Systems and Control (eess.SY), 01 natural sciences, Electrical Engineering and Systems Science - Systems and Control, Theoretical Computer Science, law.invention, Instruction set, Computer Science - Software Engineering, Development (topology), law, [INFO.INFO-SY]Computer Science [cs]/Systems and Control [cs.SY], 0202 electrical engineering, electronic engineering, information engineering, FOS: Electrical engineering, electronic engineering, information engineering, 0501 psychology and cognitive sciences, IMITATOR, scheduling, Duration (project management), Stopwatch, Parametric statistics, Algebra and Number Theory, 05 social sciences, D.2.4, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Control engineering, model checking, [INFO.INFO-ES] Computer Science [cs]/Embedded Systems, Automaton, Logic in Computer Science (cs.LO), Software Engineering (cs.SE), real-time systems, Computational Theory and Mathematics, 010201 computation theory & mathematics, Control system, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Information Systems
Abstract: The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling., Comment: This manuscript is the author version of the manuscript of the same name published in Fundamenta Informatica 182(1). This is an extended version of the manuscript published in the proceedings of the 19th International Conference on Application of Concurrency to System Design (ACSD 2019). arXiv admin note: substantial text overlap with arXiv:1903.07217
Published: 2019
Full Text: View/download PDF

40. Codensity Games for Bisimilarity

Author: Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Samuel Humeau, Clovis Eberhart, Ichiro Hasuo, Graduate University for Advanced Studies [Hayama] (SOKENDAI), National Institute of Informatics (NII), University of Oxford, École normale supérieure de Lyon (ENS de Lyon), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Theoretical computer science, Computer Networks and Communications, Computer science, Markov process, 0102 computer and information sciences, 01 natural sciences, Theoretical Computer Science, symbols.namesake, Process theory, [INFO]Computer Science [cs], [MATH]Mathematics [math], 0101 mathematics, Categorical variable, Bisimulation, 010102 general mathematics, Probabilistic logic, Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Spoiler, Hardware and Architecture, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, symbols, Software
Abstract: Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways: notably, bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric) as well as new ones (including what we call bisimulation topology)., Comment: 13 pages + 3 page appendix, to appear in Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019)
Published: 2019
Full Text: View/download PDF

41. Parametric updates in parametric timed automata

Author: André, Étienne, Lime, Didier, Ramparison, Mathias, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Jorge A. Pérez, Nobuko Yoshida, TC 6, WG 6.1, ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), STR (LS2N - équipe STR ), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-École Centrale de Nantes (Nantes Univ - ECN), Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST), Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Nantes Université (Nantes Univ), Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord, University of Luxembourg [Luxembourg], VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002) and by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015). É. André was partially supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST., ANR-19-CE25-0015,ProMiS,Mitigation formelle d'attaques via canaux auxiliaires par vérification paramétrée(2019), and École Centrale de Nantes (ECN)
Subjects: FOS: Computer and information sciences, Computer Science::Computer Science and Game Theory, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Computer science, Formal Languages and Automata Theory (cs.FL), ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.3: Formal Languages/F.4.3.3: Decision problems, Timed automaton, Value (computer science), Computer Science - Formal Languages and Automata Theory, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Subclass, Set (abstract data type), Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Parametric statistics, decidability, parametric difference bound matrix, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, parametric timed automata, clock regions, Decidability, Automaton, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, timed automata, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Algorithm, Computer Science::Formal Languages and Automata Theory, parametric updates
Abstract: Logical Methods in Computer Science ; Volume 17, Issue 2 ; 1860-5974, We introduce a new class of Parametric Timed Automata (PTAs) where we allow clocks to be compared to parameters in guards, as in classic PTAs, but also to be updated to parameters. We focus here on the EF-emptiness problem: "is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?". This problem is well-known to be undecidable for PTAs, and so it is for our extension. Nonetheless, if we update all clocks each time we compare a clock with a parameter and each time we update a clock to a parameter, we obtain a syntactic subclass for which we can decide the EF-emptiness problem and even perform the exact synthesis of the set of rational valuations such that a given location is reachable. To the best of our knowledge, this is the first non-trivial subclass of PTAs, actually even extended with parametric updates, for which this is possible.
Published: 2019
Full Text: View/download PDF

42. Parametric analyses of attack-fault trees

Author: Étienne André, Mariëlle Stoelinga, Mathias Ramparison, Didier Lime, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), National Institute of Informatics (NII), Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Laboratoire d'Informatique de Paris-Nord (LIPN), Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord, University of Luxembourg [Luxembourg], VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Formal Methods and Tools (FMT group), University of Twente, This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002), the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015), the PHC Van Gogh project PAMPAS, by STW under the project 15474 SEQUOIA, KIA KIEM project 628.010.006 StepUp, the EU under the project 102112 SUCCESS and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST., ANR-14-CE28-0002, ANR-19-CE25-0015 ProMiS, PHC Van Gogh project PAMPAS, 15474 SEQUOIA, ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, KIA KIEM project 628.010.006 StepUp, ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014), ANR-19-CE25-0015,ProMiS,Mitigation formelle d'attaques via canaux auxiliaires par vérification paramétrée(2019), European Project: 102112,SUCCESS, IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), University of Twente [Netherlands], Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Centre of Telematics and Information Technology (CTIT), Twenty University, This work is supported by ANR PACS (ANR-14-CE28-0002), the PHC Van Gogh project PAMPAS, by STW under the project 15474 SEQUOIA, KIA KIEM project 628.010.006 StepUp, the EU under the project 102112 SUCCESS and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, ANR PACS (ANR-14-CE28-0002), STW 15474 SEQUOIA, EU 102112 SUCCESS, Formal Methods and Tools, and Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS)
Subjects: FOS: Computer and information sciences, Theoretical computer science, Computer Science - Cryptography and Security, Computer science, Computation, Cost accounting, 0102 computer and information sciences, 02 engineering and technology, security, Fault (power engineering), 01 natural sciences, Theoretical Computer Science, Set (abstract data type), [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Unified Modeling Language, Safety engineering, 0202 electrical engineering, electronic engineering, information engineering, IMITATOR, Engineering(all), computer.programming_language, Parametric statistics, Fault tree analysis, Algebra and Number Theory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], parametric timed automata, Extension (predicate logic), attack-fault trees, Tree (graph theory), Automaton, Computational Theory and Mathematics, 010201 computation theory & mathematics, Logic gate, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Cryptography and Security (cs.CR), computer, Information Systems
Abstract: Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i.e. absence of unintentional failures) and security (i.e. no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to help considering these problems is attack trees, a tree-based formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parametrize constants such as time and discrete costs in an AFT and then, using the model-checker IMITATOR, to compute the set of parameter values such that a successful attack is possible. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient counter-measure., This is the extended version of the manuscript of the same name published in ACSD 2019. This work is supported by ANR PACS (ANR-14-CE28-0002), the PHC Van Gogh project PAMPAS, by STW under the project 15474 SEQUOIA, KIA KIEM project 628.010.006 StepUp, the EU under the project 102112 SUCCESS and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
Published: 2019
Full Text: View/download PDF

43. Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking

Author: Étienne André, Jean-Marc Mota, Laurent Fribourg, Romain Soulat, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Thales Communications & Security S.A.S [Velizy], THALES COMMUNICATIONS & SECURITY S.A.S, Thales Research and Technology [Palaiseau], THALES, ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, Constantin Enea and Ruzica Piskac, Springer, ANR PACS (ANR-14-CE28-0002), and ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014)
Subjects: Model checking, FOS: Computer and information sciences, 050101 languages & linguistics, Leader election, Computer Science - Logic in Computer Science, Theoretical computer science, Correctness, Computer science, 05 social sciences, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 02 engineering and technology, Solver, 16. Peace & justice, Logic in Computer Science (cs.LO), Asynchronous communication, Distributed algorithm, Parametric model, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, 0501 psychology and cognitive sciences, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Parametric statistics
Abstract: The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i.e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number p of processes (p=5000)., Comment: This is the author version of the manuscript of the same name published in the proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2019)
Published: 2019
Full Text: View/download PDF

44. Parametric Timed Broadcast Protocols

Author: Étienne André, Paulin Fournier, Didier Lime, Benoît Delahaye, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), École Centrale de Nantes (ECN), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, Constantin Enea and Ruzica Piskac, ANR PACS (ANR-14-CE28-0002), and ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014)
Subjects: Clique, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Theoretical computer science, Computer science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Decidability, Automaton, Logic in Computer Science (cs.LO), Set (abstract data type), 010201 computation theory & mathematics, Reachability, 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, State (computer science), Parametric statistics
Abstract: In this paper we consider state reachability in networks composed of many identical processes running a parametric timed broadcast protocol (PTBP). PTBP are a new model extending both broadcast protocols and parametric timed automata. This work is, up to our knowledge, the first to consider the combination of both a parametric network size and timing parameters in clock guard constraints. Since the communication topology is of utmost importance in broadcast protocols, we investigate reachability problems in both clique semantics where every message reaches every processes, and in reconfigurable semantics where the set of receivers is chosen non-deterministically. In addition, we investigate the decidability status depending on whether the timing parameters in guards appear only as upper bounds in guards, as lower bounds or when the set of parameters is partitioned in lower-bound and upper-bound parameters., Comment: This is the author (and extended) version of the manuscript of the same name published in the proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2019). This version contains additional examples and all proofs
Published: 2019
Full Text: View/download PDF

45. Repairing Timed Automata Clock Guards through Abstraction and Testing

Author: Angelo Gargantini, Marco Radavelli, Paolo Arcaini, Étienne André, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Università degli studi di Bergamo (UniBG), This work is partially supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST and by the ANR national research program PACS (ANR-14-CE28-0002)., Dirk Beyer, Chantal Keller, ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, ANR PACS (ANR-14-CE28-0002), and ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014)
Subjects: Discrete mathematics, FOS: Computer and information sciences, 050101 languages & linguistics, Computer Science - Logic in Computer Science, Computer science, 05 social sciences, init, Timed automaton, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 02 engineering and technology, Oracle, Automaton, Logic in Computer Science (cs.LO), Formalism (philosophy of mathematics), 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, 0501 psychology and cognitive sciences, Guard (computer science), [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni, Parametric statistics, Test data
Abstract: Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a TA, and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions (i.e., the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA), i.e., a TA in which some constants are parametrized. The paper presents a process that i) abstracts the initial (faulty) TA tainit in a PTA pta; ii) generates some test data (i.e., timed traces) from pta; iii) assesses the correct evaluation of the traces with the oracle; iv) uses the IMITATOR tool for synthesizing some constraints phi on the parameters of pta; v) instantiate from phi a TA tarep as final repaired model. Experiments show that the approach is successfully able to partially repair the initial design of the user., Comment: This is the author (and slightly extended) version of the manuscript of the same name published in the proceedings of the 13th International Conference on Tests and Proofs (TAP 2019). This version contains some additional explanations and all proofs
Published: 2019
Full Text: View/download PDF

46. Symbolic Monitoring against Specifications Parametric in Time and Data

Author: Waga, Masaki, André, Étienne, Hasuo, Ichiro, André, Étienne, Appel à projets générique - Analyses paramétrées de systèmes concurrents - - PACS2014 - ANR-14-CE28-0002 - Appel à projets générique - VALID, Isil Dillig, Serdar Tasiran, National Institute of Informatics (NII), JSPS Research Fellow, The Graduate University for Advanced Studies, japan (SOKENDAI), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), This work is partially supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), by JSPS Grants-in-Aid No. 15KT0012 & 18J22498 and by the ANR national research program PACS (ANR-14-CE28-0002)., ANR PACS (ANR-14-CE28-0002), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, and ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014)
Subjects: FOS: Computer and information sciences, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Formal Languages and Automata Theory (cs.FL), FOS: Electrical engineering, electronic engineering, information engineering, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Computer Science - Formal Languages and Automata Theory, Systems and Control (eess.SY), Electrical Engineering and Systems Science - Systems and Control, [INFO.INFO-ES] Computer Science [cs]/Embedded Systems
Abstract: Monitoring consists in deciding whether a log meets a given specification. In this work, we propose an automata-based formalism to monitor logs in the form of actions associated with time stamps and arbitrarily data values over infinite domains. Our formalism uses both timing parameters and data parameters, and is able to output answers symbolic in these parameters and in the log segments where the property is satisfied or violated. We implemented our approach in an ad-hoc prototype SyMon, and experiments show that its high expressive power still allows for efficient online monitoring., Comment: Accepted to CAV 2019
Published: 2019
Full Text: View/download PDF

47. Online Parametric Timed Pattern Matching with Automata-Based Skipping

Author: Étienne André, Masaki Waga, National Institute of Informatics (NII), The Graduate University for Advanced Studies, japan (SOKENDAI), JSPS Research Fellow, Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Moshe Vardi, Julia Badger, Kristin Yvonne Rozier, JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JSPS Grants-in-Aid No. 15KT0012 & 18J22498, ANR national research program PACS (ANR-14-CE28-0002), and ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014)
Subjects: Model checking, Computer science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], parametric timed automata, Computer Science - Formal Languages and Automata Theory, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Automaton, monitoring, real-time systems, 010201 computation theory & mathematics, Robustness (computer science), 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Pattern matching, Algorithm, Parametric statistics
Abstract: Timed pattern matching has strong connections with monitoring real-time systems. Given a log and a specification containing timing parameters (that can capture uncertain or unknown constants), parametric timed pattern matching aims at exhibiting for which start and end dates, as well as which parameter valuations, a specification holds on that log. This problem is notably close to robustness. We propose here a new framework for parametric timed pattern matching. Not only we dramatically improve the efficiency when compared to a previous method based on parametric timed model checking, but we further propose optimizations based on skipping. Our algorithm is suitable for online monitoring, and experiments show that it is fast enough to be applied at runtime., Comment: Accepted to NFM 2019. arXiv admin note: text overlap with arXiv:1812.08940
Published: 2019
Full Text: View/download PDF

48. Moment Propagation of Discrete-Time Stochastic Polynomial Systems using Truncated Carleman Linearization

Author: Pruekprasert, Sasinee, Takisaka, Toru, Eberhart, Clovis, Cetinkaya, Ahmet, Dubut, Jérémy, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), and National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: [MATH.MATH-PR]Mathematics [math]/Probability [math.PR], FOS: Electrical engineering, electronic engineering, information engineering, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Systems and Control (eess.SY), Electrical Engineering and Systems Science - Systems and Control, ComputingMilieux_MISCELLANEOUS
Abstract: We propose a method to compute an approximation of the moments of a discrete-time stochastic polynomial system. We use the Carleman linearization technique to transform this finite-dimensional polynomial system into an infinite-dimensional linear one. After taking expectation and truncating the induced deterministic dynamics, we obtain a finite-dimensional linear deterministic system, which we then use to iteratively compute approximations of the moments of the original polynomial system at different time steps. We provide upper bounds on the approximation error for each moment and show that, for large enough truncation limits, the proposed method precisely computes moments for sufficiently small degrees and numbers of time steps. We use our proposed method for safety analysis to compute bounds on the probability of the system state being outside a given safety region. Finally, we illustrate our results on two concrete examples, a stochastic logistic map and a vehicle dynamics under stochastic disturbance., Comment: 21st IFAC World Congress (IFAC 2020)
Published: 2019
Full Text: View/download PDF

49. Decision Making for Autonomous Vehicles at Unsignalized Intersection in Presence of Malicious Vehicles

Author: Chao Huang, Jérémy Dubut, Xiaoyi Zhang, Masako Kishida, Sasinee Pruekprasert, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, and Grant-in-aid No. 19K20215, JSPS
Subjects: 050210 logistics & transportation, Operations research, [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], Intersection (set theory), Computer science, 05 social sciences, Control (management), Systems and Control (eess.SY), 16. Peace & justice, Electrical Engineering and Systems Science - Systems and Control, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, symbols.namesake, Order (business), Nash equilibrium, 0502 economics and business, symbols, [INFO.INFO-SY]Computer Science [cs]/Systems and Control [cs.SY], FOS: Electrical engineering, electronic engineering, information engineering, 050207 economics
Abstract: In this paper, we investigate the decision making of autonomous vehicles in an unsignalized intersection in presence of malicious vehicles, which are vehicles that do not respect the law by not using the proper rules of the right of way. Each vehicle computes its control input as a Nash equilibrium of a game determined by the priority order based on its own belief: each of non-malicious vehicle bases its order on the law, while a malicious one considers itself as having priority. To illustrate our method, we provide numerical simulations, with different scenarios given by different cases of malicious vehicles., Comment: IEEE Conference on Intelligent Transportation Systems (ITSC), 2019
Published: 2019
Full Text: View/download PDF

50. On the expressive power of invariants in parametric timed automata

Author: Étienne André, Didier Lime, Mathias Ramparison, National Institute of Informatics (NII), Japanese French Laboratory for Informatics (JFLI), National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), STR (STR ), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Jing Sun, Jun Pang, ANR PACS (ANR-14-CE28-0002), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, and ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Theoretical computer science, Computer science, Reachability problem, Formal Languages and Automata Theory (cs.FL), Concurrency, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science - Formal Languages and Automata Theory, 020207 software engineering, 02 engineering and technology, 16. Peace & justice, Rotation formalisms in three dimensions, Undecidable problem, Automaton, Decidability, Logic in Computer Science (cs.LO), Reachability, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Computer Science::Formal Languages and Automata Theory, Parametric statistics
Abstract: The verification of systems combining hard timing constraints with concurrency is challenging. This challenge becomes even harder when some timing constants are missing or unknown. Parametric timed formalisms, such as parametric timed automata (PTAs), tackle the synthesis of such timing constants (seen as parameters) for which a property holds. Such formalisms are highly expressive, but also undecidable, and few decidable subclasses were proposed. We propose here a syntactic restriction on PTAs consisting in removing guards (constraints on transitions) to keep only invariants (constraints on locations). While this restriction preserves the expressiveness of PTAs (and therefore their undecidability), an additional restriction on the type of constraints allows to not only prove decidability, but also to perform the exact synthesis of parameter valuations satisfying reachability. This formalism, that seems trivial at first sight as it benefits from the decidability of the reachability problem with a better complexity than Timed Automata (TAs), suffers from the undecidability of the whole TCTL logic that TAs, on the contrary enjoy. We believe our formalism allows for an interesting trade-off between decidability and practical expressiveness and is therefore promising. We show its applicability in a small case study., Comment: This is the author version of the manuscript of the same name published in the proceedings of the 24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019). This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002) and by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
Published: 2019
Full Text: View/download PDF

Catalog

Books, media, physical & digital resources

See catalog results

Searchworks

Select search scope, currently: Articles Catalog books, media & more in Jio Institute collections Articles journal articles & other e-resources

Search

Search Constraints

Refine your results

Search Limiters

Topic

Publication Year Range

Language

Journal

Database

Publisher

111 results on '"Japanese French Laboratory for Informatics (JFLI)"'

Search Results

Catalog

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources