35 Search Results for "Schneider, Thomas"

Volume

LIPIcs, Volume 90

24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

TIME 2017, October 16-18, 2017, Mons, Belgium

Editors: Sven Schewe, Thomas Schneider, and Jef Wijsen

Document
DOI: 10.4230/LIPIcs.ESA.2021.6
Parallel Computation of Combinatorial Symmetries

Authors: Markus Anders and Pascal Schweitzer

Published in: LIPIcs, Volume 204, 29th Annual European Symposium on Algorithms (ESA 2021)

Abstract
In practice symmetries of combinatorial structures are computed by transforming the structure into an annotated graph whose automorphisms correspond exactly to the desired symmetries. An automorphism solver is then employed to compute the automorphism group of the constructed graph. Such solvers have been developed for over 50 years, and highly efficient sequential, single core tools are available. However no competitive parallel tools are available for the task. We introduce a new parallel randomized algorithm that is based on a modification of the individualization-refinement paradigm used by sequential solvers. The use of randomization crucially enables parallelization. We report extensive benchmark results that show that our solver is competitive to state-of-the-art solvers on a single thread, while scaling remarkably well with the use of more threads. This results in order-of-magnitude improvements on many graph classes over state-of-the-art solvers. In fact, our tool is the first parallel graph automorphism tool that outperforms current sequential tools.
Cite as

Markus Anders and Pascal Schweitzer. Parallel Computation of Combinatorial Symmetries. In 29th Annual European Symposium on Algorithms (ESA 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 204, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.ESA.2021.6,
  author =	{Anders, Markus and Schweitzer, Pascal},
  title =	{{Parallel Computation of Combinatorial Symmetries}},
  booktitle =	{29th Annual European Symposium on Algorithms (ESA 2021)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-204-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{204},
  editor =	{Mutzel, Petra and Pagh, Rasmus and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2021.6},
  URN =		{urn:nbn:de:0030-drops-145875},
  doi =		{10.4230/LIPIcs.ESA.2021.6},
  annote =	{Keywords: graph isomorphism, automorphism groups, algorithm engineering, parallel algorithms}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.3
Approximately Strategyproof Tournament Rules: On Large Manipulating Sets and Cover-Consistence

Authors: Ariel Schvartzman, S. Matthew Weinberg, Eitan Zlatin, and Albert Zuo

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

Abstract
We consider the manipulability of tournament rules, in which n teams play a round robin tournament and a winner is (possibly randomly) selected based on the outcome of all binom{n}{2} matches. Prior work defines a tournament rule to be k-SNM-α if no set of ≤ k teams can fix the ≤ binom{k}{2} matches among them to increase their probability of winning by >α and asks: for each k, what is the minimum α(k) such that a Condorcet-consistent (i.e. always selects a Condorcet winner when one exists) k-SNM-α(k) tournament rule exists? A simple example witnesses that α(k) ≥ (k-1)/(2k-1) for all k, and [Jon Schneider et al., 2017] conjectures that this is tight (and prove it is tight for k=2). Our first result refutes this conjecture: there exists a sufficiently large k such that no Condorcet-consistent tournament rule is k-SNM-1/2. Our second result leverages similar machinery to design a new tournament rule which is k-SNM-2/3 for all k (and this is the first tournament rule which is k-SNM-(<1) for all k). Our final result extends prior work, which proves that single-elimination bracket with random seeding is 2-SNM-1/3 [Jon Schneider et al., 2017], in a different direction by seeking a stronger notion of fairness than Condorcet-consistence. We design a new tournament rule, which we call Randomized-King-of-the-Hill, which is 2-SNM-1/3 and cover-consistent (the winner is an uncovered team with probability 1).
Cite as

Ariel Schvartzman, S. Matthew Weinberg, Eitan Zlatin, and Albert Zuo. Approximately Strategyproof Tournament Rules: On Large Manipulating Sets and Cover-Consistence. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{schvartzman_et_al:LIPIcs.ITCS.2020.3,
  author =	{Schvartzman, Ariel and Weinberg, S. Matthew and Zlatin, Eitan and Zuo, Albert},
  title =	{{Approximately Strategyproof Tournament Rules: On Large Manipulating Sets and Cover-Consistence}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{3:1--3:25},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.3},
  URN =		{urn:nbn:de:0030-drops-116881},
  doi =		{10.4230/LIPIcs.ITCS.2020.3},
  annote =	{Keywords: Tournament design, Non-manipulability, Cover-consistence, Strategyproofness}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.COSIT.2019.28
Granular Spatial Calculi of Relative Directions or Movements with Parallelism: Consistent Account (Short Paper)

Authors: Reinhard Moratz, Leif Sabellek, and Thomas Schneider

Published in: LIPIcs, Volume 142, 14th International Conference on Spatial Information Theory (COSIT 2019)

Abstract
The OPRA* calculus family, originally suggested by Frank Dylla, adds parallelism to the OPRA calculus family which is very popular in Qualitative Spatio-temporal Reasoning (QSTR). Adding parallelism enables the direct representation of parallel moving objects, which is relevant in many applications like traffic monitoring. However, it turned out that it is hard to derive a sound geometric analysis. So far no sound spatial reasoning was supported. Our new generic analysis based on combining condensed semantics lower bounds with upper bounds from algebraic mappings of related calculi already leads to a close and sound approximization. This approximization can be easily augmented with a manual analysis of few geometrically underconstrained cases and then yields a complete analysis of possible configurations in this oriented point framework. This for the first time enables sound standard QSTR constraint reasoning for the OPRA* calculus family.
Cite as

Reinhard Moratz, Leif Sabellek, and Thomas Schneider. Granular Spatial Calculi of Relative Directions or Movements with Parallelism: Consistent Account (Short Paper). In 14th International Conference on Spatial Information Theory (COSIT 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 142, pp. 28:1-28:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{moratz_et_al:LIPIcs.COSIT.2019.28,
  author =	{Moratz, Reinhard and Sabellek, Leif and Schneider, Thomas},
  title =	{{Granular Spatial Calculi of Relative Directions or Movements with Parallelism: Consistent Account}},
  booktitle =	{14th International Conference on Spatial Information Theory (COSIT 2019)},
  pages =	{28:1--28:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-115-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{142},
  editor =	{Timpf, Sabine and Schlieder, Christoph and Kattenbeck, Markus and Ludwig, Bernd and Stewart, Kathleen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2019.28},
  URN =		{urn:nbn:de:0030-drops-111206},
  doi =		{10.4230/LIPIcs.COSIT.2019.28},
  annote =	{Keywords: qualitative spatial-temporal reasoning, composition table, condensed semantics, homomorphic embeddings}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2018.15
Querying the Unary Negation Fragment with Regular Path Expressions

Authors: Jean Christoph Jung, Carsten Lutz, Mauricio Martel, and Thomas Schneider

Published in: LIPIcs, Volume 98, 21st International Conference on Database Theory (ICDT 2018)

Abstract
The unary negation fragment of first-order logic (UNFO) has recently been proposed as a generalization of modal logic that shares many of its good computational and model-theoretic properties. It is attractive from the perspective of database theory because it can express conjunctive queries (CQs) and ontologies formulated in many description logics (DLs). Both are relevant for ontology-mediated querying and, in fact, CQ evaluation under UNFO ontologies (and thus also under DL ontologies) can be `expressed' in UNFO as a satisfiability problem. In this paper, we consider the natural extension of UNFO with regular expressions on binary relations. The resulting logic UNFOreg can express (unions of) conjunctive two-way regular path queries (C2RPQs) and ontologies formulated in DLs that include transitive roles and regular expressions on roles. Our main results are that evaluating C2RPQs under UNFOreg ontologies is decidable, 2ExpTime-complete in combined complexity, and coNP-complete in data complexity, and that satisfiability in UNFOreg is 2ExpTime-complete, thus not harder than in UNFO.
Cite as

Jean Christoph Jung, Carsten Lutz, Mauricio Martel, and Thomas Schneider. Querying the Unary Negation Fragment with Regular Path Expressions. In 21st International Conference on Database Theory (ICDT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 98, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.ICDT.2018.15,
  author =	{Jung, Jean Christoph and Lutz, Carsten and Martel, Mauricio and Schneider, Thomas},
  title =	{{Querying the Unary Negation Fragment with Regular Path Expressions}},
  booktitle =	{21st International Conference on Database Theory (ICDT 2018)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-063-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{98},
  editor =	{Kimelfeld, Benny and Amsterdamer, Yael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2018.15},
  URN =		{urn:nbn:de:0030-drops-85971},
  doi =		{10.4230/LIPIcs.ICDT.2018.15},
  annote =	{Keywords: Query Answering, Regular Path Queries, Decidable Fragments of First-Order Logic, Computational Complexity}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TIME.2017
LIPIcs, Volume 90, TIME'17, Complete Volume

Authors: Sven Schewe, Thomas Schneider, and Jef Wijsen

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

Abstract
LIPIcs, Volume 90, TIME'17, Complete Volume
Cite as

24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{schewe_et_al:LIPIcs.TIME.2017,
  title =	{{LIPIcs, Volume 90, TIME'17, Complete Volume}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017},
  URN =		{urn:nbn:de:0030-drops-80233},
  doi =		{10.4230/LIPIcs.TIME.2017},
  annote =	{Keywords: Distributed Systems, Design Tools and Techniques, Software/Program Verification, Security and Protection, Models of Computation, Specifying and Verifying and Reasoning about Programs, Mathematical Logic, \lbrackNumerical Linear Algebra\rbrack Linear Systems, Graph Theory}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TIME.2017.0
Front Matter, Table of Contents, Preface, Organization, List of Authors

Authors: Sven Schewe, Thomas Schneider, and Jef Wijsen

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

Abstract
Front Matter, Table of Contents, Preface, Organization, List of Authors
Cite as

24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{schewe_et_al:LIPIcs.TIME.2017.0,
  author =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  title =	{{Front Matter, Table of Contents, Preface, Organization, List of Authors}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{0:i--0:xiv},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.0},
  URN =		{urn:nbn:de:0030-drops-79117},
  doi =		{10.4230/LIPIcs.TIME.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Organization, List of Authors}
}
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-dev.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
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2017.2
Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk)

Authors: Javier Esparza

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

Abstract
We survey recent results on the development of efficient algorithms for the quantitative analysis of business processes modeled as workflow Petri nets. The algorithms can be applied to any workflow net, but have polynomial runtime in the free-choice case.
Cite as

Javier Esparza. Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk). In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{esparza:LIPIcs.TIME.2017.2,
  author =	{Esparza, Javier},
  title =	{{Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{2:1--2:6},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.2},
  URN =		{urn:nbn:de:0030-drops-79266},
  doi =		{10.4230/LIPIcs.TIME.2017.2},
  annote =	{Keywords: Free-choice Petri Nets, concurrency theory, quantitative verification}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2017.3
Plan and Program Synthesis: A New Look at Some Old Problems (Invited Talk)

Authors: Sheila A. McIlraith

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

Abstract
The proliferation of programmable devices, personal assistants, and autonomous systems presents fundamental challenges to the deployment of safe, predictable systems that can work together, interact seamlessly with humans, and that are taskable and instructable by people who may not know how to program. In this talk, we will revisit the classical problem of program synthesis through the lens of AI automated planning. We will present recent advances in AI automated planning principles and computational methods that support the synthesis of plans with goals and preferences specified in Linear Temporal Logic and Regular Expressions. Moving from automated planning in deterministic domains to planning in nondeterministic domains, we will explore the pathway to synthesizing programs that are taskable and instructable by exploiting state-of-the-art AI planning technology.
Cite as

Sheila A. McIlraith. Plan and Program Synthesis: A New Look at Some Old Problems (Invited Talk). In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{mcilraith:LIPIcs.TIME.2017.3,
  author =	{McIlraith, Sheila A.},
  title =	{{Plan and Program Synthesis: A New Look at Some Old Problems}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{3:1--3:1},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.3},
  URN =		{urn:nbn:de:0030-drops-79343},
  doi =		{10.4230/LIPIcs.TIME.2017.3},
  annote =	{Keywords: planning, program synthesis, linear temporal logic, regular expressions}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.4
Possible and Certain Answers for Queries over Order-Incomplete Data

Authors: Antoine Amarilli, Mouhamadou Lamine Ba, Daniel Deutch, and Pierre Senellart

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

Abstract
To combine and query ordered data from multiple sources, one needs to handle uncertainty about the possible orderings. Examples of such "order-incomplete" data include integrated event sequences such as log entries; lists of properties (e.g., hotels and restaurants) ranked by an unknown function reflecting relevance or customer ratings; and documents edited concurrently with an uncertain order on edits. This paper introduces a query language for order-incomplete data, based on the positive relational algebra with order-aware accumulation. We use partial orders to represent order-incomplete data, and study possible and certain answers for queries in this context. We show that these problems are respectively NP-complete and coNP-complete, but identify many tractable cases depending on the query operators or input partial orders.
Cite as

Antoine Amarilli, Mouhamadou Lamine Ba, Daniel Deutch, and Pierre Senellart. Possible and Certain Answers for Queries over Order-Incomplete Data. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.TIME.2017.4,
  author =	{Amarilli, Antoine and Ba, Mouhamadou Lamine and Deutch, Daniel and Senellart, Pierre},
  title =	{{Possible and Certain Answers for Queries over Order-Incomplete Data}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{4:1--4:19},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.4},
  URN =		{urn:nbn:de:0030-drops-79311},
  doi =		{10.4230/LIPIcs.TIME.2017.4},
  annote =	{Keywords: certain answer, possible answer, partial order, uncertain data}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.5
Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks

Authors: Jonathan Behaegel, Jean-Paul Comet, and Maxime Folschette

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

Abstract
We present a new hybrid Hoare logic dedicated for a class of linear hybrid automata well suited to model gene regulatory networks. These automata rely on Thomas' discrete framework in which qualitative parameters have been replaced by continuous parameters called celerities. The identification of these parameters remains one of the keypoints of the modelling process, and is difficult especially because the modelling framework is based on a continuous time. We introduce Hoare triples which handle biological traces and pre/post-conditions. Observed chronometrical biological traces play the role of an imperative program for classical Hoare logic and our hybrid Hoare logic, defined by inference rules, is proved to be sound. Furthermore, we present a weakest precondition calculus (a la Dijkstra) which leads to constraints on dynamical parameters. Finally, we illustrate our "constraints generator" with a simplified circadian clock model describing the rhythmicity of cells in mammals on a 24-hour period.
Cite as

Jonathan Behaegel, Jean-Paul Comet, and Maxime Folschette. Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{behaegel_et_al:LIPIcs.TIME.2017.5,
  author =	{Behaegel, Jonathan and Comet, Jean-Paul and Folschette, Maxime},
  title =	{{Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{5:1--5:21},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.5},
  URN =		{urn:nbn:de:0030-drops-79203},
  doi =		{10.4230/LIPIcs.TIME.2017.5},
  annote =	{Keywords: Hoare logic, weakest precondition, linear hybrid automata, constraint synthesis, gene networks}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.6
Hierarchical Cost-Parity Games

Authors: Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino

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

Abstract
Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. In this paper, we contribute to research on Cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSpace-Complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.
Cite as

Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino. Hierarchical Cost-Parity Games. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.TIME.2017.6,
  author =	{Bozzelli, Laura and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},
  title =	{{Hierarchical Cost-Parity Games}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{6:1--6:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.6},
  URN =		{urn:nbn:de:0030-drops-79175},
  doi =		{10.4230/LIPIcs.TIME.2017.6},
  annote =	{Keywords: Parity Games, Cost-Parity Games, Hierarchical Systems, System Verification}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.7
Timed-Automata-Based Verification of MITL over Signals

Authors: Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege

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

Abstract
It has been argued that the most suitable semantic model for real-time formalisms is the non-negative real line (signals), i.e. the continuous semantics, which naturally captures the continuous evolution of system states. Existing tools like UPPAAL are, however, based on omega-sequences with timestamps (timed words), i.e. the pointwise semantics. Furthermore, the support for logic formalisms is very limited in these tools. In this article, we amend these issues by a compositional translation from Metric Temporal Interval Logic (MITL) to signal automata. Combined with an emptiness-preserving encoding of signal automata into timed automata, we obtain a practical automata-based approach to MITL model-checking over signals. We implement the translation in our tool MightyL and report on case studies using LTSmin as the back-end.
Cite as

Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. Timed-Automata-Based Verification of MITL over Signals. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.TIME.2017.7,
  author =	{Brihaye, Thomas and Geeraerts, Gilles and Ho, Hsi-Ming and Monmege, Benjamin},
  title =	{{Timed-Automata-Based Verification of MITL over Signals}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{7:1--7:19},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.7},
  URN =		{urn:nbn:de:0030-drops-79126},
  doi =		{10.4230/LIPIcs.TIME.2017.7},
  annote =	{Keywords: real-time temporal logic, timed automata, real-time systems}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.8
Dynamic Controllability Made Simple

Authors: Massimo Cairo and Romeo Rizzi

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

Abstract
Simple Temporal Networks with Uncertainty (STNUs) are a well-studied model for representing temporal constraints, where some intervals (contingent links) have an unknown but bounded duration, discovered only during execution. An STNU is dynamically controllable (DC) if there exists a strategy to execute its time-points satisfying all the constraints, regardless of the actual duration of contingent links revealed during execution. In this work we present a new system of constraint propagation rules for STNUs, which is sound-and-complete for DC checking. Our system comprises just three rules which, differently from the ones proposed in all previous works, only generate unconditioned constraints. In particular, after applying our sound rules, the network remains an STNU in all respects. Moreover, our completeness proof is short and non-algorithmic, based on the explicit construction of a valid execution strategy. This is a substantial simplification of the theory which underlies all the polynomial-time algorithms for DC-checking. Our analysis also shows: (1) the existence of late execution strategies for STNUs, (2) the equivalence of several variants of the notion of DC, (3) the existence of a fast algorithm for real-time execution of STNUs, which runs in O(KN) total time in a network with K contingent links and N time points, considerably improving the previous O(N^3)-time bound.
Cite as

Massimo Cairo and Romeo Rizzi. Dynamic Controllability Made Simple. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cairo_et_al:LIPIcs.TIME.2017.8,
  author =	{Cairo, Massimo and Rizzi, Romeo},
  title =	{{Dynamic Controllability Made Simple}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{8:1--8:16},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.8},
  URN =		{urn:nbn:de:0030-drops-79136},
  doi =		{10.4230/LIPIcs.TIME.2017.8},
  annote =	{Keywords: Simple Temporal Network with Uncertainty, Dynamic controllability}
}
  • Refine by Author
  • 5 Schneider, Thomas
  • 3 Cairo, Massimo
  • 3 Rizzi, Romeo
  • 2 Fuhs, Carsten
  • 2 Geeraerts, Gilles
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Spatial and physical reasoning
  • 1 Computing methodologies → Symbolic calculus algorithms
  • 1 Information systems → Spatial-temporal systems
  • 1 Mathematics of computing → Graph algorithms
  • 1 Theory of computation → Algorithmic mechanism design
  • Show More...

  • Refine by Keyword
  • 2 Decidable Fragments of First-Order Logic
  • 2 Dynamic Consistency
  • 2 Temporal Logic
  • 2 algorithm engineering
  • 2 composition table
  • Show More...

  • Refine by Type
  • 34 document
  • 1 volume

  • Refine by Publication Year
  • 27 2017
  • 2 2010
  • 1 2007
  • 1 2014
  • 1 2018
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact