12 Search Results for "Fernández-Baca, David"

Document
DOI: 10.4230/LIPIcs.SEA.2023.8
Noisy Sorting Without Searching: Data Oblivious Sorting with Comparison Errors

Authors: Ramtin Afshar, Michael Dillencourt, Michael T. Goodrich, and Evrim Ozel

Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)

Abstract
We provide and study several algorithms for sorting an array of n comparable distinct elements subject to probabilistic comparison errors. In this model, the comparison of two elements returns the wrong answer according to a fixed probability, p_e < 1/2, and otherwise returns the correct answer. The dislocation of an element is the distance between its position in a given (current or output) array and its position in a sorted array. There are various algorithms that can be utilized for sorting or near-sorting elements subject to probabilistic comparison errors, but these algorithms are not data oblivious because they all make heavy use of noisy binary searching. In this paper, we provide new methods for sorting with comparison errors that are data oblivious while avoiding the use of noisy binary search methods. In addition, we experimentally compare our algorithms and other sorting algorithms.
Cite as

Ramtin Afshar, Michael Dillencourt, Michael T. Goodrich, and Evrim Ozel. Noisy Sorting Without Searching: Data Oblivious Sorting with Comparison Errors. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 8:1-8:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{afshar_et_al:LIPIcs.SEA.2023.8,
  author =	{Afshar, Ramtin and Dillencourt, Michael and Goodrich, Michael T. and Ozel, Evrim},
  title =	{{Noisy Sorting Without Searching: Data Oblivious Sorting with Comparison Errors}},
  booktitle =	{21st International Symposium on Experimental Algorithms (SEA 2023)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-279-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{265},
  editor =	{Georgiadis, Loukas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.8},
  URN =		{urn:nbn:de:0030-drops-183585},
  doi =		{10.4230/LIPIcs.SEA.2023.8},
  annote =	{Keywords: sorting, algorithms, randomization, experimentation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.28
Concurrent Realizability on Conjunctive Structures

Authors: Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define a reference model of this structure as induced by a standard process calculus and we use this model to prove that parallel composition cannot be defined from the conjunctive structure alone.
Cite as

Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey. Concurrent Realizability on Conjunctive Structures. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 28:1-28:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{beffara_et_al:LIPIcs.FSCD.2023.28,
  author =	{Beffara, Emmanuel and Castro, F\'{e}lix and Guillermo, Mauricio and Miquey, \'{E}tienne},
  title =	{{Concurrent Realizability on Conjunctive Structures}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.28},
  URN =		{urn:nbn:de:0030-drops-180124},
  doi =		{10.4230/LIPIcs.FSCD.2023.28},
  annote =	{Keywords: Realizability, Process Algebras, Concurrent Processes, Linear Logic}
}
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
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2022.69
Tolerant Bipartiteness Testing in Dense Graphs

Authors: Arijit Ghosh, Gopinath Mishra, Rahul Raychaudhury, and Sayantan Sen

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
Bipartite testing has been a central problem in the area of property testing since its inception in the seminal work of Goldreich, Goldwasser, and Ron. Though the non-tolerant version of bipartite testing has been extensively studied in the literature, the tolerant variant is not well understood. In this paper, we consider the following version of tolerant bipartite testing problem: Given two parameters ε, δ ∈ (0,1), with δ > ε, and access to the adjacency matrix of a graph G, we have to decide whether G can be made bipartite by editing at most ε n² entries of the adjacency matrix of G, or we have to edit at least δ n² entries of the adjacency matrix to make G bipartite. In this paper, we prove that for δ = (2+Ω(1))ε, tolerant bipartite testing can be decided by performing 𝒪̃(1/ε³) many adjacency queries and in 2^𝒪̃(1/ε) time complexity. This improves upon the state-of-the-art query and time complexities of this problem of 𝒪̃(1/ε⁶) and 2^𝒪̃(1/ε²), respectively, due to Alon, Fernandez de la Vega, Kannan and Karpinski, where 𝒪̃(⋅) hides a factor polynomial in log (1/ε).
Cite as

Arijit Ghosh, Gopinath Mishra, Rahul Raychaudhury, and Sayantan Sen. Tolerant Bipartiteness Testing in Dense Graphs. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 69:1-69:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ghosh_et_al:LIPIcs.ICALP.2022.69,
  author =	{Ghosh, Arijit and Mishra, Gopinath and Raychaudhury, Rahul and Sen, Sayantan},
  title =	{{Tolerant Bipartiteness Testing in Dense Graphs}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{69:1--69:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.69},
  URN =		{urn:nbn:de:0030-drops-164101},
  doi =		{10.4230/LIPIcs.ICALP.2022.69},
  annote =	{Keywords: Tolerant Testing, Bipartite Testing, Query Complexity, Graph Property Testing}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.19
Dynamic Cantor Derivative Logic

Authors: David Fernández-Duque and Yoàv Montacute

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
Topological semantics for modal logic based on the Cantor derivative operator gives rise to derivative logics, also referred to as d-logics. Unlike logics based on the topological closure operator, d-logics have not previously been studied in the framework of dynamical systems, which are pairs (X,f) consisting of a topological space X equipped with a continuous function f: X → X. We introduce the logics wK4C, K4C and GLC and show that they all have the finite Kripke model property and are sound and complete with respect to the d-semantics in this dynamical setting. In particular, we prove that wK4C is the d-logic of all dynamic topological systems, K4C is the d-logic of all T_D dynamic topological systems, and GLC is the d-logic of all dynamic topological systems based on a scattered space. We also prove a general result for the case where f is a homeomorphism, which in particular yields soundness and completeness for the corresponding systems wK4H, K4H and GLH. The main contribution of this work is the foundation of a general proof method for finite model property and completeness of dynamic topological d-logics. Furthermore, our result for GLC constitutes the first step towards a proof of completeness for the trimodal topo-temporal language with respect to a finite axiomatisation - something known to be impossible over the class of all spaces.
Cite as

David Fernández-Duque and Yoàv Montacute. Dynamic Cantor Derivative Logic. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 19:1-19:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fernandezduque_et_al:LIPIcs.CSL.2022.19,
  author =	{Fern\'{a}ndez-Duque, David and Montacute, Yo\`{a}v},
  title =	{{Dynamic Cantor Derivative Logic}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.19},
  URN =		{urn:nbn:de:0030-drops-157397},
  doi =		{10.4230/LIPIcs.CSL.2022.19},
  annote =	{Keywords: dynamic topological logic, Cantor derivative, temporal logic, modal logic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.6
An Approximation Algorithm for the Matrix Tree Multiplication Problem

Authors: Mahmoud Abo-Khamis, Ryan Curtin, Sungjin Im, Benjamin Moseley, Hung Ngo, Kirk Pruhs, and Alireza Samadian

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
We consider the Matrix Tree Multiplication problem. This problem is a generalization of the classic Matrix Chain Multiplication problem covered in the dynamic programming chapter of many introductory algorithms textbooks. An instance of the Matrix Tree Multiplication problem consists of a rooted tree with a matrix associated with each edge. The output is, for each leaf in the tree, the product of the matrices on the chain/path from the root to that leaf. Matrix multiplications that are shared between various chains need only be computed once, potentially being shared between different root to leaf chains. Algorithms are evaluated by the number of scalar multiplications performed. Our main result is a linear time algorithm for which the number of scalar multiplications performed is at most 15 times the optimal number of scalar multiplications.
Cite as

Mahmoud Abo-Khamis, Ryan Curtin, Sungjin Im, Benjamin Moseley, Hung Ngo, Kirk Pruhs, and Alireza Samadian. An Approximation Algorithm for the Matrix Tree Multiplication Problem. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 6:1-6:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{abokhamis_et_al:LIPIcs.MFCS.2021.6,
  author =	{Abo-Khamis, Mahmoud and Curtin, Ryan and Im, Sungjin and Moseley, Benjamin and Ngo, Hung and Pruhs, Kirk and Samadian, Alireza},
  title =	{{An Approximation Algorithm for the Matrix Tree Multiplication Problem}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{6:1--6:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.6},
  URN =		{urn:nbn:de:0030-drops-144464},
  doi =		{10.4230/LIPIcs.MFCS.2021.6},
  annote =	{Keywords: Matrix Multiplication, Approximation Algorithm}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.77
Graph Spanners in the Message-Passing Model

Authors: Manuel Fernández V, David P. Woodruff, and Taisuke Yasuda

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
Graph spanners are sparse subgraphs which approximately preserve all pairwise shortest-path distances in an input graph. The notion of approximation can be additive, multiplicative, or both, and many variants of this problem have been extensively studied. We study the problem of computing a graph spanner when the edges of the input graph are distributed across two or more sites in an arbitrary, possibly worst-case partition, and the goal is for the sites to minimize the communication used to output a spanner. We assume the message-passing model of communication, for which there is a point-to-point link between all pairs of sites as well as a coordinator who is responsible for producing the output. We stress that the subset of edges that each site has is not related to the network topology, which is fixed to be point-to-point. While this model has been extensively studied for related problems such as graph connectivity, it has not been systematically studied for graph spanners. We present the first tradeoffs for total communication versus the quality of the spanners computed, for two or more sites, as well as for additive and multiplicative notions of distortion. We show separations in the communication complexity when edges are allowed to occur on multiple sites, versus when each edge occurs on at most one site. We obtain nearly tight bounds (up to polylog factors) for the communication of additive 2-spanners in both the with and without duplication models, multiplicative (2k-1)-spanners in the with duplication model, and multiplicative 3 and 5-spanners in the without duplication model. Our lower bound for multiplicative 3-spanners employs biregular bipartite graphs rather than the usual Erdős girth conjecture graphs and may be of wider interest.
Cite as

Manuel Fernández V, David P. Woodruff, and Taisuke Yasuda. Graph Spanners in the Message-Passing Model. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 77:1-77:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fernandezv_et_al:LIPIcs.ITCS.2020.77,
  author =	{Fern\'{a}ndez V, Manuel and Woodruff, David P. and Yasuda, Taisuke},
  title =	{{Graph Spanners in the Message-Passing Model}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{77:1--77:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.77},
  URN =		{urn:nbn:de:0030-drops-117620},
  doi =		{10.4230/LIPIcs.ITCS.2020.77},
  annote =	{Keywords: Graph spanners, Message-passing model, Communication complexity}
}
Document
DOI: 10.4230/LIPIcs.TIME.2019.6
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations

Authors: Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
We argue that European transport regulations can be formalized within the Sigma^1_1 fragment of monadic second order logic, and possibly weaker fragments including linear temporal logic. We consider several articles in the regulation to verify these claims.
Cite as

Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 6:1-6:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dealmeidaborges_et_al:LIPIcs.TIME.2019.6,
  author =	{de Almeida Borges, Ana and Conejero Rodr{\'\i}guez, Juan Jos\'{e} and Fern\'{a}ndez-Duque, David and Gonz\'{a}lez Bedmar, Mireia and Joosten, Joost J.},
  title =	{{The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.6},
  URN =		{urn:nbn:de:0030-drops-113649},
  doi =		{10.4230/LIPIcs.TIME.2019.6},
  annote =	{Keywords: linear temporal logic, monadic second order logic, formalized law, transport regulations}
}
Document
APPROX
DOI: 10.4230/LIPIcs.APPROX-RANDOM.2019.1
The Query Complexity of Mastermind with l_p Distances

Authors: Manuel Fernández V, David P. Woodruff, and Taisuke Yasuda

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

Abstract
Consider a variant of the Mastermind game in which queries are l_p distances, rather than the usual Hamming distance. That is, a codemaker chooses a hidden vector y in {-k,-k+1,...,k-1,k}^n and answers to queries of the form ||y-x||_p where x in {-k,-k+1,...,k-1,k}^n. The goal is to minimize the number of queries made in order to correctly guess y. In this work, we show an upper bound of O(min{n,(n log k)/(log n)}) queries for any real 1<=p<infty and O(n) queries for p=infty. To prove this result, we in fact develop a nonadaptive polynomial time algorithm that works for a natural class of separable distance measures, i.e., coordinate-wise sums of functions of the absolute value. We also show matching lower bounds up to constant factors, even for adaptive algorithms for the approximation version of the problem, in which the problem is to output y' such that ||y'-y||_p <= R for any R <= k^{1-epsilon}n^{1/p} for constant epsilon>0. Thus, essentially any approximation of this problem is as hard as finding the hidden vector exactly, up to constant factors. Finally, we show that for the noisy version of the problem, i.e., the setting when the codemaker answers queries with any q = (1 +/- epsilon)||y-x||_p, there is no query efficient algorithm.
Cite as

Manuel Fernández V, David P. Woodruff, and Taisuke Yasuda. The Query Complexity of Mastermind with l_p Distances. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 145, pp. 1:1-1:11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{fernandezv_et_al:LIPIcs.APPROX-RANDOM.2019.1,
  author =	{Fern\'{a}ndez V, Manuel and Woodruff, David P. and Yasuda, Taisuke},
  title =	{{The Query Complexity of Mastermind with l\underlinep Distances}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2019)},
  pages =	{1:1--1:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-125-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{145},
  editor =	{Achlioptas, Dimitris and V\'{e}gh, L\'{a}szl\'{o} A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2019.1},
  URN =		{urn:nbn:de:0030-drops-112165},
  doi =		{10.4230/LIPIcs.APPROX-RANDOM.2019.1},
  annote =	{Keywords: Mastermind, Query Complexity, l\underlinep Distance}
}
Document
DOI: 10.4230/LITES-v006-i001-a003
A Survey of Probabilistic Timing Analysis Techniques for Real-Time Systems

Authors: Robert I. Davis and Liliana Cucu-Grosjean

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

Abstract
This survey covers probabilistic timing analysis techniques for real-time systems. It reviews and critiques the key results in the field from its origins in 2000 to the latest research published up to the end of August 2018. The survey provides a taxonomy of the different methods used, and a classification of existing research. A detailed review is provided covering the main subject areas: static probabilistic timing analysis, measurement-based probabilistic timing analysis, and hybrid methods. In addition, research on supporting mechanisms and techniques, case studies, and evaluations is also reviewed. The survey concludes by identifying open issues, key challenges and possible directions for future research.
Cite as

Robert I. Davis and Liliana Cucu-Grosjean. A Survey of Probabilistic Timing Analysis Techniques for Real-Time Systems. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 03:1-03:60, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{davis_et_al:LITES-v006-i001-a003,
  author =	{Davis, Robert I. and Cucu-Grosjean, Liliana},
  title =	{{A Survey of Probabilistic Timing Analysis Techniques for Real-Time Systems}},
  booktitle =	{LITES, Volume 6, Issue 1 (2019)},
  pages =	{03:1--03:60},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2019},
  volume =	{6},
  number =	{1},
  editor =	{Davis, Robert I. and Cucu-Grosjean, Liliana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v006-i001-a003},
  doi =		{10.4230/LITES-v006-i001-a003},
  annote =	{Keywords: Probabilistic, real-time, timing analysis}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.14
A Decidable Intuitionistic Temporal Logic

Authors: Joseph Boudou, Martín Diéguez, and David Fernández-Duque

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We introduce the logic ITL^e, an intuitionistic temporal logic based on structures (W,R,S), where R is used to interpret intuitionistic implication and S is an R-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for ITL^e are decidable. We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a 'persistent' version of the logic, ITL^p, whose models are similar to Cartesian products. We prove that, unlike ITL^e, ITL^p does not have the finite model property.
Cite as

Joseph Boudou, Martín Diéguez, and David Fernández-Duque. A Decidable Intuitionistic Temporal Logic. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 14:1-14:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{boudou_et_al:LIPIcs.CSL.2017.14,
  author =	{Boudou, Joseph and Di\'{e}guez, Mart{\'\i}n and Fern\'{a}ndez-Duque, David},
  title =	{{A Decidable Intuitionistic Temporal Logic}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.14},
  URN =		{urn:nbn:de:0030-drops-77016},
  doi =		{10.4230/LIPIcs.CSL.2017.14},
  annote =	{Keywords: intuitionistic logic, temporal logic, products of modal logics}
}
Document
DOI: 10.4230/LIPIcs.CPM.2016.12
Fast Compatibility Testing for Rooted Phylogenetic Trees

Authors: Yun Deng and David Fernández-Baca

Published in: LIPIcs, Volume 54, 27th Annual Symposium on Combinatorial Pattern Matching (CPM 2016)

Abstract
We consider the following basic problem in phylogenetic tree construction. Let $\mathcal P = {T_1, ..., T_k} be a collection of rooted phylogenetic trees over various subsets of a set of species. The tree compatibility problem asks whether there is a tree T with the following property: for each i in {1, ..., k}, T_i can be obtained from the restriction of T to the species set of T_i by contracting zero or more edges. If such a tree T exists, we say that P is compatible. We give a ~O(M_P) algorithm for the tree compatibility problem, where M_P is the total number of nodes and edges in P. Unlike previous algorithms for this problem, the running time of our method does not depend on the degrees of the nodes in the input trees. Thus, it is equally fast on highly resolved and highly unresolved trees.
Cite as

Yun Deng and David Fernández-Baca. Fast Compatibility Testing for Rooted Phylogenetic Trees. In 27th Annual Symposium on Combinatorial Pattern Matching (CPM 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 54, pp. 12:1-12:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{deng_et_al:LIPIcs.CPM.2016.12,
  author =	{Deng, Yun and Fern\'{a}ndez-Baca, David},
  title =	{{Fast Compatibility Testing for Rooted Phylogenetic Trees}},
  booktitle =	{27th Annual Symposium on Combinatorial Pattern Matching (CPM 2016)},
  pages =	{12:1--12:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-012-5},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{54},
  editor =	{Grossi, Roberto and Lewenstein, Moshe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2016.12},
  URN =		{urn:nbn:de:0030-drops-60884},
  doi =		{10.4230/LIPIcs.CPM.2016.12},
  annote =	{Keywords: Algorithms, computational biology, phylogenetics}
}
  • Refine by Author
  • 3 Fernández-Duque, David
  • 2 Fernández V, Manuel
  • 2 Woodruff, David P.
  • 2 Yasuda, Taisuke
  • 1 Abo-Khamis, Mahmoud
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Design and analysis of algorithms
  • 2 Theory of computation → Modal and temporal logics
  • 1 Applied computing → Law
  • 1 Computer systems organization → Real-time systems
  • 1 Computing methodologies → Distributed programming languages
  • Show More...

  • Refine by Keyword
  • 2 Query Complexity
  • 2 temporal logic
  • 1 Active Objects
  • 1 Algorithms
  • 1 Approximation Algorithm
  • Show More...

  • Refine by Type
  • 12 document

  • Refine by Publication Year
  • 3 2019
  • 3 2022
  • 2 2023
  • 1 2016
  • 1 2017
  • 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