4 Search Results for "Dietrich, Christian"

Document
DOI: 10.4230/LIPIcs.STACS.2024.12
Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form

Authors: Christoph Berkholz, Dietrich Kuske, and Christian Schwarz

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Is it possible to write significantly smaller formulae, when using more Boolean operators in addition to the De Morgan basis (and, or, not)? For propositional logic a negative answer was given by Pratt: every formula with additional operators can be translated to the De Morgan basis with only polynomial increase in size. Surprisingly, for modal logic the picture is different: we show that adding bi-implication allows to write exponentially smaller formulae. Moreover, we provide a complete classification of finite sets of Boolean operators showing they are either of no help (allow polynomial translations to the De Morgan basis) or can express properties as succinct as modal logic with additional bi-implication. More precisely, these results are shown for the modal logic T (and therefore for K). We complement this result showing that the modal logic S5 behaves as propositional logic: no additional Boolean operators make it possible to write significantly smaller formulae.
Cite as

Christoph Berkholz, Dietrich Kuske, and Christian Schwarz. Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.STACS.2024.12,
  author =	{Berkholz, Christoph and Kuske, Dietrich and Schwarz, Christian},
  title =	{{Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.12},
  URN =		{urn:nbn:de:0030-drops-197228},
  doi =		{10.4230/LIPIcs.STACS.2024.12},
  annote =	{Keywords: succinctness, modal logic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.61
Complexity of Counting First-Order Logic for the Subword Order

Authors: Dietrich Kuske and Christian Schwarz

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
This paper considers the structure consisting of the set of all words over a given alphabet together with the subword relation, regular predicates, and constants for every word. We are interested in the counting extension of first-order logic by threshold counting quantifiers. The main result shows that the two-variable fragment of this logic can be decided in two-fold exponential space provided the regular predicates are restricted to piecewise testable ones. This result improves prior insights by Karandikar and Schnoebelen by extending the logic and saving one exponent. Its proof consists of two main parts: First, we provide a quantifier elimination procedure that results in a formula with constants of bounded length (this generalizes the procedure by Karandikar and Schnoebelen for first-order logic). From this, it follows that quantification in formulas can be restricted to words of bounded length, i.e., the second part of the proof is an adaptation of the method by Ferrante and Rackoff to counting logic and deviates significantly from the path of reasoning by Karandikar and Schnoebelen.
Cite as

Dietrich Kuske and Christian Schwarz. Complexity of Counting First-Order Logic for the Subword Order. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 61:1-61:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kuske_et_al:LIPIcs.MFCS.2020.61,
  author =	{Kuske, Dietrich and Schwarz, Christian},
  title =	{{Complexity of Counting First-Order Logic for the Subword Order}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{61:1--61:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.61},
  URN =		{urn:nbn:de:0030-drops-127297},
  doi =		{10.4230/LIPIcs.MFCS.2020.61},
  annote =	{Keywords: Counting logic, piecewise testable languages}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2018.24
Whole-System Worst-Case Energy-Consumption Analysis for Energy-Constrained Real-Time Systems

Authors: Peter Wägemann, Christian Dietrich, Tobias Distler, Peter Ulbrich, and Wolfgang Schröder-Preikschat

Published in: LIPIcs, Volume 106, 30th Euromicro Conference on Real-Time Systems (ECRTS 2018)

Abstract
Although internal devices (e.g., memory, timers) and external devices (e.g., transceivers, sensors) significantly contribute to the energy consumption of an embedded real-time system, their impact on the worst-case response energy consumption (WCRE) of tasks is usually not adequately taken into account. Most WCRE analysis techniques, for example, only focus on the processor and therefore do not consider the energy consumption of other hardware units. Apart from that, the typical approach for dealing with devices is to assume that all of them are always activated, which leads to high WCRE overestimations in the general case where a system switches off the devices that are currently not needed in order to minimize energy consumption. In this paper, we present SysWCEC, an approach that addresses these problems by enabling static WCRE analysis for entire real-time systems, including internal as well as external devices. For this purpose, SysWCEC introduces a novel abstraction, the power-state-transition graph, which contains information about the worst-case energy consumption of all possible execution paths. To construct the graph, SysWCEC decomposes the analyzed real-time system into blocks during which the set of active devices in the system does not change and is consequently able to precisely handle devices being dynamically activated or deactivated.
Cite as

Peter Wägemann, Christian Dietrich, Tobias Distler, Peter Ulbrich, and Wolfgang Schröder-Preikschat. Whole-System Worst-Case Energy-Consumption Analysis for Energy-Constrained Real-Time Systems. In 30th Euromicro Conference on Real-Time Systems (ECRTS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 106, pp. 24:1-24:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{wagemann_et_al:LIPIcs.ECRTS.2018.24,
  author =	{W\"{a}gemann, Peter and Dietrich, Christian and Distler, Tobias and Ulbrich, Peter and Schr\"{o}der-Preikschat, Wolfgang},
  title =	{{Whole-System Worst-Case Energy-Consumption Analysis for Energy-Constrained Real-Time Systems}},
  booktitle =	{30th Euromicro Conference on Real-Time Systems (ECRTS 2018)},
  pages =	{24:1--24:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-075-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{106},
  editor =	{Altmeyer, Sebastian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2018.24},
  URN =		{urn:nbn:de:0030-drops-89795},
  doi =		{10.4230/LIPIcs.ECRTS.2018.24},
  annote =	{Keywords: energy-constrained real-time systems, worst-case energy consumption (WCEC), worst-case response energy consumption (WCRE), static whole-system analysis}
}
Document
DOI: 10.4230/DARTS.4.2.7
Whole-System WCEC Analysis for Energy-Constrained Real-Time Systems (Artifact)

Authors: Peter Wägemann, Christian Dietrich, Tobias Distler, Peter Ulbrich, and Wolfgang Schröder-Preikschat

Published in: DARTS, Volume 4, Issue 2, Special Issue of the 30th Euromicro Conference on Real-Time Systems (ECRTS 2018)

Abstract
Although internal devices (e.g., memory, timers) and external devices (e.g., sensors, transceivers) significantly contribute to the energy consumption of an embedded real-time system, their impact on the worst-case response energy consumption (WCRE) of tasks is usually not adequately taken into account. Most WCRE analysis techniques only focus on the processor and neglect the energy consumption of other hardware units that are temporarily activated and deactivated in the system. To solve the problem of system-wide energy-consumption analysis, we present SysWCEC, an approach that addresses these problems by enabling static WCRE analysis for entire real-time systems, including internal as well as external devices. For this purpose, SysWCEC introduces a novel abstraction, the power-state--transition graph, which contains information about the worst-case energy consumption of all possible execution paths. To construct the graph, SysWCEC decomposes the analyzed real-time system into blocks during which the set of active devices in the system does not change and is consequently able to precisely handle devices being dynamically activated or deactivated. In this artifact evaluation, which accompanies our related conference paper, we present easy to reproduce WCRE analyses with the SysWCEC framework using several benchmarks. The artifact comprises the generation of the power-state--transition graph from a given benchmark system and the formulation of an integer linear program whose solution eventually yields safe WCRE bounds.
Cite as

Peter Wägemann, Christian Dietrich, Tobias Distler, Peter Ulbrich, and Wolfgang Schröder-Preikschat. Whole-System WCEC Analysis for Energy-Constrained Real-Time Systems (Artifact). In Special Issue of the 30th Euromicro Conference on Real-Time Systems (ECRTS 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 2, pp. 7:1-7:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{wagemann_et_al:DARTS.4.2.7,
  author =	{W\"{a}gemann, Peter and Dietrich, Christian and Distler, Tobias and Ulbrich, Peter and Schr\"{o}der-Preikschat, Wolfgang},
  title =	{{Whole-System WCEC Analysis for Energy-Constrained Real-Time Systems (Artifact)}},
  pages =	{7:1--7:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{2},
  editor =	{W\"{a}gemann, Peter and Dietrich, Christian and Distler, Tobias and Ulbrich, Peter and Schr\"{o}der-Preikschat, Wolfgang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.2.7},
  URN =		{urn:nbn:de:0030-drops-89756},
  doi =		{10.4230/DARTS.4.2.7},
  annote =	{Keywords: energy-constrained real-time systems, worst-case energy consumption (WCEC), worst-case response energy consumption (WCRE), static whole-system analysi}
}
  • Refine by Author
  • 2 Dietrich, Christian
  • 2 Distler, Tobias
  • 2 Kuske, Dietrich
  • 2 Schröder-Preikschat, Wolfgang
  • 2 Schwarz, Christian
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Real-time systems
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Regular languages

  • Refine by Keyword
  • 2 energy-constrained real-time systems
  • 2 worst-case energy consumption (WCEC)
  • 2 worst-case response energy consumption (WCRE)
  • 1 Counting logic
  • 1 modal logic
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2018
  • 1 2020
  • 1 2024

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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact