27 Search Results for "Frank, Michael"

Document
Invited Talk
DOI: 10.4230/LIPIcs.CALCO.2023.3
A Tour on Ecumenical Systems (Invited Talk)

Authors: Elaine Pimentel and Luiz Carlos Pereira

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract
Ecumenism can be understood as a pursuit of unity, where diverse thoughts, ideas, or points of view coexist harmoniously. In logic, ecumenical systems refer, in a broad sense, to proof systems for combining logics. One captivating area of research over the past few decades has been the exploration of seamlessly merging classical and intuitionistic connectives, allowing them to coexist peacefully. In this paper, we will embark on a journey through ecumenical systems, drawing inspiration from Prawitz' seminal work [Dag Prawitz, 2015]. We will begin by elucidating Prawitz' concept of "ecumenism" and present a pure sequent calculus version of his system. Building upon this foundation, we will expand our discussion to incorporate alethic modalities, leveraging Simpson’s meta-logical characterization. This will enable us to propose several proof systems for ecumenical modal logics. We will conclude our tour with some discussion towards a term calculus proposal for the implicational propositional fragment of the ecumenical logic, the quest of automation using a framework based in rewriting logic, and an ecumenical view of proof-theoretic semantics.
Cite as

Elaine Pimentel and Luiz Carlos Pereira. A Tour on Ecumenical Systems (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 3:1-3:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{pimentel_et_al:LIPIcs.CALCO.2023.3,
  author =	{Pimentel, Elaine and Pereira, Luiz Carlos},
  title =	{{A Tour on Ecumenical Systems}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{3:1--3:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.3},
  URN =		{urn:nbn:de:0030-drops-188003},
  doi =		{10.4230/LIPIcs.CALCO.2023.3},
  annote =	{Keywords: Intuitionistic logic, classical logic, modal logic, ecumenical systems, proof theory}
}
Document
DOI: 10.4230/LITES.8.2.2
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
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}},
  booktitle =	{LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems},
  pages =	{04:1--04:34},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  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.7.1.1
Randomization as Mitigation of Directed Timing Inference Based Attacks on Time-Triggered Real-Time Systems with Task Replication

Authors: Kristin Krüger, Nils Vreman, Richard Pates, Martina Maggio, Marcus Völp, and Gerhard Fohler

Published in: LITES, Volume 7, Issue 1 (2021): Special Issue on Embedded System Security. Leibniz Transactions on Embedded Systems, Volume 7, Issue 1

Abstract
Time-triggered real-time systems achieve deterministic behavior using schedules that are constructed offline, based on scheduling constraints. Their deterministic behavior makes time-triggered systems suitable for usage in safety-critical environments, like avionics. However, this determinism also allows attackers to fine-tune attacks that can be carried out after studying the behavior of the system through side channels, targeting safety-critical victim tasks. Replication -- i.e., the execution of task variants across different cores -- is inherently able to tolerate both accidental and malicious faults (i.e. attacks) as long as these faults are independent of one another. Yet, targeted attacks on the timing behavior of tasks which utilize information gained about the system behavior violate the fault independence assumption fault tolerance is based on. This violation may give attackers the opportunity to compromise all replicas simultaneously, in particular if they can mount the attack from already compromised components. In this paper, we analyze vulnerabilities of time-triggered systems, focusing on safety-certified multicore real-time systems. We introduce two runtime mitigation strategies to withstand directed timing inference based attacks: (i) schedule randomization at slot level, and (ii) randomization within a set of offline constructed schedules. We evaluate these mitigation strategies with synthetic experiments and a real case study to show their effectiveness and practicality.
Cite as

Kristin Krüger, Nils Vreman, Richard Pates, Martina Maggio, Marcus Völp, and Gerhard Fohler. Randomization as Mitigation of Directed Timing Inference Based Attacks on Time-Triggered Real-Time Systems with Task Replication. In LITES, Volume 7, Issue 1 (2021): Special Issue on Embedded System Security. Leibniz Transactions on Embedded Systems, Volume 7, Issue 1, pp. 01:1-01:29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{kruger_et_al:LITES.7.1.1,
  author =	{Kr\"{u}ger, Kristin and Vreman, Nils and Pates, Richard and Maggio, Martina and V\"{o}lp, Marcus and Fohler, Gerhard},
  title =	{{Randomization as Mitigation of Directed Timing Inference Based Attacks on Time-Triggered Real-Time Systems with Task Replication}},
  booktitle =	{LITES, Volume 7, Issue 1 (2021): Special Issue on Embedded System Security},
  pages =	{01:1--01:29},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2021},
  volume =	{7},
  number =	{1},
  editor =	{Kr\"{u}ger, Kristin and Vreman, Nils and Pates, Richard and Maggio, Martina and V\"{o}lp, Marcus and Fohler, Gerhard},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.7.1.1},
  doi =		{10.4230/LITES.7.1.1},
  annote =	{Keywords: real-time systems, time-triggered systems, security}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2021.5
Chasing Puppies: Mobile Beacon Routing on Closed Curves

Authors: Mikkel Abrahamsen, Jeff Erickson, Irina Kostitsyna, Maarten Löffler, Tillmann Miltzow, Jérôme Urhausen, Jordi Vermeulen, and Giovanni Viglietta

Published in: LIPIcs, Volume 189, 37th International Symposium on Computational Geometry (SoCG 2021)

Abstract
We solve an open problem posed by Michael Biro at CCCG 2013 that was inspired by his and others’ work on beacon-based routing. Consider a human and a puppy on a simple closed curve in the plane. The human can walk along the curve at bounded speed and change direction as desired. The puppy runs with unbounded speed along the curve as long as the Euclidean straight-line distance to the human is decreasing, so that it is always at a point on the curve where the distance is locally minimal. Assuming that the curve is smooth (with some mild genericity constraints) or a simple polygon, we prove that the human can always catch the puppy in finite time.
Cite as

Mikkel Abrahamsen, Jeff Erickson, Irina Kostitsyna, Maarten Löffler, Tillmann Miltzow, Jérôme Urhausen, Jordi Vermeulen, and Giovanni Viglietta. Chasing Puppies: Mobile Beacon Routing on Closed Curves. In 37th International Symposium on Computational Geometry (SoCG 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 189, pp. 5:1-5:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{abrahamsen_et_al:LIPIcs.SoCG.2021.5,
  author =	{Abrahamsen, Mikkel and Erickson, Jeff and Kostitsyna, Irina and L\"{o}ffler, Maarten and Miltzow, Tillmann and Urhausen, J\'{e}r\^{o}me and Vermeulen, Jordi and Viglietta, Giovanni},
  title =	{{Chasing Puppies: Mobile Beacon Routing on Closed Curves}},
  booktitle =	{37th International Symposium on Computational Geometry (SoCG 2021)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-184-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{189},
  editor =	{Buchin, Kevin and Colin de Verdi\`{e}re, \'{E}ric},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2021.5},
  URN =		{urn:nbn:de:0030-drops-138046},
  doi =		{10.4230/LIPIcs.SoCG.2021.5},
  annote =	{Keywords: Beacon routing, navigation, generic smooth curves, puppies}
}
Document
DOI: 10.4230/LIPIcs.AofA.2020.20
Greedy Maximal Independent Sets via Local Limits

Authors: Michael Krivelevich, Tamás Mészáros, Peleg Michaeli, and Clara Shikhelman

Published in: LIPIcs, Volume 159, 31st International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2020)

Abstract
The random greedy algorithm for finding a maximal independent set in a graph has been studied extensively in various settings in combinatorics, probability, computer science - and even in chemistry. The algorithm builds a maximal independent set by inspecting the vertices of the graph one at a time according to a random order, adding the current vertex to the independent set if it is not connected to any previously added vertex by an edge. In this paper we present a natural and general framework for calculating the asymptotics of the proportion of the yielded independent set for sequences of (possibly random) graphs, involving a useful notion of local convergence. We use this framework both to give short and simple proofs for results on previously studied families of graphs, such as paths and binomial random graphs, and to study new ones, such as random trees. We conclude our work by analysing the random greedy algorithm more closely when the base graph is a tree. We show that in expectation, the cardinality of a random greedy independent set in the path is no larger than that in any other tree of the same order.
Cite as

Michael Krivelevich, Tamás Mészáros, Peleg Michaeli, and Clara Shikhelman. Greedy Maximal Independent Sets via Local Limits. In 31st International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 159, pp. 20:1-20:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{krivelevich_et_al:LIPIcs.AofA.2020.20,
  author =	{Krivelevich, Michael and M\'{e}sz\'{a}ros, Tam\'{a}s and Michaeli, Peleg and Shikhelman, Clara},
  title =	{{Greedy Maximal Independent Sets via Local Limits}},
  booktitle =	{31st International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2020)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-147-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{159},
  editor =	{Drmota, Michael and Heuberger, Clemens},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AofA.2020.20},
  URN =		{urn:nbn:de:0030-drops-120507},
  doi =		{10.4230/LIPIcs.AofA.2020.20},
  annote =	{Keywords: Greedy maximal independent set, random graph, local limit}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2020.13
Distribution Constraints: The Chase for Distributed Data

Authors: Gaetano Geck, Frank Neven, and Thomas Schwentick

Published in: LIPIcs, Volume 155, 23rd International Conference on Database Theory (ICDT 2020)

Abstract
This paper introduces a declarative framework to specify and reason about distributions of data over computing nodes in a distributed setting. More specifically, it proposes distribution constraints which are tuple and equality generating dependencies (tgds and egds) extended with node variables ranging over computing nodes. In particular, they can express co-partitioning constraints and constraints about range-based data distributions by using comparison atoms. The main technical contribution is the study of the implication problem of distribution constraints. While implication is undecidable in general, relevant fragments of so-called data-full constraints are exhibited for which the corresponding implication problems are complete for EXPTIME, PSPACE and NP. These results yield bounds on deciding parallel-correctness for conjunctive queries in the presence of distribution constraints.
Cite as

Gaetano Geck, Frank Neven, and Thomas Schwentick. Distribution Constraints: The Chase for Distributed Data. In 23rd International Conference on Database Theory (ICDT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 155, pp. 13:1-13:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{geck_et_al:LIPIcs.ICDT.2020.13,
  author =	{Geck, Gaetano and Neven, Frank and Schwentick, Thomas},
  title =	{{Distribution Constraints: The Chase for Distributed Data}},
  booktitle =	{23rd International Conference on Database Theory (ICDT 2020)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-139-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{155},
  editor =	{Lutz, Carsten and Jung, Jean Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2020.13},
  URN =		{urn:nbn:de:0030-drops-119378},
  doi =		{10.4230/LIPIcs.ICDT.2020.13},
  annote =	{Keywords: tuple-generating dependencies, chase, conjunctive queries, distributed evaluation}
}
Document
DOI: 10.4230/OASIcs.CERTS.2019.1
Combined Security and Schedulability Analysis for MILS Real-Time Critical Architectures

Authors: Ill-ham Atchadam, Frank Singhoff, Hai Nam Tran, Noura Bouzid, and Laurent Lemarchand

Published in: OASIcs, Volume 73, 4th International Workshop on Security and Dependability of Critical Embedded Real-Time Systems (CERTS 2019)

Abstract
Real-time critical systems have to comply with stringent timing constraints, otherwise, disastrous consequences can occur at runtime. A large effort has been made to propose models and tools to verify timing constraints by schedulability analysis at the early stages of system designs. Fewer efforts have been made on verifying the security properties in these systems despite the fact that sinister consequences can also happen if these properties are compromised. In this article, we investigate how to jointly verify security and timing constraints. We show how to model a security architecture (MILS) and how to verify both timing constraints and security properties. Schedulability is investigated by the mean of scheduling analysis methods implemented into the Cheddar scheduling analyzer. Experiments are conducted to show the impact that improving security has on the schedulability analysis.
Cite as

Ill-ham Atchadam, Frank Singhoff, Hai Nam Tran, Noura Bouzid, and Laurent Lemarchand. Combined Security and Schedulability Analysis for MILS Real-Time Critical Architectures. In 4th International Workshop on Security and Dependability of Critical Embedded Real-Time Systems (CERTS 2019). Open Access Series in Informatics (OASIcs), Volume 73, pp. 1:1-1:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{atchadam_et_al:OASIcs.CERTS.2019.1,
  author =	{Atchadam, Ill-ham and Singhoff, Frank and Tran, Hai Nam and Bouzid, Noura and Lemarchand, Laurent},
  title =	{{Combined Security and Schedulability Analysis for MILS Real-Time Critical Architectures}},
  booktitle =	{4th International Workshop on Security and Dependability of Critical Embedded Real-Time Systems (CERTS 2019)},
  pages =	{1:1--1:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-119-1},
  ISSN =	{2190-6807},
  year =	{2019},
  volume =	{73},
  editor =	{Asplund, Mikael and Paulitsch, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.CERTS.2019.1},
  URN =		{urn:nbn:de:0030-drops-108922},
  doi =		{10.4230/OASIcs.CERTS.2019.1},
  annote =	{Keywords: MILS (Multi Independent Levels of Security), RTCS (Real-Time Critical Systems), Security architecture and models, Scheduling analysis, Security analysis}
}
Document
DOI: 10.4230/LITES-v005-i001-a003
The Semantic Foundations and a Landscape of Cache-Persistence Analyses

Authors: Jan Reineke

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

Abstract
We clarify the notion of cache persistence and contribute to the understanding of persistence analysis for caches with least-recently-used replacement.To this end, we provide the first formal definition of persistence as a property of a trace semantics. Based on this trace semantics we introduce a semantics-based, i.e., abstract-interpretation-based persistence analysis framework.We identify four basic persistence analyses and prove their correctness as instances of this analysis framework.Combining these basic persistence analyses via two generic cooperation mechanisms yields a lattice of ten persistence analyses.Notably, this lattice contains all persistence analyses previously described in the literature. As a consequence, we obtain uniform correctness proofs for all prior analyses and a precise understanding of how and why these analyses work, as well as how they relate to each other in terms of precision.
Cite as

Jan Reineke. The Semantic Foundations and a Landscape of Cache-Persistence Analyses. In LITES, Volume 5, Issue 1 (2018). Leibniz Transactions on Embedded Systems, Volume 5, Issue 1, pp. 03:1-03:52, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{reineke:LITES-v005-i001-a003,
  author =	{Reineke, Jan},
  title =	{{The Semantic Foundations and a Landscape of Cache-Persistence Analyses}},
  booktitle =	{LITES, Volume 5, Issue 1 (2018)},
  pages =	{03:1--03:52},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2018},
  volume =	{5},
  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-v005-i001-a003},
  doi =		{10.4230/LITES-v005-i001-a003},
  annote =	{Keywords: caches, persistence analysis, WCET analysis}
}
Document
Tool Description
DOI: 10.4230/OASIcs.ICLP.2017.5
Logic Programming with Max-Clique and its Application to Graph Coloring (Tool Description)

Authors: Michael Codish, Michael Frank, Amit Metodi, and Morad Muslimany

Published in: OASIcs, Volume 58, Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017)

Abstract
This paper presents pl-cliquer, a Prolog interface to the cliquer tool for the maximum clique problem. Using pl-cliquer facilitates a programming style that allows logic programs to integrate with other tools such as: Boolean satisfiability solvers, finite domain constraint solvers, and graph isomorphism tools. We illustrate this programming style to solve the Graph Coloring problem, applying a symmetry break that derives from finding a maximum clique in the input graph. We present an experimentation of the resulting Graph Coloring solver on two benchmarks, one from the graph coloring community and the other from the examination timetabling community. The implementation of pl-cliquer consists of two components: A lightweight C interface, connecting cliquer's C library and Prolog, and a Prolog module which loads the library. The complete tool is available as a SWI-Prolog module.
Cite as

Michael Codish, Michael Frank, Amit Metodi, and Morad Muslimany. Logic Programming with Max-Clique and its Application to Graph Coloring (Tool Description). In Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017). Open Access Series in Informatics (OASIcs), Volume 58, pp. 5:1-5:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{codish_et_al:OASIcs.ICLP.2017.5,
  author =	{Codish, Michael and Frank, Michael and Metodi, Amit and Muslimany, Morad},
  title =	{{Logic Programming with Max-Clique and its Application to Graph Coloring}},
  booktitle =	{Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017)},
  pages =	{5:1--5:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-058-3},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{58},
  editor =	{Rocha, Ricardo and Son, Tran Cao and Mears, Christopher and Saeedloei, Neda},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2017.5},
  URN =		{urn:nbn:de:0030-drops-84559},
  doi =		{10.4230/OASIcs.ICLP.2017.5},
  annote =	{Keywords: Logic Programming, Constraints, Maximum Clique}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2017.1
Ontology-Mediated Query Answering over Temporal Data: A Survey (Invited Talk)

Authors: Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev

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

Abstract
We discuss the use of various temporal knowledge representation formalisms for ontology-mediated query answering over temporal data. In particular, we analyse ontology and query languages based on the linear temporal logic LTL, the multi-dimensional Halpern-Shoham interval temporal logic HS_n, as well as the metric temporal logic MTL. Our main focus is on the data complexity of answering temporal ontology-mediated queries and their rewritability into standard first-order and datalog queries.
Cite as

Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. Ontology-Mediated Query Answering over Temporal Data: A Survey (Invited Talk). In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 1:1-1:37, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{artale_et_al:LIPIcs.TIME.2017.1,
  author =	{Artale, Alessandro and Kontchakov, Roman and Kovtunova, Alisa and Ryzhikov, Vladislav and Wolter, Frank and Zakharyaschev, Michael},
  title =	{{Ontology-Mediated Query Answering over Temporal Data: A Survey}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{1:1--1:37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.1},
  URN =		{urn:nbn:de:0030-drops-79338},
  doi =		{10.4230/LIPIcs.TIME.2017.1},
  annote =	{Keywords: Description Logic, Temporal Logic, Ontology Mediated Query Answering, Data Complexity}
}
Document
DOI: 10.4230/LITES-v004-i002-a001
Dynamic and Static Task Allocation for Hard Real-Time Video Stream Decoding on NoCs

Authors: Hashan R. Mendis, Neil C. Audsley, and Leandro Soares Indrusiak

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

Abstract
Hard real-time (HRT) video systems require admission control decisions that rely on two factors. Firstly, schedulability analysis of the data-dependent, communicating tasks within the application need to be carried out in order to guarantee timing and predictability. Secondly, the allocation of the tasks to multi-core processing elements would generate different results in the schedulability analysis. Due to the conservative nature of the state-of-the-art schedulability analysis of tasks and message flows, and the unpredictability in the application, the system resources are often under-utilised. In this paper we propose two blocking-aware dynamic task allocation techniques that exploit application and platform characteristics, in order to increase the number of simultaneous, fully schedulable, video streams handled by the system. A novel, worst-case response time aware, search-based, static hard real-time task mapper is introduced to act as an upper-baseline to the proposed techniques. Further evaluations are carried out against existing heuristic-based dynamic mappers. Improvements to the admission rates and the system utilisation under a range of different workloads and platform sizes are explored.
Cite as

Hashan R. Mendis, Neil C. Audsley, and Leandro Soares Indrusiak. Dynamic and Static Task Allocation for Hard Real-Time Video Stream Decoding on NoCs. In LITES, Volume 4, Issue 2 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 2, pp. 01:1-01:25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{mendis_et_al:LITES-v004-i002-a001,
  author =	{Mendis, Hashan R. and Audsley, Neil C. and Indrusiak, Leandro Soares},
  title =	{{Dynamic and Static Task Allocation for Hard Real-Time Video Stream Decoding on NoCs}},
  booktitle =	{LITES, Volume 4, Issue 2 (2017)},
  pages =	{01:1--01:25},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{2},
  editor =	{Mendis, Hashan R. and Audsley, Neil C. and Indrusiak, Leandro Soares},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i002-a001},
  doi =		{10.4230/LITES-v004-i002-a001},
  annote =	{Keywords: Real-time multimedia, Task mapping, Network-on-chip}
}
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}},
  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
DOI: 10.4230/OASIcs.ICLP.2016.21
Methods for Solving Extremal Problems in Practice

Authors: Michael Frank

Published in: OASIcs, Volume 52, Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)

Abstract
During the 20 th century there has been an incredible progress in solving theoretically hard problems in practice. One of the most prominent examples is the DPLL algorithm and its derivatives to solve the Boolean satisfiability problem, which can handle instances with millions of variables and clauses in reasonable time, notwithstanding the theoretical difficulty of solving the problem. Despite this progress, there are classes of problems that contain especially hard instances, which have remained open for decades despite their relative small size. One such class is the class of extremal problems, which typically involve finding a combinatorial object under some constraints (e.g, the search for Ramsey numbers). In recent years, a number of specialized methods have emerged to tackle extremal problems. Most of these methods are applied to a specific problem, despite the fact there is a great deal in common between different problems. Following a meticulous examination of these methods, we would like to extend them to handle general extremal problems. Further more, we would like to offer ways to exploit the general structure of extremal problems in order to develop constraints and symmetry breaking techniques which will, hopefully, improve existing tools. The latter point is of immense importance in the context of extremal problems, which often hamper existing tools when there is a great deal of symmetry in the search space, or when not enough is known of the problem structure. For example, if a graph is a solution to a problem instance, in many cases any isomorphic graph will also be a solution. In such cases, existing methods can usually be applied only if the model excludes symmetries.
Cite as

Michael Frank. Methods for Solving Extremal Problems in Practice. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 21:1-21:6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{frank:OASIcs.ICLP.2016.21,
  author =	{Frank, Michael},
  title =	{{Methods for Solving Extremal Problems in Practice}},
  booktitle =	{Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)},
  pages =	{21:1--21:6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-007-1},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{52},
  editor =	{Carro, Manuel and King, Andy and Saeedloei, Neda and De Vos, Marina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2016.21},
  URN =		{urn:nbn:de:0030-drops-67513},
  doi =		{10.4230/OASIcs.ICLP.2016.21},
  annote =	{Keywords: Extremal Problems, Constraints, SAT Solving, Logic Programming, Parallelism}
}
Document
DOI: 10.4230/LITES-v003-i001-a003
Modeling Power Consumption and Temperature in TLM Models

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

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

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

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

Copy BibTex To Clipboard

@Article{moy_et_al:LITES-v003-i001-a003,
  author =	{Moy, Matthieu and Helmstetter, Claude and Bouhadiba, Tayeb and Maraninchi, Florence},
  title =	{{Modeling Power Consumption and Temperature in TLM Models}},
  booktitle =	{LITES, Volume 3, Issue 1 (2016)},
  pages =	{03:1--03:29},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2016},
  volume =	{3},
  number =	{1},
  editor =	{Moy, Matthieu and Helmstetter, Claude and Bouhadiba, Tayeb and Maraninchi, Florence},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v003-i001-a003},
  doi =		{10.4230/LITES-v003-i001-a003},
  annote =	{Keywords: Power consumption, Temperature control, Virtual prototype, SystemC, Transactional modeling}
}
  • Refine by Author
  • 3 Reineke, Jan
  • 2 Frank, Michael
  • 1 Abella, Jaume
  • 1 Abrahamsen, Mikkel
  • 1 Albayrak, Sahin
  • Show More...

  • Refine by Classification
  • 4 Computer systems organization → Real-time system architecture
  • 2 Hardware → Safety critical systems
  • 2 Theory of computation → Caching and paging algorithms
  • 2 Theory of computation → Logic and verification
  • 1 Computer systems organization → Embedded and cyber-physical systems
  • Show More...

  • Refine by Keyword
  • 2 Constraints
  • 2 Logic Programming
  • 2 Real-time systems
  • 2 Service-oriented computing
  • 2 WCET analysis
  • Show More...

  • Refine by Type
  • 27 document

  • Refine by Publication Year
  • 3 2006
  • 3 2016
  • 3 2017
  • 2 2007
  • 2 2010
  • 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