16 Search Results for "Laurent, Thomas"

Document
DOI: 10.4230/LITES.8.2.3
Higher-Dimensional Timed and Hybrid Automata

Authors: Uli Fahrenberg

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

Abstract
We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata.The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.
Cite as

Uli Fahrenberg. Higher-Dimensional Timed and Hybrid Automata. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 03:1-03:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{fahrenberg:LITES.8.2.3,
  author =	{Fahrenberg, Uli},
  title =	{{Higher-Dimensional Timed and Hybrid Automata}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:16},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.3},
  doi =		{10.4230/LITES.8.2.3},
  annote =	{Keywords: timed automaton, higher-dimensional automaton, precubical set, real time, non-interleaving concurrency, hybrid automaton}
}
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}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:27},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{1},
  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.CP.2021.33
Learning TSP Requires Rethinking Generalization

Authors: Chaitanya K. Joshi, Quentin Cappart, Louis-Martin Rousseau, and Thomas Laurent

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
End-to-end training of neural network solvers for combinatorial optimization problems such as the Travelling Salesman Problem is intractable and inefficient beyond a few hundreds of nodes. While state-of-the-art Machine Learning approaches perform closely to classical solvers when trained on trivially small sizes, they are unable to generalize the learnt policy to larger instances of practical scales. Towards leveraging transfer learning to solve large-scale TSPs, this paper identifies inductive biases, model architectures and learning algorithms that promote generalization to instances larger than those seen in training. Our controlled experiments provide the first principled investigation into such zero-shot generalization, revealing that extrapolating beyond training data requires rethinking the neural combinatorial optimization pipeline, from network layers and learning paradigms to evaluation protocols.
Cite as

Chaitanya K. Joshi, Quentin Cappart, Louis-Martin Rousseau, and Thomas Laurent. Learning TSP Requires Rethinking Generalization. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 33:1-33:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{joshi_et_al:LIPIcs.CP.2021.33,
  author =	{Joshi, Chaitanya K. and Cappart, Quentin and Rousseau, Louis-Martin and Laurent, Thomas},
  title =	{{Learning TSP Requires Rethinking Generalization}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.33},
  URN =		{urn:nbn:de:0030-drops-153248},
  doi =		{10.4230/LIPIcs.CP.2021.33},
  annote =	{Keywords: Combinatorial Optimization, Travelling Salesman Problem, Graph Neural Networks, Deep Learning}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.143
Analytical Differential Calculus with Integration

Authors: Han Xu and Zhenjiang Hu

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
Differential lambda-calculus was first introduced by Thomas Ehrhard and Laurent Regnier in 2003. Despite more than 15 years of history, little work has been done on a differential calculus with integration. In this paper, we shall propose a differential calculus with integration from a programming point of view. We show its good correspondence with mathematics, which is manifested by how we construct these reduction rules and how we preserve important mathematical theorems in our calculus. Moreover, we highlight applications of the calculus in incremental computation, automatic differentiation, and computation approximation.
Cite as

Han Xu and Zhenjiang Hu. Analytical Differential Calculus with Integration. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 143:1-143:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{xu_et_al:LIPIcs.ICALP.2021.143,
  author =	{Xu, Han and Hu, Zhenjiang},
  title =	{{Analytical Differential Calculus with Integration}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{143:1--143:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.143},
  URN =		{urn:nbn:de:0030-drops-142127},
  doi =		{10.4230/LIPIcs.ICALP.2021.143},
  annote =	{Keywords: Differential Calculus, Integration, Lambda Calculus, Incremental Computation, Adaptive Computing}
}
Document
DOI: 10.4230/LIPIcs.CCC.2020.7
Quantum Lower Bounds for Approximate Counting via Laurent Polynomials

Authors: Scott Aaronson, Robin Kothari, William Kretschmer, and Justin Thaler

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)

Abstract
We study quantum algorithms that are given access to trusted and untrusted quantum witnesses. We establish strong limitations of such algorithms, via new techniques based on Laurent polynomials (i.e., polynomials with positive and negative integer exponents). Specifically, we resolve the complexity of approximate counting, the problem of multiplicatively estimating the size of a nonempty set S ⊆ [N], in two natural generalizations of quantum query complexity. Our first result holds in the standard Quantum Merlin - Arthur (QMA) setting, in which a quantum algorithm receives an untrusted quantum witness. We show that, if the algorithm makes T quantum queries to S, and also receives an (untrusted) m-qubit quantum witness, then either m = Ω(|S|) or T = Ω(√{N/|S|}). This is optimal, matching the straightforward protocols where the witness is either empty, or specifies all the elements of S. As a corollary, this resolves the open problem of giving an oracle separation between SBP, the complexity class that captures approximate counting, and QMA. In our second result, we ask what if, in addition to a membership oracle for S, a quantum algorithm is also given "QSamples" - i.e., copies of the state |S⟩ = 1/√|S| ∑_{i ∈ S} |i⟩ - or even access to a unitary transformation that enables QSampling? We show that, even then, the algorithm needs either Θ(√{N/|S|}) queries or else Θ(min{|S|^{1/3},√{N/|S|}}) QSamples or accesses to the unitary. Our lower bounds in both settings make essential use of Laurent polynomials, but in different ways.
Cite as

Scott Aaronson, Robin Kothari, William Kretschmer, and Justin Thaler. Quantum Lower Bounds for Approximate Counting via Laurent Polynomials. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 7:1-7:47, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aaronson_et_al:LIPIcs.CCC.2020.7,
  author =	{Aaronson, Scott and Kothari, Robin and Kretschmer, William and Thaler, Justin},
  title =	{{Quantum Lower Bounds for Approximate Counting via Laurent Polynomials}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{7:1--7:47},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.7},
  URN =		{urn:nbn:de:0030-drops-125593},
  doi =		{10.4230/LIPIcs.CCC.2020.7},
  annote =	{Keywords: Approximate counting, Laurent polynomials, QSampling, query complexity}
}
Document
DOI: 10.4230/LITES-v006-i001-a001
Local Planning Semantics: A Semantics for Distributed Real-Time Systems

Authors: Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga

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

Abstract
Design, implementation and verification of distributed real-time systems are acknowledged to be very hard tasks. Such systems are prone to different kinds of delay, such as execution time of actions or communication delays implied by distributed platforms. The latter increase considerably the complexity of coordinating the parallel activities of running components. Scheduling such systems must cope with those delays by proposing execution strategies  ensuring global consistency while satisfying the imposed timing constraints. In this paper, we investigate a formal model for such systems as compositions of timed automata subject to multiparty interactions, and propose a semantics aiming to overcome the communication delays problem through anticipating the execution of interactions. To be effective in a distributed context, scheduling an interaction should rely on (as much as possible) local information only, namely the state of its participating components. However, as shown in this paper these information is not always sufficient and does not guarantee a safe execution of the system as it may introduce deadlocks. Moreover, delays may also affect the satisfaction of timing constraints, which also corresponds to deadlocks in the former model. Thus, we also explore methods for analyzing such deadlock situations and for computing  deadlock-free scheduling strategies when possible.
Cite as

Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga. Local Planning Semantics: A Semantics for Distributed Real-Time Systems. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 01:1-01:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{dellabani_et_al:LITES-v006-i001-a001,
  author =	{Dellabani, Mahieddine and Combaz, Jacques and Bensalem, Saddek and Bozga, Marius},
  title =	{{Local Planning Semantics: A Semantics for Distributed Real-Time Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:27},
  ISSN =	{2199-2002},
  year =	{2019},
  volume =	{6},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v006-i001-a001},
  doi =		{10.4230/LITES-v006-i001-a001},
  annote =	{Keywords: Distributed Real-Time Systems, Timed Automata, Formal Verification}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.20
Dynamic Purpose Decomposition of Mobility Flows Based on Geographical Data

Authors: Etienne Thuillier, Laurent Moalic, and Alexandre Caminada

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
Spatial and temporal decomposition of aggregated mobility flows is nowadays a commonly addressed issue, but a trip-purpose decomposition of mobility flows is a more challenging topic, which requires more sensitive analysis such as heterogeneous data fusion. In this paper, we study the relation between land use and mobility purposes. We propose a model that dynamically decomposes mobility flows into six mobility purposes. To this end, we use a national transportation database that surveyed more than 35,000 individuals and a national ground description database that identifies six distinct ground types. Based on these two types of data, we dynamically solve several overdetermined systems of linear equations from a training set and we infer the travel purposes. Our experimental results demonstrate that our model effectively predicts the purposes of mobility from the land use. Furthermore, our model shows great results compared with a reference supervised learning decomposition.
Cite as

Etienne Thuillier, Laurent Moalic, and Alexandre Caminada. Dynamic Purpose Decomposition of Mobility Flows Based on Geographical Data. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 20:1-20:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{thuillier_et_al:LIPIcs.TIME.2017.20,
  author =	{Thuillier, Etienne and Moalic, Laurent and Caminada, Alexandre},
  title =	{{Dynamic Purpose Decomposition of Mobility Flows Based on Geographical Data}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{20:1--20:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.20},
  URN =		{urn:nbn:de:0030-drops-79221},
  doi =		{10.4230/LIPIcs.TIME.2017.20},
  annote =	{Keywords: Human mobility, Purpose decomposition, Information extraction, Linear model}
}
Document
DOI: 10.4230/LITES-v003-i001-a003
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}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:29},
  ISSN =	{2199-2002},
  year =	{2016},
  volume =	{3},
  number =	{1},
  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
DOI: 10.4230/LITES-v003-i001-a005
A Survey on Static Cache Analysis for Real-Time Systems

Authors: Mingsong Lv, Nan Guan, Jan Reineke, Reinhard Wilhelm, and Wang Yi

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

Abstract
Real-time systems are reactive computer systems that must produce their reaction to a stimulus within given time bounds. A vital verification requirement is to estimate the Worst-Case Execution Time (WCET) of programs. These estimates are then used to predict the timing behavior of the overall system. The execution time of a program heavily depends on the underlying hardware, among which cache has the biggest influence. Analyzing cache behavior is very challenging due to the versatile cache features and complex execution environment. This article provides a survey on static cache analysis for real-time systems. We first present the challenges and static analysis techniques for independent programs with respect to different cache features. Then, the discussion is extended to cache analysis in complex execution environment, followed by a survey of existing tools based on static techniques for cache analysis. An outlook for future research is provided at last.
Cite as

Mingsong Lv, Nan Guan, Jan Reineke, Reinhard Wilhelm, and Wang Yi. A Survey on Static Cache Analysis for Real-Time Systems. In LITES, Volume 3, Issue 1 (2016). Leibniz Transactions on Embedded Systems, Volume 3, Issue 1, pp. 05:1-05:48, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{lv_et_al:LITES-v003-i001-a005,
  author =	{Lv, Mingsong and Guan, Nan and Reineke, Jan and Wilhelm, Reinhard and Yi, Wang},
  title =	{{A Survey on Static Cache Analysis for Real-Time Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{05:1--05:48},
  ISSN =	{2199-2002},
  year =	{2016},
  volume =	{3},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v003-i001-a005},
  doi =		{10.4230/LITES-v003-i001-a005},
  annote =	{Keywords: Hard real-time, Cache analysis, Worst-case execution time}
}
Document
DOI: 10.4230/LITES-v002-i002-a001
From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation

Authors: Thomas Carle, Dumitru Potop-Butucaru, Yves Sorel, and David Lesens

Published in: LITES, Volume 2, Issue 2 (2015). Leibniz Transactions on Embedded Systems, Volume 2, Issue 2

Abstract
Our objective is to facilitate the development of complex time-triggered systems by automating the allocation and scheduling steps. We show that full automation is possible while taking into account the elements of complexity needed by a complex embedded control system. More precisely, we consider deterministic functional specifications provided (as often in an industrial setting) by means of synchronous data-flow models with multiple modes and multiple relative periods. We first extend this functional model with an original real-time characterization that takes advantage of our time-triggered framework to provide a simpler representation of complex end-to-end flow requirements. We also extend our specifications with additional non-functional properties specifying partitioning, allocation, and preemptability constraints. Then, we provide novel algorithms for the off-line scheduling of these extended specifications onto partitioned time-triggered architectures à la ARINC 653. The main originality of our work is that it takes into account at the same time multiple complexity elements: various types of non-functional properties (real-time, partitioning, allocation, preemptability) and functional specifications with conditional execution and multiple modes. Allocation of time slots/windows to partitions can be fully or partially provided, or synthesized by our tool. Our algorithms allow the automatic allocation and scheduling onto multi-processor (distributed) systems with a global time base, taking into account communication costs. We demonstrate our technique on a model of space flight software system with strong real-time determinism requirements.
Cite as

Thomas Carle, Dumitru Potop-Butucaru, Yves Sorel, and David Lesens. From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation. In LITES, Volume 2, Issue 2 (2015). Leibniz Transactions on Embedded Systems, Volume 2, Issue 2, pp. 01:1-01:30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{carle_et_al:LITES-v002-i002-a001,
  author =	{Carle, Thomas and Potop-Butucaru, Dumitru and Sorel, Yves and Lesens, David},
  title =	{{From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:30},
  ISSN =	{2199-2002},
  year =	{2015},
  volume =	{2},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v002-i002-a001},
  doi =		{10.4230/LITES-v002-i002-a001},
  annote =	{Keywords: Time-triggered, Off-line real-time scheduling, Temporal partitioning}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.582
On Classical PCF, Linear Logic and the MIX Rule

Authors: Shahin Amini and Thomas Erhard

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We study a classical version of PCF from a semantical point of view. We define a general notion of model based on categorical models of Linear Logic, in the spirit of earlier work by Girard, Regnier and Laurent. We give a concrete example based on the relational model of Linear Logic, that we present as a non-idempotents intersection type system, and we prove an Adequacy Theorem using ideas introduced by Krivine. Following Danos and Krivine, we also consider an extension of this language with a MIX construction introducing a form of must non-determinism; in this language, a program of type integer can have more than one value (or no value at all, raising an error). We propose a refinement of the relational model of classical PCF in which programs of type integer are single valued; this model rejects the MIX syntactical constructs (and the MIX rule of Linear Logic).
Cite as

Shahin Amini and Thomas Erhard. On Classical PCF, Linear Logic and the MIX Rule. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 582-596, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{amini_et_al:LIPIcs.CSL.2015.582,
  author =	{Amini, Shahin and Erhard, Thomas},
  title =	{{On Classical PCF, Linear Logic and the MIX Rule}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{582--596},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.582},
  URN =		{urn:nbn:de:0030-drops-54402},
  doi =		{10.4230/LIPIcs.CSL.2015.582},
  annote =	{Keywords: lambda-calculus, linear logic, classical logic, denotational semantics}
}
Document
DOI: 10.4230/LITES-v001-i002-a001
Blocking Optimality in Distributed Real-Time Locking Protocols

Authors: Björn Bernhard Brandenburg

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

Abstract
Lower and upper bounds on the maximum priority inversion blocking (pi-blocking) that is generally unavoidable in distributed multiprocessor real-time locking protocols (where resources may be accessed only from specific synchronization processors) are established. Prior work on suspension-based shared-memory multiprocessor locking protocols (which require resources to be accessible from all processors) has established asymptotically tight bounds of Ω(m) and Ω(n) maximum pi-blocking under suspension-oblivious and suspension-aware analysis, respectively, where m denotes the total number of processors and n denotes the number of tasks. In this paper, it is shown that, in the case of distributed semaphore protocols, there exist two different task allocation scenarios that give rise to distinct lower bounds. In the case of co-hosted task allocation, where application tasks may also be assigned to synchronization processors (i.e., processors hosting critical sections), Ω(Φ · n) maximum pi-blocking is unavoidable for some tasks under any locking protocol under both suspension-aware and suspension-oblivious schedulability analysis, where Φ denotes the ratio of the maximum response time to the shortest period. In contrast, in the case of disjoint task allocation (i.e., if application tasks may not be assigned to synchronization processors), only Ω(m) and Ω(n) maximum pi-blocking is fundamentally unavoidable under suspension-oblivious and suspension-aware analysis, respectively, as in the shared-memory case. These bounds are shown to be asymptotically tight with the construction of two new distributed real-time locking protocols that ensure O(m) and O(n) maximum pi-blocking under suspension-oblivious and suspension-aware analysis, respectively.
Cite as

Björn Bernhard Brandenburg. Blocking Optimality in Distributed Real-Time Locking Protocols. In LITES, Volume 1, Issue 2 (2014). Leibniz Transactions on Embedded Systems, Volume 1, Issue 2, pp. 01:1-01:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{brandenburg:LITES-v001-i002-a001,
  author =	{Brandenburg, Bj\"{o}rn Bernhard},
  title =	{{Blocking Optimality in Distributed Real-Time Locking Protocols}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:22},
  ISSN =	{2199-2002},
  year =	{2014},
  volume =	{1},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v001-i002-a001},
  doi =		{10.4230/LITES-v001-i002-a001},
  annote =	{Keywords: Distributed multiprocessor real-time systems, Real-time locking, Priority inversion, Blocking optimality}
}
Document
DOI: 10.4230/LIPIcs.STACS.2012.543
The Denjoy alternative for computable functions

Authors: Laurent Bienvenu, Rupert Hölzl, Joseph S. Miller, and André Nies

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Abstract
The Denjoy-Young-Saks Theorem from classical analysis states that for an arbitrary function f:R->R, the Denjoy alternative holds outside a null set, i.e., for almost every real x, either the derivative of f exists at x, or the derivative fails to exist in the worst possible way: the limit superior of the slopes around x equals +infinity, and the limit inferior -infinity. Algorithmic randomness allows us to define randomness notions giving rise to different concepts of almost everywhere. It is then natural to wonder which of these concepts corresponds to the almost everywhere notion appearing in the Denjoy-Young-Saks theorem. To answer this question Demuth investigated effective versions of the theorem and proved that Demuth randomness is strong enough to ensure the Denjoy alternative for Markov computable functions. In this paper, we show that the set of these points is indeed strictly bigger than the set of Demuth random reals - showing that Demuth's sufficient condition was too strong - and moreover is incomparable with Martin-Löf randomness; meaning in particular that it does not correspond to any known set of random reals. To prove these two theorems, we study density-type theorems, such as the Lebesgue density theorem and obtain results of independent interest. We show for example that the classical notion of Lebesgue density can be characterized by the only very recently defined notion of difference randomness. This is to our knowledge the first analytical characterization of difference randomness. We also consider the concept of porous points, a special type of Lebesgue nondensity points that are well-behaved in the sense that the "density holes" around the point are continuous intervals whose length follows a certain systematic rule. An essential part of our proof will be to argue that porous points of effectively closed classes can never be difference random.
Cite as

Laurent Bienvenu, Rupert Hölzl, Joseph S. Miller, and André Nies. The Denjoy alternative for computable functions. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 543-554, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bienvenu_et_al:LIPIcs.STACS.2012.543,
  author =	{Bienvenu, Laurent and H\"{o}lzl, Rupert and Miller, Joseph S. and Nies, Andr\'{e}},
  title =	{{The Denjoy alternative for computable functions}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{543--554},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.543},
  URN =		{urn:nbn:de:0030-drops-34095},
  doi =		{10.4230/LIPIcs.STACS.2012.543},
  annote =	{Keywords: Differentiability, Denjoy alternative, density, porosity, randomness}
}
Document
DOI: 10.4230/LIPIcs.STACS.2011.452
Solovay functions and K-triviality

Authors: Laurent Bienvenu, Wolfgang Merkle, and Andre Nies

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

Abstract
As part of his groundbreaking work on algorithmic randomness, Solovay demonstrated in the 1970s the remarkable fact that there are computable upper bounds of prefix-free Kolmogorov complexity $K$ that are tight on infinitely many values (up to an additive constant). Such computable upper bounds are called Solovay functions. Recent work of Bienvenu and Downey~[STACS 2009, LIPIcs 3, pp 147-158] indicates that Solovay functions are deeply connected with central concepts of algorithmic randomness such as $Omega$ numbers, K-triviality, and Martin-Loef randomness. In what follows, among other results we answer two open problems posed by Bienvenu and Downey about the definition of $K$-triviality and about the Gacs-Miller-Yu characterization of Martin-Loef randomness. The former defines a sequence A to be K-trivial if K(A|n) <=^+ K(n), the latter asserts that a sequence A is Martin-Loef random iff C(A|n) >=^+ n-K(n). So both involve the noncomputable function K. As our main results we show that in both cases K(n) can be equivalently replaced by any Solovay function, and, what is more, that among all computable functions such a replacement is possible exactly for the Solovay functions. Moreover, similar statements hold for the larger class of all right-c.e. in place of the computable functions. These full characterizations, besides having significant theoretical interest on their own, will be useful as tools when working with K-trivial and Martin-Loef random sequences.
Cite as

Laurent Bienvenu, Wolfgang Merkle, and Andre Nies. Solovay functions and K-triviality. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 452-463, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bienvenu_et_al:LIPIcs.STACS.2011.452,
  author =	{Bienvenu, Laurent and Merkle, Wolfgang and Nies, Andre},
  title =	{{Solovay functions and K-triviality}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
  pages =	{452--463},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.452},
  URN =		{urn:nbn:de:0030-drops-30345},
  doi =		{10.4230/LIPIcs.STACS.2011.452},
  annote =	{Keywords: Algorithmic randomness, Kolmogorov complexity, K-triviality}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.505
Generalized Mean-payoff and Energy Games

Authors: Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Generalized mean-payoff and energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of generalized energy games and show the inter-reducibility of generalized mean-payoff and energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete.
Cite as

Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 505-516, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.FSTTCS.2010.505,
  author =	{Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Generalized Mean-payoff and Energy Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{505--516},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.505},
  URN =		{urn:nbn:de:0030-drops-28484},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.505},
  annote =	{Keywords: mean-payoff games, energy games, finite memory strategies, determinacy}
}
  • Refine by Author
  • 2 Bienvenu, Laurent
  • 1 Aaronson, Scott
  • 1 Amini, Shahin
  • 1 Bensalem, Saddek
  • 1 Botsch, Michael
  • Show More...

  • Refine by Classification
  • 2 Computer systems organization → Real-time systems
  • 1 Computer systems organization
  • 1 Computing methodologies → Machine learning
  • 1 Computing methodologies → Neural networks
  • 1 General and reference → Surveys and overviews
  • Show More...

  • Refine by Keyword
  • 2 Information extraction
  • 1 Adaptive Computing
  • 1 Algorithmic randomness
  • 1 Approximate counting
  • 1 Blocking optimality
  • Show More...

  • Refine by Type
  • 16 document

  • Refine by Publication Year
  • 2 2015
  • 2 2016
  • 2 2021
  • 2 2022
  • 1 2005
  • Show More...

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