7 Search Results for "Lück, Martin"

Document
DOI: 10.4230/LIPIcs.CSL.2025.10
The Complexity of Second-Order HyperLTL

Authors: Hadar Frenkel and Martin Zimmermann

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is Σ₁¹-complete, i.e., only as hard as for (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in Σ₂² and are Σ₁¹-hard, and thus also less complex than for full second-order HyperLTL.
Cite as

Hadar Frenkel and Martin Zimmermann. The Complexity of Second-Order HyperLTL. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{frenkel_et_al:LIPIcs.CSL.2025.10,
  author =	{Frenkel, Hadar and Zimmermann, Martin},
  title =	{{The Complexity of Second-Order HyperLTL}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{10:1--10:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.10},
  URN =		{urn:nbn:de:0030-drops-227679},
  doi =		{10.4230/LIPIcs.CSL.2025.10},
  annote =	{Keywords: HyperLTL, Satisfiability, Model-checking}
}
Document
Vision
DOI: 10.4230/TGDK.1.1.13
Autonomy in the Age of Knowledge Graphs: Vision and Challenges

Authors: Jean-Paul Calbimonte, Andrei Ciortea, Timotheus Kampik, Simon Mayer, Terry R. Payne, Valentina Tamma, and Antoine Zimmermann

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
In this position paper, we propose that Knowledge Graphs (KGs) are one of the prime approaches to support the programming of autonomous software systems at the knowledge level. From this viewpoint, we survey how KGs can support different dimensions of autonomy in such systems: For example, the autonomy of systems with respect to their environment, or with respect to organisations; and we discuss related practical and research challenges. We emphasise that KGs need to be able to support systems of autonomous software agents that are themselves highly heterogeneous, which limits how these systems may use KGs. Furthermore, these heterogeneous software agents may populate highly dynamic environments, which implies that they require adaptive KGs. The scale of the envisioned systems - possibly stretching to the size of the Internet - highlights the maintainability of the underlying KGs that need to contain large-scale knowledge, which requires that KGs are maintained jointly by humans and machines. Furthermore, autonomous agents require procedural knowledge, and KGs should hence be explored more towards the provisioning of such knowledge to augment autonomous behaviour. Finally, we highlight the importance of modelling choices, including with respect to the selected abstraction level when modelling and with respect to the provisioning of more expressive constraint languages.
Cite as

Jean-Paul Calbimonte, Andrei Ciortea, Timotheus Kampik, Simon Mayer, Terry R. Payne, Valentina Tamma, and Antoine Zimmermann. Autonomy in the Age of Knowledge Graphs: Vision and Challenges. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{calbimonte_et_al:TGDK.1.1.13,
  author =	{Calbimonte, Jean-Paul and Ciortea, Andrei and Kampik, Timotheus and Mayer, Simon and Payne, Terry R. and Tamma, Valentina and Zimmermann, Antoine},
  title =	{{Autonomy in the Age of Knowledge Graphs: Vision and Challenges}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{13:1--13:22},
  ISSN =	{2942-7517},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.13},
  URN =		{urn:nbn:de:0030-drops-194872},
  doi =		{10.4230/TGDK.1.1.13},
  annote =	{Keywords: Knowledge graphs, Autonomous Systems}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.27
On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic

Authors: Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Second-order Boolean logic is a generalization of QBF, whose constant alternation fragments are known to be complete for the levels of the exponential time hierarchy. We consider two types of restriction of this logic: 1) restrictions to term constructions, 2) restrictions to the form of the Boolean matrix. Of the first sort, we consider two kinds of restrictions: firstly, disallowing nested use of proper function variables, and secondly stipulating that each function variable must appear with a fixed sequence of arguments. Of the second sort, we consider Horn, Krom, and core fragments of the Boolean matrix. We classify the complexity of logics obtained by combining these two types of restrictions. We show that, in most cases, logics with k alternating blocks of function quantifiers are complete for the kth or (k-1)th level of the exponential time hierarchy. Furthermore, we establish NL-completeness for the Krom and core fragments, when k = 1 and both restrictions of the first sort are in effect.
Cite as

Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema. On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hannula_et_al:LIPIcs.CSL.2021.27,
  author =	{Hannula, Miika and Kontinen, Juha and L\"{u}ck, Martin and Virtema, Jonni},
  title =	{{On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{27:1--27:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.27},
  URN =		{urn:nbn:de:0030-drops-134610},
  doi =		{10.4230/LIPIcs.CSL.2021.27},
  annote =	{Keywords: quantified Boolean formulae, computational complexity, second-order logic, Horn and Krom fragment}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.30
Canonical Models and the Complexity of Modal Team Logic

Authors: Martin Lück

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We study modal team logic MTL, the team-semantical extension of classical modal logic closed under Boolean negation. Its fragments, such as modal dependence, independence, and inclusion logic, are well-understood. However, due to the unrestricted Boolean negation, the satisfiability problem of full MTL has been notoriously resistant to a complexity theoretical classification. In our approach, we adapt the notion of canonical models for team semantics. By construction of such a model, we reduce the satisfiability problem of MTL to simple model checking. Afterwards, we show that this method is optimal in the sense that MTL-formulas can efficiently enforce canonicity. Furthermore, to capture these results in terms of computational complexity, we introduce a non-elementary complexity class, TOWER(poly), and prove that the satisfiability and validity problem of MTL are complete for it. We also show that the fragments of MTL with bounded modal depth are complete for the levels of the elementary hierarchy (with polynomially many alternations).
Cite as

Martin Lück. Canonical Models and the Complexity of Modal Team Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{luck:LIPIcs.CSL.2018.30,
  author =	{L\"{u}ck, Martin},
  title =	{{Canonical Models and the Complexity of Modal Team Logic}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{30:1--30:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.30},
  URN =		{urn:nbn:de:0030-drops-96979},
  doi =		{10.4230/LIPIcs.CSL.2018.30},
  annote =	{Keywords: team semantics, modal logic, complexity, satisfiability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.27
On the Complexity of Team Logic and Its Two-Variable Fragment

Authors: Martin Lück

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We study the logic FO(~), the extension of first-order logic with team semantics by unrestricted Boolean negation. It was recently shown to be axiomatizable, but otherwise has not yet received much attention in questions of computational complexity. In this paper, we consider its two-variable fragment FO^2(~) and prove that its satisfiability problem is decidable, and in fact complete for the recently introduced non-elementary class TOWER(poly). Moreover, we classify the complexity of model checking of FO(~) with respect to the number of variables and the quantifier rank, and prove a dichotomy between PSPACE- and ATIME-ALT(exp, poly)-complete fragments. For the lower bounds, we propose a translation from modal team logic MTL to FO^2(~) that extends the well-known standard translation from modal logic ML to FO^2. For the upper bounds, we translate FO(~) to fragments of second-order logic with PSPACE-complete and ATIME-ALT(exp, poly)-complete model checking, respectively.
Cite as

Martin Lück. On the Complexity of Team Logic and Its Two-Variable Fragment. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{luck:LIPIcs.MFCS.2018.27,
  author =	{L\"{u}ck, Martin},
  title =	{{On the Complexity of Team Logic and Its Two-Variable Fragment}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{27:1--27:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.27},
  URN =		{urn:nbn:de:0030-drops-96094},
  doi =		{10.4230/LIPIcs.MFCS.2018.27},
  annote =	{Keywords: team logic, two-variable logic, complexity, satisfiability, model checking}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.31
The Power of the Filtration Technique for Modal Logics with Team Semantics

Authors: Martin Lück

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

Abstract
Modal Team Logic (MTL) extends Väänänen's Modal Dependence Logic (MDL) by Boolean negation. Its satisfiability problem is decidable, but the exact complexity is not yet understood very well. We investigate a model-theoretical approach and generalize the successful filtration technique to work in team semantics. We identify an "existential" fragment of MTL that enjoys the exponential model property and is therefore, like Propositional Team Logic (PTL), complete for the class AEXP(poly). Moreover, superexponential filtration lower bounds for different fragments of MTL are proven, up to the full logic having no filtration for any elementary size bound. As a corollary, superexponential gaps of succinctness between MTL fragments of equal expressive power are shown.
Cite as

Martin Lück. The Power of the Filtration Technique for Modal Logics with Team Semantics. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{luck:LIPIcs.CSL.2017.31,
  author =	{L\"{u}ck, Martin},
  title =	{{The Power of the Filtration Technique for Modal Logics with Team Semantics}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{31:1--31:20},
  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.31},
  URN =		{urn:nbn:de:0030-drops-76739},
  doi =		{10.4230/LIPIcs.CSL.2017.31},
  annote =	{Keywords: dependence logic,team logic,modal logic,finite model theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.33
Axiomatizations for Propositional and Modal Team Logic

Authors: Martin Lück

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
A framework is developed that extends Hilbert-style proof systems for propositional and modal logics to comprehend their team-based counterparts. The method is applied to classical propositional logic and the modal logic K. Complete axiomatizations for their team-based extensions, propositional team logic PTL and modal team logic MTL, are presented.
Cite as

Martin Lück. Axiomatizations for Propositional and Modal Team Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{luck:LIPIcs.CSL.2016.33,
  author =	{L\"{u}ck, Martin},
  title =	{{Axiomatizations for Propositional and Modal Team Logic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{33:1--33:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.33},
  URN =		{urn:nbn:de:0030-drops-65739},
  doi =		{10.4230/LIPIcs.CSL.2016.33},
  annote =	{Keywords: team logic, propositional team logic, modal team logic, proof system, axiomatization}
}
  • Refine by Type
  • 7 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2023
  • 1 2021
  • 2 2018
  • 1 2017
  • Show More...

  • Refine by Author
  • 5 Lück, Martin
  • 1 Calbimonte, Jean-Paul
  • 1 Ciortea, Andrei
  • 1 Frenkel, Hadar
  • 1 Hannula, Miika
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs
  • 1 TGDK

  • Refine by Classification
  • 3 Theory of computation → Complexity theory and logic
  • 2 Theory of computation → Logic
  • 1 Computer systems organization → Self-organizing autonomic computing
  • 1 Computing methodologies → Intelligent agents
  • 1 Computing methodologies → Knowledge representation and reasoning
  • Show More...

  • Refine by Keyword
  • 2 complexity
  • 2 satisfiability
  • 2 team logic
  • 1 Autonomous Systems
  • 1 Horn and Krom fragment
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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