17 Search Results for "Stephan, Frank"


Document
Swarms of Mobile Robots: Towards Versatility with Safety

Authors: Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain

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 present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.

Cite as

Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{courtieu_et_al:LITES.8.2.2,
  author =	{Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
  title =	{{Swarms of Mobile Robots: Towards Versatility with Safety}},
  booktitle =	{LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems},
  pages =	{02:1--02:36},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.2},
  doi =		{10.4230/LITES.8.2.2},
  annote =	{Keywords: distributed algorithm, mobile autonomous robots, formal proof}
}
Document
Randomness and Initial Segment Complexity for Probability Measures

Authors: André Nies and Frank Stephan

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)


Abstract
We study algorithmic randomness properties for probability measures on Cantor space. We say that a measure μ on the space of infinite bit sequences is Martin-Löf absolutely continuous if the non-Martin-Löf random bit sequences form a null set with respect to μ. We think of this as a weak randomness notion for measures. We begin with examples, and a robustness property related to Solovay tests. Our main work connects our property to the growth of the initial segment complexity for measures μ; the latter is defined as a μ-average over the complexity of strings of the same length. We show that a maximal growth implies our weak randomness property, but also that both implications of the Levin-Schnorr theorem fail. We briefly discuss K-triviality for measures, which means that the growth of initial segment complexity is as slow as possible. We show that full Martin-Löf randomness of a measure implies Martin-Löf absolute continuity; the converse fails because only the latter property is compatible with having atoms. In a final section we consider weak randomness relative to a general ergodic computable measure. We seek appropriate effective versions of the Shannon-McMillan-Breiman theorem and the Brudno theorem where the bit sequences are replaced by measures.

Cite as

André Nies and Frank Stephan. Randomness and Initial Segment Complexity for Probability Measures. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 55:1-55:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{nies_et_al:LIPIcs.STACS.2020.55,
  author =	{Nies, Andr\'{e} and Stephan, Frank},
  title =	{{Randomness and Initial Segment Complexity for Probability Measures}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{55:1--55:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.55},
  URN =		{urn:nbn:de:0030-drops-119168},
  doi =		{10.4230/LIPIcs.STACS.2020.55},
  annote =	{Keywords: algorithmic randomness, probability measure on Cantor space, Kolmogorov complexity, statistical superposition, quantum states}
}
Document
A Fast Exponential Time Algorithm for Max Hamming Distance X3SAT

Authors: Gordon Hoi, Sanjay Jain, and Frank Stephan

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)


Abstract
X3SAT is the problem of whether one can satisfy a given set of clauses with up to three literals such that in every clause, exactly one literal is true and the others are false. A related question is to determine the maximal Hamming distance between two solutions of the instance. Dahllöf provided an algorithm for Maximum Hamming Distance XSAT, which is more complicated than the same problem for X3SAT, with a runtime of O(1.8348^n); Fu, Zhou and Yin considered Maximum Hamming Distance for X3SAT and found for this problem an algorithm with runtime O(1.6760^n). In this paper, we propose an algorithm in O(1.3298^n) time to solve the Max Hamming Distance X3SAT problem; the algorithm actually counts for each k the number of pairs of solutions which have Hamming Distance k.

Cite as

Gordon Hoi, Sanjay Jain, and Frank Stephan. A Fast Exponential Time Algorithm for Max Hamming Distance X3SAT. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 17:1-17:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{hoi_et_al:LIPIcs.FSTTCS.2019.17,
  author =	{Hoi, Gordon and Jain, Sanjay and Stephan, Frank},
  title =	{{A Fast Exponential Time Algorithm for Max Hamming Distance X3SAT}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{17:1--17:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.17},
  URN =		{urn:nbn:de:0030-drops-115799},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.17},
  annote =	{Keywords: X3SAT Problem, Maximum Hamming Distance of Solutions, Exponential Time Algorithms, DPLL Algorithms}
}
Document
Measure and Conquer for Max Hamming Distance XSAT

Authors: Gordon Hoi and Frank Stephan

Published in: LIPIcs, Volume 149, 30th International Symposium on Algorithms and Computation (ISAAC 2019)


Abstract
XSAT is defined as the following: Given a propositional formula in conjunctive normal form, can one find an assignment to variables such that there is exactly only 1 literal that is true in every clause, while the other literals are false. The decision problem XSAT is known to be NP-complete. Crescenzi and Rossi [Pierluigi Crescenzi and Gianluca Rossi, 2002] introduced the variant where one searches for a pair of two solutions of an X3SAT instance with maximal Hamming Distance among them, that is, one wants to identify the largest number k such that there are two solutions of the instance with Hamming Distance k. Dahllöf [Vilhelm Dahllöf, 2005; Vilhelm Dahllöf, 2006] provided an algorithm using branch and bound method for Max Hamming Distance XSAT in O(1.8348^n); Fu, Zhou and Yin [Linlu Fu and Minghao Yin, 2012] worked on a more specific problem, the Max Hamming Distance X3SAT, and found for this problem an algorithm with runtime O(1.6760^n). In this paper, we propose an exact exponential algorithm to solve the Max Hamming Distance XSAT problem in O(1.4983^n) time. Like all of them, we will use the branch and bound technique alongside a newly defined measure to improve the analysis of the algorithm.

Cite as

Gordon Hoi and Frank Stephan. Measure and Conquer for Max Hamming Distance XSAT. In 30th International Symposium on Algorithms and Computation (ISAAC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 149, pp. 15:1-15:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{hoi_et_al:LIPIcs.ISAAC.2019.15,
  author =	{Hoi, Gordon and Stephan, Frank},
  title =	{{Measure and Conquer for Max Hamming Distance XSAT}},
  booktitle =	{30th International Symposium on Algorithms and Computation (ISAAC 2019)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-130-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{149},
  editor =	{Lu, Pinyan and Zhang, Guochuan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2019.15},
  URN =		{urn:nbn:de:0030-drops-115119},
  doi =		{10.4230/LIPIcs.ISAAC.2019.15},
  annote =	{Keywords: XSAT, Measure and Conquer, DPLL, Exponential Time Algorithms}
}
Document
Random Subgroups of Rationals

Authors: Ziyuan Gao, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, Alexander Melnikov, Karen Seidel, and Frank Stephan

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
This paper introduces and studies a notion of algorithmic randomness for subgroups of rationals. Given a randomly generated additive subgroup (G,+) of rationals, two main questions are addressed: first, what are the model-theoretic and recursion-theoretic properties of (G,+); second, what learnability properties can one extract from G and its subclass of finitely generated subgroups? For the first question, it is shown that the theory of (G,+) coincides with that of the additive group of integers and is therefore decidable; furthermore, while the word problem for G with respect to any generating sequence for G is not even semi-decidable, one can build a generating sequence beta such that the word problem for G with respect to beta is co-recursively enumerable (assuming that the set of generators of G is limit-recursive). In regard to the second question, it is proven that there is a generating sequence beta for G such that every non-trivial finitely generated subgroup of G is recursively enumerable and the class of all such subgroups of G is behaviourally correctly learnable, that is, every non-trivial finitely generated subgroup can be semantically identified in the limit (again assuming that the set of generators of G is limit-recursive). On the other hand, the class of non-trivial finitely generated subgroups of G cannot be syntactically identified in the limit with respect to any generating sequence for G. The present work thus contributes to a recent line of research studying algorithmically random infinite structures and uncovers an interesting connection between the arithmetical complexity of the set of generators of a randomly generated subgroup of rationals and the learnability of its finitely generated subgroups.

Cite as

Ziyuan Gao, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, Alexander Melnikov, Karen Seidel, and Frank Stephan. Random Subgroups of Rationals. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 25:1-25:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gao_et_al:LIPIcs.MFCS.2019.25,
  author =	{Gao, Ziyuan and Jain, Sanjay and Khoussainov, Bakhadyr and Li, Wei and Melnikov, Alexander and Seidel, Karen and Stephan, Frank},
  title =	{{Random Subgroups of Rationals}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{25:1--25:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.25},
  URN =		{urn:nbn:de:0030-drops-109693},
  doi =		{10.4230/LIPIcs.MFCS.2019.25},
  annote =	{Keywords: Martin-L\"{o}f randomness, subgroups of rationals, finitely generated subgroups of rationals, learning in the limit, behaviourally correct learning}
}
Document
Improving WCET Evaluation using Linear Relation Analysis

Authors: Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet

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


Abstract
The precision of a worst case execution time (WCET) evaluation tool on a given program is highly dependent on how the tool is able to detect and discard semantically infeasible executions of the program. In this paper, we propose to use the classical abstract interpretation-based method of linear relation analysis to discover and exploit relations between execution paths. For this purpose, we add auxiliary variables (counters) to the program to trace its execution paths. The results are easily incorporated in the classical workflow of a WCET evaluator, when the evaluator is based on the popular implicit path enumeration technique. We use existing tools - a WCET evaluator and a linear relation analyzer - to build and experiment a prototype implementation of this idea.

Cite as

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet. Improving WCET Evaluation using Linear Relation Analysis. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 02:1-02:28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@Article{raymond_et_al:LITES-v006-i001-a002,
  author =	{Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Jahier, Erwan and Halbwachs, Nicolas and Carrier, Fabienne and Asavoae, Mihail and Boutonnet, R\'{e}my},
  title =	{{Improving WCET Evaluation using Linear Relation Analysis}},
  booktitle =	{LITES, Volume 6, Issue 1 (2019)},
  pages =	{02:1--02:28},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2019},
  volume =	{6},
  number =	{1},
  editor =	{Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Jahier, Erwan and Halbwachs, Nicolas and Carrier, Fabienne and Asavoae, Mihail and Boutonnet, R\'{e}my},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v006-i001-a002},
  doi =		{10.4230/LITES-v006-i001-a002},
  annote =	{Keywords: Worst Case Execution Time estimation, Infeasible Execution Paths, Abstract Interpretation}
}
Document
Short Paper
An Experimental Comparison of Two Definitions for Groups of Moving Entities (Short Paper)

Authors: Lionov Wiratma, Maarten Löffler, and Frank Staals

Published in: LIPIcs, Volume 114, 10th International Conference on Geographic Information Science (GIScience 2018)


Abstract
Two of the grouping definitions for trajectories that have been developed in recent years allow a continuous motion model and allow varying shape groups. One of these definitions was suggested as a refinement of the other. In this paper we perform an experimental comparison to highlight the differences in these two definitions on various data sets.

Cite as

Lionov Wiratma, Maarten Löffler, and Frank Staals. An Experimental Comparison of Two Definitions for Groups of Moving Entities (Short Paper). In 10th International Conference on Geographic Information Science (GIScience 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 114, pp. 64:1-64:6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{wiratma_et_al:LIPIcs.GISCIENCE.2018.64,
  author =	{Wiratma, Lionov and L\"{o}ffler, Maarten and Staals, Frank},
  title =	{{An Experimental Comparison of Two Definitions for Groups of Moving Entities}},
  booktitle =	{10th International Conference on Geographic Information Science (GIScience 2018)},
  pages =	{64:1--64:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-083-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{114},
  editor =	{Winter, Stephan and Griffin, Amy and Sester, Monika},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GISCIENCE.2018.64},
  URN =		{urn:nbn:de:0030-drops-93928},
  doi =		{10.4230/LIPIcs.GISCIENCE.2018.64},
  annote =	{Keywords: Trajectories, grouping algorithms, experimental comparison}
}
Document
Closure of Resource-Bounded Randomness Notions Under Polynomial-Time Permutations

Authors: André Nies and Frank Stephan

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)


Abstract
An infinite bit sequence is called recursively random if no computable strategy betting along the sequence has unbounded capital. It is well-known that the property of recursive randomness is closed under computable permutations. We investigate analogous statements for randomness notions defined by betting strategies that are computable within resource bounds. Suppose that S is a polynomial time computable permutation of the set of strings over the unary alphabet (identified with the set of natural numbers). If the inverse of S is not polynomially bounded, it is not hard to build a polynomial time random bit sequence Z such that Z o S is not polynomial time random. So one should only consider permutations S satisfying the extra condition that the inverse is polynomially bounded. Now the closure depends on additional assumptions in complexity theory. Our first main result, Theorem 4, shows that if BPP contains a superpolynomial deterministic time class, then polynomial time randomness is not preserved by some permutation S such that in fact both S and its inverse are in P. Our second result, Theorem 11, shows that polynomial space randomness is preserved by polynomial time permutations with polynomially bounded inverse, so if P = PSPACE then polynomial time randomness is preserved.

Cite as

André Nies and Frank Stephan. Closure of Resource-Bounded Randomness Notions Under Polynomial-Time Permutations. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 51:1-51:10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{nies_et_al:LIPIcs.STACS.2018.51,
  author =	{Nies, Andr\'{e} and Stephan, Frank},
  title =	{{Closure of Resource-Bounded Randomness Notions Under Polynomial-Time Permutations}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{51:1--51:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.51},
  URN =		{urn:nbn:de:0030-drops-84938},
  doi =		{10.4230/LIPIcs.STACS.2018.51},
  annote =	{Keywords: Computational complexity, Randomness via resource-bounded betting strategies, Martingales, Closure under permutations}
}
Document
EMSBench: Benchmark and Testbed for Reactive Real-Time Systems

Authors: Florian Kluge, Christine Rochange, and Theo Ungerer

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


Abstract
Benchmark suites for real-time embedded systems (RTES) usually contain only pure computations that are often used in this domain. They allow to evaluate computing performance, but do not reproduce the complexity and behaviour that is typical for such systems. Actual RTES have to interact with the physical environment, which is often reflected by code that is executed concurrently. In this article, we present the software package EMSBench that mimics such complex behaviour, and highlight some of its use cases. The benchmark code ems of EMSBench is based on the open-source engine management system (EMS) FreeEMS. Additionally, EMSBench contains a trace generator (tg) that provides input signals for ems and enables to execute ems close to reality. We provide detailed descriptions of the ems's execution behaviour and of trace generation. EMSBench can be used as test or benchmark program to compare different hardware platforms, e.g. in terms of schedulability. Also, we use EMSBench as a benchmark for static worst-case execution time (WCET) analysis and compare these results to measurements performed on existing hardware. Our results based on the OTAWA WCET estimation tool show WCET overestimations by the static analysis from 11.9% to 41.1% depending on the complexity of the analysed functions.

Cite as

Florian Kluge, Christine Rochange, and Theo Ungerer. EMSBench: Benchmark and Testbed for Reactive Real-Time Systems. In LITES, Volume 4, Issue 2 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 2, pp. 02:1-02:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@Article{kluge_et_al:LITES-v004-i002-a002,
  author =	{Kluge, Florian and Rochange, Christine and Ungerer, Theo},
  title =	{{EMSBench: Benchmark and Testbed for Reactive Real-Time Systems}},
  booktitle =	{LITES, Volume 4, Issue 2 (2017)},
  pages =	{02:1--02:23},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{2},
  editor =	{Kluge, Florian and Rochange, Christine and Ungerer, Theo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i002-a002},
  doi =		{10.4230/LITES-v004-i002-a002},
  annote =	{Keywords: Real-time benchmark, WCET Analysis, Engine Management System}
}
Document
Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains

Authors: Eric W. D. Rozier, Kristin Y. Rozier, and Ulya Bayram

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


Abstract
As data centers attempt to cope with the exponential growth of data, new techniques for intelligent, software-defined data centers (SDDC) are being developed to confront the scale and pace of changing resources and requirements.  For cost-constrained environments, like those increasingly present in scientific research labs, SDDCs also may provide better reliability and performability with no additional hardware through the use of dynamic syndrome allocation. To do so, the middleware layers of SDDCs must be able to calculate and account for complex dependence relationships to determine an optimal data layout.  This challenge is exacerbated by the growth of constraints on the dependence problem when available resources are both large (due to a higher number of syndromes that can be stored) and small (due to the lack of available space for syndrome allocation). We present a quantitative method for characterizing these challenges using an analysis of attack domains for high-dimension variants of the $n$-queens problem that enables performable solutions via the SMT solver Z3. We demonstrate correctness of our technique, and provide experimental evidence of its efficacy; our implementation is publicly available.

Cite as

Eric W. D. Rozier, Kristin Y. Rozier, and Ulya Bayram. Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains. In LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1, pp. 05:1-05:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@Article{rozier_et_al:LITES-v004-i001-a005,
  author =	{Rozier, Eric W. D. and Rozier, Kristin Y. and Bayram, Ulya},
  title =	{{Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains}},
  booktitle =	{LITES, Volume 4, Issue 1 (2017)},
  pages =	{05:1--05:26},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  editor =	{Rozier, Eric W. D. and Rozier, Kristin Y. and Bayram, Ulya},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i001-a005},
  doi =		{10.4230/LITES-v004-i001-a005},
  annote =	{Keywords: SMT, Data dependence, n-queens}
}
Document
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}},
  booktitle =	{LITES, Volume 3, Issue 1 (2016)},
  pages =	{05:1--05:48},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2016},
  volume =	{3},
  number =	{1},
  editor =	{Lv, Mingsong and Guan, Nan and Reineke, Jan and Wilhelm, Reinhard and Yi, Wang},
  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
Randomized Caches Can Be Pretty Useful to Hard Real-Time Systems

Authors: Enrico Mezzetti, Marco Ziccardi, Tullio Vardanega, Jaume Abella, Eduardo Quiñones, and Francisco J. Cazorla

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


Abstract
Cache randomization per se, and its viability for probabilistic timing analysis (PTA) of critical real-time systems, are receiving increasingly close attention from the scientific community and the industrial practitioners. In fact, the very notion of introducing randomness and probabilities in time-critical systems has caused strenuous debates owing to the apparent clash that this idea has with the strictly deterministic view traditionally held for those systems. A paper recently appeared in LITES (Reineke, J. (2014). Randomized Caches Considered Harmful in Hard Real-Time Systems. LITES, 1(1), 03:1-03:13.) provides a critical analysis of the weaknesses and risks entailed in using randomized caches in hard real-time systems. In order to provide the interested reader with a fuller, balanced appreciation of the subject matter, a critical analysis of the benefits brought about by that innovation should be provided also. This short paper addresses that need by revisiting the array of issues addressed in the cited work, in the light of the latest advances to the relevant state of the art. Accordingly, we show that the potential benefits of randomized caches do offset their limitations, causing them to be - when used in conjunction with PTA - a serious competitor to conventional designs.

Cite as

Enrico Mezzetti, Marco Ziccardi, Tullio Vardanega, Jaume Abella, Eduardo Quiñones, and Francisco J. Cazorla. Randomized Caches Can Be Pretty Useful to Hard Real-Time Systems. In LITES, Volume 2, Issue 1 (2015). Leibniz Transactions on Embedded Systems, Volume 2, Issue 1, pp. 01:1-01:10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{mezzetti_et_al:LITES-v002-i001-a001,
  author =	{Mezzetti, Enrico and Ziccardi, Marco and Vardanega, Tullio and Abella, Jaume and Qui\~{n}ones, Eduardo and Cazorla, Francisco J.},
  title =	{{Randomized Caches Can Be Pretty Useful to Hard Real-Time Systems}},
  booktitle =	{LITES, Volume 2, Issue 1 (2015)},
  pages =	{01:1--01:10},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2015},
  volume =	{2},
  number =	{1},
  editor =	{Mezzetti, Enrico and Ziccardi, Marco and Vardanega, Tullio and Abella, Jaume and Qui\~{n}ones, Eduardo and Cazorla, Francisco J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v002-i001-a001},
  doi =		{10.4230/LITES-v002-i001-a001},
  annote =	{Keywords: Real-time systems, Probabilistic WCET, Randomized caches}
}
Document
Inductive Inference and Reverse Mathematics

Authors: Rupert Hölzl, Sanjay Jain, and Frank Stephan

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)


Abstract
The present work investigates inductive inference from the perspective of reverse mathematics. Reverse mathematics is a framework which relates the proof strength of theorems and axioms throughout many areas of mathematics in an interdisciplinary way. The present work looks at basic notions of learnability including Angluin's tell-tale condition and its variants for learning in the limit and for conservative learning. Furthermore, the more general criterion of partial learning is investigated. These notions are studied in the reverse mathematics context for uniformly and weakly represented families of languages. The results are stated in terms of axioms referring to domination and induction strength.

Cite as

Rupert Hölzl, Sanjay Jain, and Frank Stephan. Inductive Inference and Reverse Mathematics. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 420-433, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{holzl_et_al:LIPIcs.STACS.2015.420,
  author =	{H\"{o}lzl, Rupert and Jain, Sanjay and Stephan, Frank},
  title =	{{Inductive Inference and Reverse Mathematics}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{420--433},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.420},
  URN =		{urn:nbn:de:0030-drops-49324},
  doi =		{10.4230/LIPIcs.STACS.2015.420},
  annote =	{Keywords: reverse mathematics, recursion theory, inductive inference, learning from positive data}
}
Document
Implementing Mixed-criticality Systems Upon a Preemptive Varying-speed Processor

Authors: Zhishan Guo and Sanjoy K. Baruah

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


Abstract
A mixed criticality (MC) workload consists of components of varying degrees of importance (or "criticalities"); the more critical components typically need to have their correctness validated to greater levels of assurance than the less critical ones. The problem of executing such a MC workload upon a preemptive processor whose effective speed may vary during run-time, in a manner that is not completely known prior to run-time, is considered.Such a processor is modeled as being characterized by several execution speeds: a normal speed and several levels of degraded speed. Under normal circumstances it will execute at or above its normal speed; conditions during run-time may cause it to execute slower. It is desired that all components of the MC workload execute correctly under normal circumstances. If the processor speed degrades, it should nevertheless remain the case that the more critical components execute correctly (although the less critical ones need not do so).In this work, we derive an optimal algorithm for scheduling MC workloads upon such platforms; achieving optimality does not require that the processor be able to monitor its own run-time speed. For the sub-case of the general problem where there are only two criticality levels defined, we additionally provide an implementation that is asymptotically optimal in terms of run-time efficiency.

Cite as

Zhishan Guo and Sanjoy K. Baruah. Implementing Mixed-criticality Systems Upon a Preemptive Varying-speed Processor. In LITES, Volume 1, Issue 2 (2014). Leibniz Transactions on Embedded Systems, Volume 1, Issue 2, pp. 03:1-03:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@Article{guo_et_al:LITES-v001-i002-a003,
  author =	{Guo, Zhishan and Baruah, Sanjoy K.},
  title =	{{Implementing Mixed-criticality Systems Upon a Preemptive Varying-speed Processor}},
  booktitle =	{LITES, Volume 1, Issue 2 (2014)},
  pages =	{03:1--03:19},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2014},
  volume =	{1},
  number =	{2},
  editor =	{Guo, Zhishan and Baruah, Sanjoy K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v001-i002-a003},
  doi =		{10.4230/LITES-v001-i002-a003},
  annote =	{Keywords: Mixed criticalities, Varying-speed processor, Preemptive uniprocessor scheduling, }
}
Document
Randomized Caches Considered Harmful in Hard Real-Time Systems

Authors: Jan Reineke

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


Abstract
We investigate the suitability of caches with randomized placement and replacement in the context of hard real-time systems. Such caches have been claimed to drastically reduce the amount of information required by static worst-case execution time (WCET) analysis, and to be an enabler for measurement-based probabilistic timing analysis. We refute these claims and conclude that with prevailing static and measurement-based analysis techniques caches with deterministic placement and least-recently-used replacement are preferable over randomized ones.

Cite as

Jan Reineke. Randomized Caches Considered Harmful in Hard Real-Time Systems. In LITES, Volume 1, Issue 1 (2014). Leibniz Transactions on Embedded Systems, Volume 1, Issue 1, pp. 03:1-03:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@Article{reineke:LITES-v001-i001-a003,
  author =	{Reineke, Jan},
  title =	{{Randomized Caches Considered Harmful in Hard Real-Time Systems}},
  booktitle =	{LITES, Volume 1, Issue 1 (2014)},
  pages =	{03:1--03:13},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2014},
  volume =	{1},
  number =	{1},
  editor =	{Reineke, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v001-i001-a003},
  doi =		{10.4230/LITES-v001-i001-a003},
  annote =	{Keywords: Real-time systems, Caches, Randomization, WCET analysis}
}
  • Refine by Author
  • 7 Stephan, Frank
  • 3 Jain, Sanjay
  • 2 Hoi, Gordon
  • 2 Nies, André
  • 2 Reineke, Jan
  • Show More...

  • Refine by Classification
  • 2 Computer systems organization → Real-time system architecture
  • 2 Software and its engineering → Real-time systems software
  • 2 Theory of computation → Design and analysis of algorithms
  • 1 Computer systems organization
  • 1 Computer systems organization → Embedded and cyber-physical systems
  • Show More...

  • Refine by Keyword
  • 2 Exponential Time Algorithms
  • 2 Real-time systems
  • 1 Abstract Interpretation
  • 1 Cache analysis
  • 1 Caches
  • Show More...

  • Refine by Type
  • 17 document

  • Refine by Publication Year
  • 4 2019
  • 2 2014
  • 2 2015
  • 2 2017
  • 2 2018
  • 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