5 Search Results for "Thierry-Mieg, Nicolas"


Document
Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation

Authors: Paul Kröger and Martin Fränzle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2


Abstract
Hybrid discrete-continuous system dynamics arises when discrete actions, e.g. by a decision algorithm, meet continuous behaviour, e.g. due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes.Various flavours of hybrid automata have been suggested as a means to formally analyse CPS dynamics. In a previous article, we demonstrated that all these variants of hybrid automata provide inaccurate, in the sense of either overly pessimistic or overly optimistic, verdicts for engineered systems operating under imprecise observation of their environment due to, e.g., measurement error. We suggested a revised formal model, called Bayesian hybrid automata, that is able to represent state tracking and estimation in hybrid systems and thereby enhances precision of verdicts obtained from the model in comparison to traditional model variants.In this article, we present an extended definition of Bayesian hybrid automata which incorporates a new class of guard and invariant functions that allow to evaluate traditional guards and invariants over probability distributions. The resulting framework allows to model observers with knowledge about the control strategy of an observed agent but with imprecise estimates of the data on which the control decisions are based.

Cite as

Paul Kröger and Martin Fränzle. Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 05:1-05:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{kroger_et_al:LITES.8.2.5,
  author =	{Kr\"{o}ger, Paul and Fr\"{a}nzle, Martin},
  title =	{{Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation}},
  booktitle =	{LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems},
  pages =	{05:1--05:27},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Kr\"{o}ger, Paul and Fr\"{a}nzle, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.5},
  doi =		{10.4230/LITES.8.2.5},
  annote =	{Keywords: }
}
Document
Gluing for Type Theory

Authors: Ambrus Kaposi, Simon Huber, and Christian Sattler

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


Abstract
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.

Cite as

Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25,
  author =	{Kaposi, Ambrus and Huber, Simon and Sattler, Christian},
  title =	{{Gluing for Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{25:1--25:19},
  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.25},
  URN =		{urn:nbn:de:0030-drops-105323},
  doi =		{10.4230/LIPIcs.FSCD.2019.25},
  annote =	{Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive types}
}
Document
Modeling Power Consumption and Temperature in TLM Models

Authors: Matthieu Moy, Claude Helmstetter, Tayeb Bouhadiba, and Florence Maraninchi

Published in: LITES, Volume 3, Issue 1 (2016). Leibniz Transactions on Embedded Systems, Volume 3, Issue 1


Abstract
Many techniques and tools exist to estimate the power consumption and the temperature map of a chip. These tools help the hardware designers develop power efficient chips in the presence of temperature constraints. For this task, the application can be ignored or at least abstracted by some high level scenarios; at this stage, the actual embedded software is generally not available yet.However, after the hardware is defined, the embedded software can still have a significant influence on the power consumption; i.e., two implementations of the same application can consume more or less power. Moreover, the actual software power manager ensuring the temperature constraints, usually by acting dynamically on the voltage and frequency, must itself be validated. Validating such power management policy requires a model of both actuators and sensors, hence a closed-loop simulation of the functional model with a non-functional one.In this paper, we present and compare several tools to simulate the power and thermal behavior of a chip together with its functionality. We explore several levels of abstraction and study the impact on the precision of the analysis.

Cite as

Matthieu Moy, Claude Helmstetter, Tayeb Bouhadiba, and Florence Maraninchi. Modeling Power Consumption and Temperature in TLM Models. In LITES, Volume 3, Issue 1 (2016). Leibniz Transactions on Embedded Systems, Volume 3, Issue 1, pp. 03:1-03:29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{moy_et_al:LITES-v003-i001-a003,
  author =	{Moy, Matthieu and Helmstetter, Claude and Bouhadiba, Tayeb and Maraninchi, Florence},
  title =	{{Modeling Power Consumption and Temperature in TLM Models}},
  booktitle =	{LITES, Volume 3, Issue 1 (2016)},
  pages =	{03:1--03:29},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2016},
  volume =	{3},
  number =	{1},
  editor =	{Moy, Matthieu and Helmstetter, Claude and Bouhadiba, Tayeb and Maraninchi, Florence},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v003-i001-a003},
  doi =		{10.4230/LITES-v003-i001-a003},
  annote =	{Keywords: Power consumption, Temperature control, Virtual prototype, SystemC, Transactional modeling}
}
Document
Quantum key distribution and cryptography: a survey

Authors: Romain Alléaume, Norbert Lütkenhaus, Renato Renner, Philippe Grangier, Thierry Debuisschert, Gregoire Ribordy, Nicolas Gisin, Philippe Painchault, Thomas Pornin, Louis Slavail, Michel Riguidel, Andrew Shilds, Thomas Länger, Momtchil Peev, Mehrdad Dianati, Anthony Leverrier, Andreas Poppe, Jan Bouda, Cyril Branciard, Mark Godfrey, John Rarity, Harald Weinfurter, Anton Zeilinger, and Christian Monyk

Published in: Dagstuhl Seminar Proceedings, Volume 9311, Classical and Quantum Information Assurance Foundations and Practice (2010)


Abstract
I will try to partially answer, based on a review on recent work, the following question: Can QKD and more generally quantum information be useful to cover some practical security requirements in current (and future) IT infrastructures ? I will in particular cover the following topics - practical performances of QKD - QKD network deployment - SECOQC project - Capabilities of QKD as a cryptographic primitive - comparative advantage with other solution, in order to cover practical security requirements - Quantum information and Side-channels - QKD security assurance - Thoughts about "real" Post-Quantum Cryptography

Cite as

Romain Alléaume, Norbert Lütkenhaus, Renato Renner, Philippe Grangier, Thierry Debuisschert, Gregoire Ribordy, Nicolas Gisin, Philippe Painchault, Thomas Pornin, Louis Slavail, Michel Riguidel, Andrew Shilds, Thomas Länger, Momtchil Peev, Mehrdad Dianati, Anthony Leverrier, Andreas Poppe, Jan Bouda, Cyril Branciard, Mark Godfrey, John Rarity, Harald Weinfurter, Anton Zeilinger, and Christian Monyk. Quantum key distribution and cryptography: a survey. In Classical and Quantum Information Assurance Foundations and Practice. Dagstuhl Seminar Proceedings, Volume 9311, pp. 1-29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{alleaume_et_al:DagSemProc.09311.3,
  author =	{All\'{e}aume, Romain and L\"{u}tkenhaus, Norbert and Renner, Renato and Grangier, Philippe and Debuisschert, Thierry and Ribordy, Gregoire and Gisin, Nicolas and Painchault, Philippe and Pornin, Thomas and Slavail, Louis and Riguidel, Michel and Shilds, Andrew and L\"{a}nger, Thomas and Peev, Momtchil and Dianati, Mehrdad and Leverrier, Anthony and Poppe, Andreas and Bouda, Jan and Branciard, Cyril and Godfrey, Mark and Rarity, John and Weinfurter, Harald and Zeilinger, Anton and Monyk, Christian},
  title =	{{Quantum key distribution and cryptography: a survey}},
  booktitle =	{Classical and Quantum Information Assurance Foundations and Practice},
  pages =	{1--29},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9311},
  editor =	{Samual L. Braunstein and Hoi-Kwong Lo and Kenny Paterson and Peter Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09311.3},
  URN =		{urn:nbn:de:0030-drops-23618},
  doi =		{10.4230/DagSemProc.09311.3},
  annote =	{Keywords: QKD, QKD networks, Security assurance, Post-Quantum Cryptography}
}
Document
08301 Final Report – Group Testing in the Life Sciences

Authors: Alexander Schliep, Nicolas Thierry-Mieg, and Amin Shokrollahi

Published in: Dagstuhl Seminar Proceedings, Volume 8301, Group Testing in the Life Sciences (2008)


Abstract
Group testing AKA smart-pooling is a general strategy for minimizing the number of tests necessary for identifying positives among a large collection of items. It has the potential to efficiently identify and correct for experimental errors (false–positives and false–negatives). It can be used whenever tests can detect the presence of a positive in a group (or pool) of items, provided that positives are rare. Group testing has numerous applications in the life sciences, such as physical mapping, interactome mapping, drug–resistance screening, or designing DNA-microarrays, and many connections to computer science, mathematics and communications, from error-correcting codes to combinatorial design theory and to statistics. The seminar brought together researchers representing the different communities working on group testing and experimentalists from the life sciences. The desired outcome of the seminar was a better understanding of the requirements for and the possibilities of group testing in the life sciences.

Cite as

Alexander Schliep, Nicolas Thierry-Mieg, and Amin Shokrollahi. 08301 Final Report – Group Testing in the Life Sciences. In Group Testing in the Life Sciences. Dagstuhl Seminar Proceedings, Volume 8301, pp. 1-8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{schliep_et_al:DagSemProc.08301.1,
  author =	{Schliep, Alexander and Thierry-Mieg, Nicolas and Shokrollahi, Amin},
  title =	{{08301 Final Report – Group Testing in the Life Sciences}},
  booktitle =	{Group Testing in the Life Sciences},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8301},
  editor =	{Alexander Schliep and Amin Shokrollahi and Nicolas Thierry-Mieg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08301.1},
  URN =		{urn:nbn:de:0030-drops-17806},
  doi =		{10.4230/DagSemProc.08301.1},
  annote =	{Keywords: Group Testing, Pooling, Combinatorics, Design Theory, Error correcting}
}
  • Refine by Author
  • 1 Alléaume, Romain
  • 1 Bouda, Jan
  • 1 Bouhadiba, Tayeb
  • 1 Branciard, Cyril
  • 1 Debuisschert, Thierry
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Embedded and cyber-physical systems
  • 1 Hardware → Chip-level power issues
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Combinatorics
  • 1 Design Theory
  • 1 Error correcting
  • 1 Group Testing
  • 1 Martin-Löf type theory
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 1 2008
  • 1 2010
  • 1 2016
  • 1 2019
  • 1 2022

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