3 Search Results for "Ross, Neil J."

Document
DOI: 10.4230/LITES.8.1.2
Micro- and Macroscopic Road Traffic Analysis using Drone Image Data

Authors: Friedrich Kruber, Eduardo Sánchez Morales, Robin Egolf, Jonas Wurst, Samarjit Chakraborty, and Michael Botsch

Published in: LITES, Volume 8, Issue 1 (2022): Special Issue on Embedded Systems for Computer Vision. Leibniz Transactions on Embedded Systems, Volume 8, Issue 1

Abstract
The current development in the drone technology, alongside with machine learning based image processing, open new possibilities for various applications. Thus, the market volume is expected to grow rapidly over the next years. The goal of this paper is to demonstrate the capabilities and limitations of drone based image data processing for the purpose of road traffic analysis. In the first part a method for generating microscopic traffic data is proposed. More precisely, the state of vehicles and the resulting trajectories are estimated. The method is validated by conducting experiments with reference sensors and proofs to achieve precise vehicle state estimation results. It is also shown, how the computational effort can be reduced by incorporating the tracking information into a neural network. A discussion on current limitations supplements the findings. By collecting a large number of vehicle trajectories, macroscopic statistics, such as traffic flow and density can be obtained from the data. In the second part, a publicly available drone based data set is analyzed to evaluate the suitability for macroscopic traffic modeling. The results show that the method is well suited for gaining detailed information about macroscopic statistics, such as traffic flow dependent time headway or lane change occurrences. In conclusion, this paper presents methods to exploit the remarkable opportunities of drone based image processing for joint macro- and microscopic traffic analysis.
Cite as

Friedrich Kruber, Eduardo Sánchez Morales, Robin Egolf, Jonas Wurst, Samarjit Chakraborty, and Michael Botsch. Micro- and Macroscopic Road Traffic Analysis using Drone Image Data. In LITES, Volume 8, Issue 1 (2022): Special Issue on Embedded Systems for Computer Vision. Leibniz Transactions on Embedded Systems, Volume 8, Issue 1, pp. 02:1-02:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kruber_et_al:LITES.8.1.2,
  author =	{Kruber, Friedrich and S\'{a}nchez Morales, Eduardo and Egolf, Robin and Wurst, Jonas and Chakraborty, Samarjit and Botsch, Michael},
  title =	{{Micro- and Macroscopic Road Traffic Analysis using Drone Image Data}},
  booktitle =	{LITES, Volume 8, Issue 1 (2022): Special Issue on Embedded Systems for Computer Vision},
  pages =	{02:1--02:27},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{1},
  editor =	{Kruber, Friedrich and S\'{a}nchez Morales, Eduardo and Egolf, Robin and Wurst, Jonas and Chakraborty, Samarjit and Botsch, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.1.2},
  doi =		{10.4230/LITES.8.1.2},
  annote =	{Keywords: traffic data analysis, trajectory data, drone image data}
}
Document
DOI: 10.4230/LIPIcs.TQC.2022.12
Qutrit Metaplectic Gates Are a Subset of Clifford+T

Authors: Andrew N. Glaudell, Neil J. Ross, John van de Wetering, and Lia Yeh

Published in: LIPIcs, Volume 232, 17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022)

Abstract
A popular universal gate set for quantum computing with qubits is Clifford+T, as this can be readily implemented on many fault-tolerant architectures. For qutrits, there is an equivalent T gate, that, like its qubit analogue, makes Clifford+T approximately universal, is injectable by a magic state, and supports magic state distillation. However, it was claimed that a better gate set for qutrits might be Clifford+R, where R = diag(1,1,-1) is the metaplectic gate, as certain protocols and gates could more easily be implemented using the R gate than the T gate. In this paper we show that the qutrit Clifford+R unitaries form a strict subset of the Clifford+T unitaries when we have at least two qutrits. We do this by finding a direct decomposition of R ⊗ 𝕀 as a Clifford+T circuit and proving that the T gate cannot be exactly synthesized in Clifford+R. This shows that in fact the T gate is more expressive than the R gate. Moreover, we additionally show that it is impossible to find a single-qutrit Clifford+T decomposition of the R gate, making our result tight.
Cite as

Andrew N. Glaudell, Neil J. Ross, John van de Wetering, and Lia Yeh. Qutrit Metaplectic Gates Are a Subset of Clifford+T. In 17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 232, pp. 12:1-12:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{glaudell_et_al:LIPIcs.TQC.2022.12,
  author =	{Glaudell, Andrew N. and Ross, Neil J. and van de Wetering, John and Yeh, Lia},
  title =	{{Qutrit Metaplectic Gates Are a Subset of Clifford+T}},
  booktitle =	{17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-237-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{232},
  editor =	{Le Gall, Fran\c{c}ois and Morimae, Tomoyuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2022.12},
  URN =		{urn:nbn:de:0030-drops-165195},
  doi =		{10.4230/LIPIcs.TQC.2022.12},
  annote =	{Keywords: Quantum computation, qutrits, gate synthesis, metaplectic gate, Clifford+T}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2019.2
A Linear Logical Framework in Hybrid (Invited Talk)

Authors: Amy P. Felty

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We present a linear logical framework implemented within the Hybrid system [Amy P. Felty and Alberto Momigliano, 2012]. Hybrid is designed to support the use of higher-order abstract syntax for representing and reasoning about formal systems, implemented in the Coq Proof Assistant. In this work, we extend the system with two linear specification logics, which provide infrastructure for reasoning directly about object languages with linear features. We originally developed this framework in order to address the challenges of reasoning about the type system of a quantum lambda calculus. In particular, we started by considering the Proto-Quipper language [Neil J. Ross, 2015], which contains the core of Quipper [Green et al., 2013; Peter Selinger and Benoît Valiron, 2006]. Quipper is a relatively new quantum programming language under active development with a linear type system. We have completed a formal proof of type soundness for Proto-Quipper [Mohamed Yousri Mahmoud and Amy P. Felty, 2018]. Our current work includes extending this work to other properties of Proto-Quipper, reasoning about other quantum programming languages [Mohamed Yousri Mahmoud and Amy P. Felty, 2018], and reasoning about other languages such as the meta-theory of low-level abstract machine code. We are also interested in applying this framework to applications outside the domain of meta-theory of programming languages and have focused on two areas - formal reasoning about the proof theory of focused linear sequent calculi and modeling biological processes as transition systems and proving properties about them. We found that a slight extension of the initial linear specification logic allowed us to provide succinct encodings and facilitate reasoning in these new domains. We illustrate by discussing a model of breast cancer progression as a set of transition rules and proving properties about this model [Joëlle Despeyroux et al., 2018]. Current work also includes modeling stem cells as they mature into different types of blood cells. This work illustrates the use of Hybrid as a meta-logical framework for fast prototyping of logical frameworks, which is achieved by defining inference rules of a specification logic inductively in Coq and building a library of definitions and lemmas used to reason about a class of object logics. Our focus here is on linear specification logics and their applications.
Cite as

Amy P. Felty. A Linear Logical Framework in Hybrid (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 2:1-2:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{felty:LIPIcs.FSCD.2019.2,
  author =	{Felty, Amy P.},
  title =	{{A Linear Logical Framework in Hybrid}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.2},
  URN =		{urn:nbn:de:0030-drops-105099},
  doi =		{10.4230/LIPIcs.FSCD.2019.2},
  annote =	{Keywords: Logical frameworks, proof assistants, linear logic}
}
  • Refine by Author
  • 1 Botsch, Michael
  • 1 Chakraborty, Samarjit
  • 1 Egolf, Robin
  • 1 Felty, Amy P.
  • 1 Glaudell, Andrew N.
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Machine learning
  • 1 Theory of computation → Functional constructs
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Operational semantics
  • 1 Theory of computation → Quantum computation theory
  • Show More...

  • Refine by Keyword
  • 1 Clifford+T
  • 1 Logical frameworks
  • 1 Quantum computation
  • 1 drone image data
  • 1 gate synthesis
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2022
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact