32 Search Results for "Reynolds, Mark"

Volume

LIPIcs, Volume 206

28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

TIME 2021, September 27-29, 2021, Klagenfurt, Austria

Editors: Carlo Combi, Johann Eder, and Mark Reynolds

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.22
Constrictor: Immutability as a Design Concept

Authors: Elad Kinsbruner, Shachar Itzhaky, and Hila Peleg

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Many object-oriented applications in algorithm design rely on objects never changing during their lifetime. This is often tackled by marking object references as read-only, e.g., using the const keyword in C++. In other languages like Python or Java where such a concept does not exist, programmers rely on best practices that are entirely unenforced. While reliance on best practices is obviously too permissive, const-checking is too restrictive: it is possible for a method to mutate the internal state while still satisfying the property we expect from an "immutable" object in this setting. We would therefore like to enforce the immutability of an object’s abstract state. We check an object’s immutability through a view of its abstract state: for instances of an immutable class, the view does not change when running any of the class’s methods, even if some of the internal state does change. If all methods of a class are verified as non-mutating, we can deem the entire class view-immutable. We present an SMT-based algorithm to check view-immutability, and implement it in our linter/verifier, Constrictor. We evaluate Constrictor on 51 examples of immutability-related design violations. Our evaluation shows that Constrictor is effective at catching a variety of prototypical design violations, and does so in seconds. We also explore Constrictor with two real-world case studies.
Cite as

Elad Kinsbruner, Shachar Itzhaky, and Hila Peleg. Constrictor: Immutability as a Design Concept. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 22:1-22:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kinsbruner_et_al:LIPIcs.ECOOP.2024.22,
  author =	{Kinsbruner, Elad and Itzhaky, Shachar and Peleg, Hila},
  title =	{{Constrictor: Immutability as a Design Concept}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{22:1--22:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.22},
  URN =		{urn:nbn:de:0030-drops-208715},
  doi =		{10.4230/LIPIcs.ECOOP.2024.22},
  annote =	{Keywords: Immutability, Design Enforcement, SMT, Liskov Substitution Principle, Object-oriented Programming}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.24
Qafny: A Quantum-Program Verifier

Authors: Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny’s automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover’s algorithm, and Shor’s algorithm.
Cite as

Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A Quantum-Program Verifier. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 24:1-24:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ECOOP.2024.24,
  author =	{Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi},
  title =	{{Qafny: A Quantum-Program Verifier}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{24:1--24:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.24},
  URN =		{urn:nbn:de:0030-drops-208735},
  doi =		{10.4230/LIPIcs.ECOOP.2024.24},
  annote =	{Keywords: Quantum Computing, Automated Verification, Separation Logic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.39
Formalizing, Mechanizing, and Verifying Class-Based Refinement Types

Authors: Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Refinement types have been extensively used in class-based languages to specify and verify fine-grained logical specifications. Despite the advances in practical aspects such as applicability and usability, two fundamental issues persist. First, the soundness of existing class-based refinement type systems is inadequately explored, casting doubts on their reliability. Second, the expressiveness of existing systems is limited, restricting the depiction of semantic properties related to object-oriented constructs. This work tackles these issues through a systematic framework. We formalize a declarative class-based refinement type calculus (named RFJ), that is expressive and concise. We rigorously develop the soundness meta-theory of this calculus, followed by its mechanization in Coq. Finally, to ensure the calculus’s verifiability, we propose an algorithmic verification approach based on a fragment of first-order logic (named LFJ), and implement this approach as a type checker.
Cite as

Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 39:1-39:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{sun_et_al:LIPIcs.ECOOP.2024.39,
  author =	{Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan},
  title =	{{Formalizing, Mechanizing, and Verifying Class-Based Refinement Types}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{39:1--39:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.39},
  URN =		{urn:nbn:de:0030-drops-208881},
  doi =		{10.4230/LIPIcs.ECOOP.2024.39},
  annote =	{Keywords: Refinement Types, Program Verification, Object-oriented Programming}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.29
Mutational Fuzz Testing for Constraint Modeling Systems

Authors: Wout Vanroose, Ignace Bleukx, Jo Devriendt, Dimos Tsouros, Hélène Verhaeghe, and Tias Guns

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Constraint programming (CP) modeling languages, like MiniZinc, Essence and CPMpy, play a crucial role in making CP technology accessible to non-experts. Both solver-independent modeling frameworks and solvers themselves are complex pieces of software that can contain bugs, which undermines their usefulness. Mutational fuzz testing is a way to test complex systems by stochastically mutating input and verifying preserved properties of the mutated output. We investigate different mutations and verification methods that can be used on the constraint specifications directly. This includes methods proposed in the context of SMT problem specifications, as well as new methods related to global constraints, optimization, and solution counting/preservation. Our results show that such a fuzz testing approach improves the overall code coverage of a modeling system compared to only unit testing, and is able to find bugs in the whole toolchain, from the modeling language transformations themselves to the underlying solvers.
Cite as

Wout Vanroose, Ignace Bleukx, Jo Devriendt, Dimos Tsouros, Hélène Verhaeghe, and Tias Guns. Mutational Fuzz Testing for Constraint Modeling Systems. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 29:1-29:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vanroose_et_al:LIPIcs.CP.2024.29,
  author =	{Vanroose, Wout and Bleukx, Ignace and Devriendt, Jo and Tsouros, Dimos and Verhaeghe, H\'{e}l\`{e}ne and Guns, Tias},
  title =	{{Mutational Fuzz Testing for Constraint Modeling Systems}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{29:1--29:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.29},
  URN =		{urn:nbn:de:0030-drops-207149},
  doi =		{10.4230/LIPIcs.CP.2024.29},
  annote =	{Keywords: fuzz testing, Constraint modeling language, bugs, mutational testing, modeling, constraint reformulation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.14
Two-Dimensional Kripke Semantics I: Presheaves

Authors: G. A. Kavvos

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.
Cite as

G. A. Kavvos. Two-Dimensional Kripke Semantics I: Presheaves. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kavvos:LIPIcs.FSCD.2024.14,
  author =	{Kavvos, G. A.},
  title =	{{Two-Dimensional Kripke Semantics I: Presheaves}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.14},
  URN =		{urn:nbn:de:0030-drops-203438},
  doi =		{10.4230/LIPIcs.FSCD.2024.14},
  annote =	{Keywords: modal logic, categorical semantics, Kripke semantics, duality, open maps}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.151
Identifying Tractable Quantified Temporal Constraints Within Ord-Horn

Authors: Jakub Rydval, Žaneta Semanišinová, and Michał Wrona

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
The constraint satisfaction problem, parameterized by a relational structure, provides a general framework for expressing computational decision problems. Already the restriction to the class of all finite structures forms an interesting microcosm on its own, but to express decision problems in temporal reasoning one has to take a step beyond the finite-domain realm. An important class of templates used in this context are temporal structures, i.e., structures over ℚ whose relations are first-order definable using the usual countable dense linear order without endpoints. In the standard setting, which allows only existential quantification over input variables, the complexity of finite and temporal constraints has been fully classified. In the quantified setting, i.e., when one also allows universal quantifiers, there is only a handful of partial classification results and many concrete cases of unknown complexity. This paper presents a significant progress towards understanding the complexity of the quantified constraint satisfaction problem for temporal structures. We provide a complexity dichotomy for quantified constraints over the Ord-Horn fragment, which played an important role in understanding the complexity of constraints both over temporal structures and in Allen’s interval algebra. We show that all problems under consideration are in P or coNP-hard. In particular, we determine the complexity of the quantified constraint satisfaction problem for (ℚ;x = y⇒ x ≥ z), hereby settling a question open for more than ten years.
Cite as

Jakub Rydval, Žaneta Semanišinová, and Michał Wrona. Identifying Tractable Quantified Temporal Constraints Within Ord-Horn. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 151:1-151:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{rydval_et_al:LIPIcs.ICALP.2024.151,
  author =	{Rydval, Jakub and Semani\v{s}inov\'{a}, \v{Z}aneta and Wrona, Micha{\l}},
  title =	{{Identifying Tractable Quantified Temporal Constraints Within Ord-Horn}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{151:1--151:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.151},
  URN =		{urn:nbn:de:0030-drops-202944},
  doi =		{10.4230/LIPIcs.ICALP.2024.151},
  annote =	{Keywords: constraint satisfaction problems, quantifiers, dichotomy, temporal reasoning, Ord-Horn}
}
Document
Position
DOI: 10.4230/TGDK.2.1.2
Grounding Stream Reasoning Research

Authors: Pieter Bonte, Jean-Paul Calbimonte, Daniel de Leng, Daniele Dell'Aglio, Emanuele Della Valle, Thomas Eiter, Federico Giannini, Fredrik Heintz, Konstantin Schekotihin, Danh Le-Phuoc, Alessandra Mileo, Patrik Schneider, Riccardo Tommasini, Jacopo Urbani, and Giacomo Ziffer

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
In the last decade, there has been a growing interest in applying AI technologies to implement complex data analytics over data streams. To this end, researchers in various fields have been organising a yearly event called the "Stream Reasoning Workshop" to share perspectives, challenges, and experiences around this topic. In this paper, the previous organisers of the workshops and other community members provide a summary of the main research results that have been discussed during the first six editions of the event. These results can be categorised into four main research areas: The first is concerned with the technological challenges related to handling large data streams. The second area aims at adapting and extending existing semantic technologies to data streams. The third and fourth areas focus on how to implement reasoning techniques, either considering deductive or inductive techniques, to extract new and valuable knowledge from the data in the stream. This summary is written not only to provide a crystallisation of the field, but also to point out distinctive traits of the stream reasoning community. Moreover, it also provides a foundation for future research by enumerating a list of use cases and open challenges, to stimulate others to join this exciting research area.
Cite as

Pieter Bonte, Jean-Paul Calbimonte, Daniel de Leng, Daniele Dell'Aglio, Emanuele Della Valle, Thomas Eiter, Federico Giannini, Fredrik Heintz, Konstantin Schekotihin, Danh Le-Phuoc, Alessandra Mileo, Patrik Schneider, Riccardo Tommasini, Jacopo Urbani, and Giacomo Ziffer. Grounding Stream Reasoning Research. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 2:1-2:47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{bonte_et_al:TGDK.2.1.2,
  author =	{Bonte, Pieter and Calbimonte, Jean-Paul and de Leng, Daniel and Dell'Aglio, Daniele and Della Valle, Emanuele and Eiter, Thomas and Giannini, Federico and Heintz, Fredrik and Schekotihin, Konstantin and Le-Phuoc, Danh and Mileo, Alessandra and Schneider, Patrik and Tommasini, Riccardo and Urbani, Jacopo and Ziffer, Giacomo},
  title =	{{Grounding Stream Reasoning Research}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{2:1--2:47},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.2},
  URN =		{urn:nbn:de:0030-drops-198597},
  doi =		{10.4230/TGDK.2.1.2},
  annote =	{Keywords: Stream Reasoning, Stream Processing, RDF streams, Streaming Linked Data, Continuous query processing, Temporal Logics, High-performance computing, Databases}
}
Document
Survey
DOI: 10.4230/TGDK.2.1.3
Semantic Web: Past, Present, and Future

Authors: Ansgar Scherp, Gerd Groener, Petr Škoda, Katja Hose, and Maria-Esther Vidal

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
Ever since the vision was formulated, the Semantic Web has inspired many generations of innovations. Semantic technologies have been used to share vast amounts of information on the Web, enhance them with semantics to give them meaning, and enable inference and reasoning on them. Throughout the years, semantic technologies, and in particular knowledge graphs, have been used in search engines, data integration, enterprise settings, and machine learning. In this paper, we recap the classical concepts and foundations of the Semantic Web as well as modern and recent concepts and applications, building upon these foundations. The classical topics we cover include knowledge representation, creating and validating knowledge on the Web, reasoning and linking, and distributed querying. We enhance this classical view of the so-called "Semantic Web Layer Cake" with an update of recent concepts that include provenance, security and trust, as well as a discussion of practical impacts from industry-led contributions. We conclude with an outlook on the future directions of the Semantic Web. This is a living document. If you like to contribute, please contact the first author and visit: https://github.com/ascherp/semantic-web-primer
Cite as

Ansgar Scherp, Gerd Groener, Petr Škoda, Katja Hose, and Maria-Esther Vidal. Semantic Web: Past, Present, and Future. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 3:1-3:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{scherp_et_al:TGDK.2.1.3,
  author =	{Scherp, Ansgar and Groener, Gerd and \v{S}koda, Petr and Hose, Katja and Vidal, Maria-Esther},
  title =	{{Semantic Web: Past, Present, and Future}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{3:1--3:37},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.3},
  URN =		{urn:nbn:de:0030-drops-198607},
  doi =		{10.4230/TGDK.2.1.3},
  annote =	{Keywords: Linked Open Data, Semantic Web Graphs, Knowledge Graphs}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.8
Seventeen Provers Under the Hammer

Authors: Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers," increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL’s Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow’s Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.
Cite as

Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8,
  author =	{Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
  title =	{{Seventeen Provers Under the Hammer}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8},
  URN =		{urn:nbn:de:0030-drops-167178},
  doi =		{10.4230/LIPIcs.ITP.2022.8},
  annote =	{Keywords: Automatic theorem proving, interactive theorem proving, proof assistants}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TIME.2021
LIPIcs, Volume 206, TIME 2021, Complete Volume

Authors: Carlo Combi, Johann Eder, and Mark Reynolds

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

Abstract
LIPIcs, Volume 206, TIME 2021, Complete Volume
Cite as

28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 1-244, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{combi_et_al:LIPIcs.TIME.2021,
  title =	{{LIPIcs, Volume 206, TIME 2021, Complete Volume}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{1--244},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021},
  URN =		{urn:nbn:de:0030-drops-147755},
  doi =		{10.4230/LIPIcs.TIME.2021},
  annote =	{Keywords: LIPIcs, Volume 206, TIME 2021, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TIME.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Carlo Combi, Johann Eder, and Mark Reynolds

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

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

Copy BibTex To Clipboard

@InProceedings{combi_et_al:LIPIcs.TIME.2021.0,
  author =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.0},
  URN =		{urn:nbn:de:0030-drops-147761},
  doi =		{10.4230/LIPIcs.TIME.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2021.1
Simple Temporal Networks: A Practical Foundation for Temporal Representation and Reasoning (Invited Talk)

Authors: Luke Hunsberger and Roberto Posenato

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

Abstract
Since Simple Temporal Networks (STNs) were first introduced in 1991, there have been numerous theoretic and algorithmic advances that have made them practical for a wide variety of applications. However, the presentation of most of the important advances have been scattered across numerous conference papers and journal articles. As a result, it is too easy for even experienced researchers to be unaware of results that could positively impact their work. In this talk we review the most important results about STNs for researchers in Artificial Intelligence who are interested in incorporating the management of time and temporal constraints into their projects.
Cite as

Luke Hunsberger and Roberto Posenato. Simple Temporal Networks: A Practical Foundation for Temporal Representation and Reasoning (Invited Talk). In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hunsberger_et_al:LIPIcs.TIME.2021.1,
  author =	{Hunsberger, Luke and Posenato, Roberto},
  title =	{{Simple Temporal Networks: A Practical Foundation for Temporal Representation and Reasoning}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{1:1--1:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.1},
  URN =		{urn:nbn:de:0030-drops-147770},
  doi =		{10.4230/LIPIcs.TIME.2021.1},
  annote =	{Keywords: Simple Temporal Networks, Consistency Checking, Restoring Consistency, Dispatchability, Temporal Decoupling Problem}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2021.2
Extreme-Scale Model-Based Time Series Management with ModelarDB (Invited Talk)

Authors: Torben Bach Pedersen

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

Abstract
To monitor critical industrial devices such as wind turbines, high quality sensors sampled at a high frequency are increasingly used. Current technology does not handle these extreme-scale time series well [Søren Kejser Jensen et al., 2017], so only simple aggregates are traditionally stored, removing outliers and fluctuations that could indicate problems. As a remedy, we present a model-based approach for managing extreme-scale time series that approximates the time series values using mathematical functions (models) and stores only model coefficients rather than data values. Compression is done both for individual time series and for correlated groups of time series. The keynote will present concepts, techniques, and algorithms from model-based time series management and our implementation of these in the open source Time Series Management System (TSMS) ModelarDB[Søren Kejser Jensen et al., 2018; Søren Kejser Jensen et al., 2019; Søren Kejser Jensen et al., 2021] . Furthermore, it will present our experimental evaluation of ModelarDB on extreme-scale real-world time series, which shows that that compared to widely used Big Data formats, ModelarDB provides up to 14× faster ingestion due to high compression, 113× better compression due to its adaptability, 573× faster aggregatation by using models, and close to linear scale-out scalability. ModelarDB is being commercialized by the spin-out company ModelarData.
Cite as

Torben Bach Pedersen. Extreme-Scale Model-Based Time Series Management with ModelarDB (Invited Talk). In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{pedersen:LIPIcs.TIME.2021.2,
  author =	{Pedersen, Torben Bach},
  title =	{{Extreme-Scale Model-Based Time Series Management with ModelarDB}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.2},
  URN =		{urn:nbn:de:0030-drops-147785},
  doi =		{10.4230/LIPIcs.TIME.2021.2},
  annote =	{Keywords: Model-based storage, approximate query processing, time series management, extreme-scale data}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2021.3
Kernel Machines in Time (Invited Talk)

Authors: Johan Suykens

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

Abstract
Kernel machines is a powerful class of models in machine learning with solid foundations and many existing application fields. The scope of this talk is kernel machines in time with a main focus on least squares support vector machines, and other related methods such as kernel principal component analysis and kernel spectral clustering. For dynamical systems modelling different possible input-output and state space model structures will be discussed. Applications will be shown on electricity load forecasting and temperature prediction in weather forecasting. Approximate closed-form solutions can be given to ordinary and partial differential equations. Kernel spectral clustering applications to identifying customer profiles, pollution modelling and detecting topological changes in time-series of bridges will be shown. Finally, new synergies between kernel machines and deep learning will be presented, leading for example to generative kernel machines, with new insights on disentangled representations, explainability and latent space exploration. Application of these models will be illustrated on out-of-distribution detection of time-series data.
Cite as

Johan Suykens. Kernel Machines in Time (Invited Talk). In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{suykens:LIPIcs.TIME.2021.3,
  author =	{Suykens, Johan},
  title =	{{Kernel Machines in Time}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.3},
  URN =		{urn:nbn:de:0030-drops-147791},
  doi =		{10.4230/LIPIcs.TIME.2021.3},
  annote =	{Keywords: SVM, Time series analysis}
}
  • Refine by Author
  • 5 Reynolds, Mark
  • 4 Montanari, Angelo
  • 2 Cashmore, Michael
  • 2 Combi, Carlo
  • 2 Eder, Johann
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Modal and temporal logics
  • 4 Computing methodologies → Temporal reasoning
  • 2 Applied computing
  • 2 Computing methodologies → Artificial intelligence
  • 2 Computing methodologies → Robotic planning
  • Show More...

  • Refine by Keyword
  • 2 Interval temporal logic
  • 2 Object-oriented Programming
  • 2 Temporal Planning
  • 2 Temporal logic
  • 2 Timed Automata
  • Show More...

  • Refine by Type
  • 31 document
  • 1 volume

  • Refine by Publication Year
  • 20 2021
  • 8 2024
  • 2 2018
  • 1 2019
  • 1 2022

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