18 Search Results for "Lee, Edward"

Document
DOI: 10.4230/LIPIcs.AFT.2023.23
Buying Time: Latency Racing vs. Bidding for Transaction Ordering

Authors: Akaki Mamageishvili, Mahimna Kelkar, Jan Christoph Schlegel, and Edward W. Felten

Published in: LIPIcs, Volume 282, 5th Conference on Advances in Financial Technologies (AFT 2023)

Abstract
We design TimeBoost: a practical transaction ordering policy for rollup sequencers that takes into account both transaction timestamps and bids; it works by creating a score from timestamps and bids, and orders transactions based on this score. TimeBoost is transaction-data-independent (i.e., can work with encrypted transactions) and supports low transaction finalization times similar to a first-come first-serve (FCFS or pure-latency) ordering policy. At the same time, it avoids the inefficient latency competition created by an FCFS policy. It further satisfies useful economic properties of first-price auctions that come with a pure-bidding policy. We show through rigorous economic analyses how TimeBoost allows players to compete on arbitrage opportunities in a way that results in better guarantees compared to both pure-latency and pure-bidding approaches.
Cite as

Akaki Mamageishvili, Mahimna Kelkar, Jan Christoph Schlegel, and Edward W. Felten. Buying Time: Latency Racing vs. Bidding for Transaction Ordering. In 5th Conference on Advances in Financial Technologies (AFT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 282, pp. 23:1-23:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mamageishvili_et_al:LIPIcs.AFT.2023.23,
  author =	{Mamageishvili, Akaki and Kelkar, Mahimna and Schlegel, Jan Christoph and Felten, Edward W.},
  title =	{{Buying Time: Latency Racing vs. Bidding for Transaction Ordering}},
  booktitle =	{5th Conference on Advances in Financial Technologies (AFT 2023)},
  pages =	{23:1--23:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-303-4},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{282},
  editor =	{Bonneau, Joseph and Weinberg, S. Matthew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2023.23},
  URN =		{urn:nbn:de:0030-drops-192120},
  doi =		{10.4230/LIPIcs.AFT.2023.23},
  annote =	{Keywords: Transaction ordering, First-come-first-serve, First-price auctions}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2023.44
On the Power of Regular and Permutation Branching Programs

Authors: Chin Ho Lee, Edward Pyne, and Salil Vadhan

Published in: LIPIcs, Volume 275, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)

Abstract
We give new upper and lower bounds on the power of several restricted classes of arbitrary-order read-once branching programs (ROBPs) and standard-order ROBPs (SOBPs) that have received significant attention in the literature on pseudorandomness for space-bounded computation. - Regular SOBPs of length n and width ⌊w(n+1)/2⌋ can exactly simulate general SOBPs of length n and width w, and moreover an n/2-o(n) blow-up in width is necessary for such a simulation. Our result extends and simplifies prior average-case simulations (Reingold, Trevisan, and Vadhan (STOC 2006), Bogdanov, Hoza, Prakriya, and Pyne (CCC 2022)), in particular implying that weighted pseudorandom generators (Braverman, Cohen, and Garg (SICOMP 2020)) for regular SOBPs of width poly(n) or larger automatically extend to general SOBPs. Furthermore, our simulation also extends to general (even read-many) oblivious branching programs. - There exist natural functions computable by regular SOBPs of constant width that are average-case hard for permutation SOBPs of exponential width. Indeed, we show that Inner-Product mod 2 is average-case hard for arbitrary-order permutation ROBPs of exponential width. - There exist functions computable by constant-width arbitrary-order permutation ROBPs that are worst-case hard for exponential-width SOBPs. - Read-twice permutation branching programs of subexponential width can simulate polynomial-width arbitrary-order ROBPs.
Cite as

Chin Ho Lee, Edward Pyne, and Salil Vadhan. On the Power of Regular and Permutation Branching Programs. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 44:1-44:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{lee_et_al:LIPIcs.APPROX/RANDOM.2023.44,
  author =	{Lee, Chin Ho and Pyne, Edward and Vadhan, Salil},
  title =	{{On the Power of Regular and Permutation Branching Programs}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)},
  pages =	{44:1--44:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-296-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{275},
  editor =	{Megow, Nicole and Smith, Adam},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.44},
  URN =		{urn:nbn:de:0030-drops-188698},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2023.44},
  annote =	{Keywords: Pseudorandomness, Branching Programs}
}
Document
DOI: 10.4230/OASIcs.NG-RES.2023.3
Beyond the Threaded Programming Model on Real-Time Operating Systems

Authors: Erling Rennemo Jellum, Shaokai Lin, Peter Donovan, Efsane Soyer, Fuzail Shakir, Torleiv Bryne, Milica Orlandic, Marten Lohstroh, and Edward A. Lee

Published in: OASIcs, Volume 108, Fourth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2023)

Abstract
The use of a real-time operating system (RTOS) raises the abstraction level for embedded systems design when compared to traditional bare-metal programming, resulting in simpler and more reusable application code. Modern RTOSes for resource-constrained platforms, like Zephyr and FreeRTOS, also offer threading support, but this kind of shared memory concurrency is a poor fit for expressing the reactive and interactive behaviors that are common in embedded systems. To address this, alternative concurrency models like the actor model or communicating sequential processes have been proposed. While those alternatives enable reactive design patterns, they fail to deliver determinism and do not address timing. This makes it difficult to verify that implemented behavior is as intended and impossible to specify timing constraints in a portable way. This makes it hard to create reusable library components out of common embedded design patterns, forcing developers to keep reinventing the wheel for each application and each platform. In this paper, we introduce the embedded target of Lingua Franca (LF) as a means to move beyond the threaded programming model provided by RTOSes and improve the state of the art in embedded programming. LF is based on the reactor model of computation, which is reactive, deterministic, and timed, providing a means to express concurrency and timing in a platform-independent way. We compare the performance of LF versus threaded C code - both running on Zephyr - in terms of response time, timing precision, throughput, and memory footprint.
Cite as

Erling Rennemo Jellum, Shaokai Lin, Peter Donovan, Efsane Soyer, Fuzail Shakir, Torleiv Bryne, Milica Orlandic, Marten Lohstroh, and Edward A. Lee. Beyond the Threaded Programming Model on Real-Time Operating Systems. In Fourth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2023). Open Access Series in Informatics (OASIcs), Volume 108, pp. 3:1-3:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jellum_et_al:OASIcs.NG-RES.2023.3,
  author =	{Jellum, Erling Rennemo and Lin, Shaokai and Donovan, Peter and Soyer, Efsane and Shakir, Fuzail and Bryne, Torleiv and Orlandic, Milica and Lohstroh, Marten and Lee, Edward A.},
  title =	{{Beyond the Threaded Programming Model on Real-Time Operating Systems}},
  booktitle =	{Fourth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2023)},
  pages =	{3:1--3:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-268-6},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{108},
  editor =	{Terraneo, Federico and Cattaneo, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.NG-RES.2023.3},
  URN =		{urn:nbn:de:0030-drops-177348},
  doi =		{10.4230/OASIcs.NG-RES.2023.3},
  annote =	{Keywords: Real time, concurrency, reactors, Lingua Franca, RTOS}
}
Document
DOI: 10.4230/LITES.8.2.4
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors: Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle

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

Abstract
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Cite as

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:LITES.8.2.4,
  author =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  title =	{{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:34},
  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.4},
  doi =		{10.4230/LITES.8.2.4},
  annote =	{Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}
Document
DOI: 10.4230/LITES.8.2.7
Real-Time Verification for Distributed Cyber-Physical Systems

Authors: Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson

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

Abstract
Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent transportation, where autonomous vehicles communicate and cooperate with each other via a high-speed communication network. Such systems require an ability to identify maneuvers in real-time that cause dangerous circumstances and ensure the implementation always meets safety-critical requirements. In this paper, we propose a real-time decentralized reachability approach for safety verification of a distributed multi-agent CPS with the underlying assumption that all agents are time-synchronized with a low degree of error. In the proposed approach, each agent periodically computes its local reachable set and exchanges this reachable set with the other agents with the goal of verifying the system safety. Our method, implemented in Java, takes advantages of the timing information and the reachable set information that are available in the exchanged messages to reason about the safety of the whole system in a decentralized manner. Any particular agent can also perform local safety verification tasks based on their local clocks by analyzing the messages it receives. We applied the proposed method to verify, in real-time, the safety properties of a group of quadcopters performing a distributed search mission.
Cite as

Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson. Real-Time Verification for Distributed Cyber-Physical Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 07:1-07:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{tran_et_al:LITES.8.2.7,
  author =	{Tran, Hoang-Dung and Nguyen, Luan Viet and Musau, Patrick and Xiang, Weiming and Johnson, Taylor T.},
  title =	{{Real-Time Verification for Distributed Cyber-Physical Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{07:1--07:19},
  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.7},
  doi =		{10.4230/LITES.8.2.7},
  annote =	{Keywords: Verification, Reachability Analysis, Distributed Cyber-Physical Systems}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2022.2
Fourier Growth of Regular Branching Programs

Authors: Chin Ho Lee, Edward Pyne, and Salil Vadhan

Published in: LIPIcs, Volume 245, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2022)

Abstract
We analyze the Fourier growth, i.e. the L₁ Fourier weight at level k (denoted L_{1,k}), of read-once regular branching programs. We prove that every read-once regular branching program B of width w ∈ [1,∞] with s accepting states on n-bit inputs must have its L_{1,k} bounded by min{Pr[B(U_n) = 1](w-1)^k, s ⋅ O((n log n)/k)^{(k-1)/2}}. For any constant k, our result is tight up to constant factors for the AND function on w-1 bits, and is tight up to polylogarithmic factors for unbounded width programs. In particular, for k = 1 we have L_{1,1}(B) ≤ s, with no dependence on the width w of the program. Our result gives new bounds on the coin problem and new pseudorandom generators (PRGs). Furthermore, we obtain an explicit generator for unordered permutation branching programs of unbounded width with a constant factor stretch, where no PRG was previously known. Applying a composition theorem of Błasiok, Ivanov, Jin, Lee, Servedio and Viola (RANDOM 2021), we extend our results to "generalized group products," a generalization of modular sums and product tests.
Cite as

Chin Ho Lee, Edward Pyne, and Salil Vadhan. Fourier Growth of Regular Branching Programs. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 245, pp. 2:1-2:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{lee_et_al:LIPIcs.APPROX/RANDOM.2022.2,
  author =	{Lee, Chin Ho and Pyne, Edward and Vadhan, Salil},
  title =	{{Fourier Growth of Regular Branching Programs}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2022)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-249-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{245},
  editor =	{Chakrabarti, Amit and Swamy, Chaitanya},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2022.2},
  URN =		{urn:nbn:de:0030-drops-171247},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2022.2},
  annote =	{Keywords: pseudorandomness, fourier analysis}
}
Document
DOI: 10.4230/LIPIcs.CCC.2022.3
Hitting Sets for Regular Branching Programs

Authors: Andrej Bogdanov, William M. Hoza, Gautam Prakriya, and Edward Pyne

Published in: LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022)

Abstract
We construct improved hitting set generators (HSGs) for ordered (read-once) regular branching programs in two parameter regimes. First, we construct an explicit ε-HSG for unbounded-width regular branching programs with a single accept state with seed length Õ(log n ⋅ log(1/ε)), where n is the length of the program. Second, we construct an explicit ε-HSG for width-w length-n regular branching programs with seed length Õ(log n ⋅ (√{log(1/ε)} + log w) + log(1/ε)). For context, the "baseline" in this area is the pseudorandom generator (PRG) by Nisan (Combinatorica 1992), which fools ordered (possibly non-regular) branching programs with seed length O(log(wn/ε) ⋅ log n). For regular programs, the state-of-the-art PRG, by Braverman, Rao, Raz, and Yehudayoff (FOCS 2010, SICOMP 2014), has seed length Õ(log(w/ε) ⋅ log n), which beats Nisan’s seed length when log(w/ε) = o(log n). Taken together, our two new constructions beat Nisan’s seed length in all parameter regimes except when log w and log(1/ε) are both Ω(log n) (for the construction of HSGs for regular branching programs with a single accept vertex). Extending work by Reingold, Trevisan, and Vadhan (STOC 2006), we furthermore show that an explicit HSG for regular branching programs with a single accept vertex with seed length o(log² n) in the regime log w = Θ(log(1/ε)) = Θ(log n) would imply improved HSGs for general ordered branching programs, which would be a major breakthrough in derandomization. Pyne and Vadhan (CCC 2021) recently obtained such parameters for the special case of permutation branching programs.
Cite as

Andrej Bogdanov, William M. Hoza, Gautam Prakriya, and Edward Pyne. Hitting Sets for Regular Branching Programs. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 3:1-3:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bogdanov_et_al:LIPIcs.CCC.2022.3,
  author =	{Bogdanov, Andrej and Hoza, William M. and Prakriya, Gautam and Pyne, Edward},
  title =	{{Hitting Sets for Regular Branching Programs}},
  booktitle =	{37th Computational Complexity Conference (CCC 2022)},
  pages =	{3:1--3:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-241-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{234},
  editor =	{Lovett, Shachar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.3},
  URN =		{urn:nbn:de:0030-drops-165658},
  doi =		{10.4230/LIPIcs.CCC.2022.3},
  annote =	{Keywords: Pseudorandomness, hitting set generators, space-bounded computation}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2021.7
Pseudorandom Generators for Unbounded-Width Permutation Branching Programs

Authors: William M. Hoza, Edward Pyne, and Salil Vadhan

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)

Abstract
We prove that the Impagliazzo-Nisan-Wigderson [Impagliazzo et al., 1994] pseudorandom generator (PRG) fools ordered (read-once) permutation branching programs of unbounded width with a seed length of Õ(log d + log n ⋅ log(1/ε)), assuming the program has only one accepting vertex in the final layer. Here, n is the length of the program, d is the degree (equivalently, the alphabet size), and ε is the error of the PRG. In contrast, we show that a randomly chosen generator requires seed length Ω(n log d) to fool such unbounded-width programs. Thus, this is an unusual case where an explicit construction is "better than random." Except when the program’s width w is very small, this is an improvement over prior work. For example, when w = poly(n) and d = 2, the best prior PRG for permutation branching programs was simply Nisan’s PRG [Nisan, 1992], which fools general ordered branching programs with seed length O(log(wn/ε) log n). We prove a seed length lower bound of Ω̃(log d + log n ⋅ log(1/ε)) for fooling these unbounded-width programs, showing that our seed length is near-optimal. In fact, when ε ≤ 1/log n, our seed length is within a constant factor of optimal. Our analysis of the INW generator uses the connection between the PRG and the derandomized square of Rozenman and Vadhan [Rozenman and Vadhan, 2005] and the recent analysis of the latter in terms of unit-circle approximation by Ahmadinejad et al. [Ahmadinejad et al., 2020].
Cite as

William M. Hoza, Edward Pyne, and Salil Vadhan. Pseudorandom Generators for Unbounded-Width Permutation Branching Programs. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 7:1-7:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hoza_et_al:LIPIcs.ITCS.2021.7,
  author =	{Hoza, William M. and Pyne, Edward and Vadhan, Salil},
  title =	{{Pseudorandom Generators for Unbounded-Width Permutation Branching Programs}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.7},
  URN =		{urn:nbn:de:0030-drops-135464},
  doi =		{10.4230/LIPIcs.ITCS.2021.7},
  annote =	{Keywords: Pseudorandom generators, permutation branching programs}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.69
Exact Algorithms via Multivariate Subroutines

Authors: Serge Gaspers and Edward J. Lee

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We consider the family of Phi-Subset problems, where the input consists of an instance I of size N over a universe U_I of size n and the task is to check whether the universe contains a subset with property Phi (e.g., Phi could be the property of being a feedback vertex set for the input graph of size at most k). Our main tool is a simple randomized algorithm which solves Phi-Subset in time (1+b-(1/c))^n N^(O(1)), provided that there is an algorithm for the Phi-Extension problem with running time b^{n-|X|} c^k N^{O(1)}. Here, the input for Phi-Extension is an instance I of size N over a universe U_I of size n, a subset X \subseteq U_I, and an integer k, and the task is to check whether there is a set Y with X \subseteq Y \subseteq U_I and |Y \ X| <= k with property Phi. We derandomize this algorithm at the cost of increasing the running time by a subexponential factor in n, and we adapt it to the enumeration setting where we need to enumerate all subsets of the universe with property Phi. This generalizes the results of Fomin et al. [STOC 2016] who proved the case where b=1. As case studies, we use these results to design faster deterministic algorithms for: - checking whether a graph has a feedback vertex set of size at most k - enumerating all minimal feedback vertex sets - enumerating all minimal vertex covers of size at most k, and - enumerating all minimal 3-hitting sets. We obtain these results by deriving new b^{n-|X|} c^k N^{O(1)}-time algorithms for the corresponding Phi-Extension problems (or enumeration variant). In some cases, this is done by adapting the analysis of an existing algorithm, or in other cases by designing a new algorithm. Our analyses are based on Measure and Conquer, but the value to minimize, 1+b-(1/c), is unconventional and requires non-convex optimization.
Cite as

Serge Gaspers and Edward J. Lee. Exact Algorithms via Multivariate Subroutines. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 69:1-69:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gaspers_et_al:LIPIcs.ICALP.2017.69,
  author =	{Gaspers, Serge and Lee, Edward J.},
  title =	{{Exact Algorithms via Multivariate Subroutines}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{69:1--69:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.69},
  URN =		{urn:nbn:de:0030-drops-74251},
  doi =		{10.4230/LIPIcs.ICALP.2017.69},
  annote =	{Keywords: enumeration algorithms, exponential time algorithms, feedback vertex set, hitting set}
}
Document
DOI: 10.4230/LITES-v004-i001-a004
How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty

Authors: Holger Hermanns, Jan Krčál, and Gilles Nies

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

Abstract
The kinetic battery model is a popular model of the dynamic behaviour of a conventional battery, useful to predict or optimize the time until battery depletion. The model however lacks certain obvious aspects of batteries in-the-wild, especially with respect to the effects of random influences and the behaviour when charging up to capacity limits.This paper considers the kinetic battery model with limited capacity in the context of piecewise constant yet random charging and discharging. We provide exact representations of the battery behaviour wherever possible, and otherwise develop safe approximations that bound the probability distribution of the battery state from above and below. The resulting model enables the time-dependent evaluation of the risk of battery depletion. This is demonstrated in an extensive dependability study of a nano satellite currently orbiting the earth.
Cite as

Holger Hermanns, Jan Krčál, and Gilles Nies. How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty. In LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1, pp. 04:1-04:28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{hermanns_et_al:LITES-v004-i001-a004,
  author =	{Hermanns, Holger and Kr\v{c}\'{a}l, Jan and Nies, Gilles},
  title =	{{How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:28},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i001-a004},
  doi =		{10.4230/LITES-v004-i001-a004},
  annote =	{Keywords: Battery Power, Depletion Risk, Bounded Charging and Discharging, Stochastic Load, Distribution Bounds}
}
Document
DOI: 10.4230/LITES-v004-i001-a005
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}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{05:1--05:26},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  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
DOI: 10.4230/LITES-v003-i001-a001
Programming Language Constructs Supporting Fault Tolerance

Authors: Christina Houben and Sebastian Houben

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

Abstract
In order to render software viable for highly safety-critical applications, we describe how to incorporate fault tolerance mechanisms into the real-time programming language PEARL. Therefore, we present, classify, evaluate and illustrate known fault tolerance methods for software. We link them together with the requirements of the international standard IEC 61508-3 for functional safety. We contribute PEARL-2020 programming language constructs for fault tolerance methods that need to be implemented by operating systems, and code-snippets as well as libraries for those independent from runtime systems.
Cite as

Christina Houben and Sebastian Houben. Programming Language Constructs Supporting Fault Tolerance. In LITES, Volume 3, Issue 1 (2016). Leibniz Transactions on Embedded Systems, Volume 3, Issue 1, pp. 01:1-01:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{houben_et_al:LITES-v003-i001-a001,
  author =	{Houben, Christina and Houben, Sebastian},
  title =	{{Programming Language Constructs Supporting Fault Tolerance}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:20},
  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-a001},
  doi =		{10.4230/LITES-v003-i001-a001},
  annote =	{Keywords: Fault tolerance, Functional safety, PEARL, Embedded systems, Software engineering}
}
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.FSTTCS.2014.199
Lift & Project Systems Performing on the Partial Vertex Cover Polytope

Authors: Konstantinos Georgiou and Edward Lee

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We study integrality gap (IG) lower bounds on strong LP and SDP relaxations derived by the Sherali-Adams (SA), Lovász-Schrijver-SDP (LS_+), and Sherali-Adams-SDP (SA_+) lift-and-project (L&P) systems for the t-Partial-Vertex-Cover (t-PVC) problem, a variation of the classic Vertex-Cover problem in which only t edges need to be covered. t-PVC admits a 2-approximation using various algorithmic techniques, all relying on a natural LP relaxation. Starting from this LP relaxation, our main results assert that for every epsilon>0, level-Theta(n) LPs or SDPs derived by all known L&P systems that have been used for positive algorithmic results (but the Lasserre hierarchy) have IGs at least (1-epsilon)n/t, where n is the number of vertices of the input graph. Our lower bounds are nearly tight, in that level-n relaxations, even of the weakest systems, have integrality gap 1. As lift-and-project systems have given the best algorithms known for numerous combinatorial optimization problems, our results show that restricted yet powerful models of computation derived by many L&P systems fail to witness c-approximate solutions to t-PVC for any constant c, and for t=O(n). This is one of the very few known examples of an intractable combinatorial optimization problem for which LP-based algorithms induce a constant approximation ratio, still lift-and-project LP and SDP tightenings of the same LP have unbounded IGs. As further motivation for our results, we show that the SDP that has given the best algorithm known for t-PVC has integrality gap n/t on instances that can be solved by the level-1 LP relaxation derived by the LS system. This constitutes another rare phenomenon where (even in specific instances) a static LP outperforms an SDP that has been used for the best approximation guarantee for the problem at hand. Finally, we believe our results are of independent interest as they are among the very few known integrality gap lower bounds for LP and SDP 0-1 relaxations in which not all variables possess the same semantics in the underlying combinatorial optimization problem. Most importantly, one of our main contributions is that we make explicit of a new and simple methodology of constructing solutions to LP relaxations that almost trivially satisfy constraints derived by all SDP L&P systems known to be useful for algorithmic positive results (except the La system). The latter sheds some light as to why La tightenings seem strictly stronger than LS_+ or SA_+ tightenings.
Cite as

Konstantinos Georgiou and Edward Lee. Lift & Project Systems Performing on the Partial Vertex Cover Polytope. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 199-211, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{georgiou_et_al:LIPIcs.FSTTCS.2014.199,
  author =	{Georgiou, Konstantinos and Lee, Edward},
  title =	{{Lift \& Project Systems Performing on the Partial Vertex Cover Polytope}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{199--211},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.199},
  URN =		{urn:nbn:de:0030-drops-48437},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.199},
  annote =	{Keywords: Partial vertex cover, combinatorial optimization, linear programming, semidefinite programming, lift and project systems, integrality gaps}
}
Document
DOI: 10.4230/DagSemProc.09481.1
09481 Abstracts Collection – SYNCHRON 2009

Authors: Albert Benveniste, Stephen A. Edwards, Edward Lee, Klaus Schneider, and Reinhard von Hanxleden

Published in: Dagstuhl Seminar Proceedings, Volume 9481, SYNCHRON 2009

Abstract
The 16th SYNCHRON workshop has been organized as Dagstuhl seminar 09481 from November 22-27, 2009. Online material of the seminar is available at the following web page: http://www.dagstuhl.de/de/programm/kalender/semhp/?semnr=09481
Cite as

Albert Benveniste, Stephen A. Edwards, Edward Lee, Klaus Schneider, and Reinhard von Hanxleden. 09481 Abstracts Collection – SYNCHRON 2009. In SYNCHRON 2009. Dagstuhl Seminar Proceedings, Volume 9481, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{benveniste_et_al:DagSemProc.09481.1,
  author =	{Benveniste, Albert and Edwards, Stephen A. and Lee, Edward and Schneider, Klaus and von Hanxleden, Reinhard},
  title =	{{09481 Abstracts Collection – SYNCHRON 2009}},
  booktitle =	{SYNCHRON 2009},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9481},
  editor =	{Albert Benveniste and Stephen A. Edwards and Edward Lee and Klaus Schneider and Reinhard von Hanxleden},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09481.1},
  URN =		{urn:nbn:de:0030-drops-24340},
  doi =		{10.4230/DagSemProc.09481.1},
  annote =	{Keywords: Synchronous languages, Safety-critical real-time systems, Model-based design, Discrete and hybrid systems, Combining synchronous and asynchronous models, Formally consistent subsetting of UML, High-level hardware modeling and synthesis, Compilation and code synthesis for embedded systems}
}
  • Refine by Author
  • 4 Lee, Edward
  • 4 Pyne, Edward
  • 3 Vadhan, Salil
  • 2 Giese, Holger
  • 2 Hoza, William M.
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Pseudorandomness and derandomization
  • 1 Computer systems organization
  • 1 Computer systems organization → Embedded and cyber-physical systems
  • 1 Computer systems organization → Embedded software
  • 1 Computer systems organization → Real-time systems
  • Show More...

  • Refine by Keyword
  • 2 MDD
  • 2 Models
  • 2 Pseudorandomness
  • 2 embedded systems
  • 2 model-based
  • Show More...

  • Refine by Type
  • 18 document

  • Refine by Publication Year
  • 4 2022
  • 3 2017
  • 3 2023
  • 2 2007
  • 1 1997
  • 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