Search Results

Documents authored by Meier, Arne

Document
DOI: 10.4230/LIPIcs.STACS.2021.40
Parameterised Counting in Logspace

Authors: Anselm Haak, Arne Meier, Om Prakash, and Raghavendra Rao B. V.

Published in: LIPIcs, Volume 187, 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)

Abstract
Logarithmic space bounded complexity classes such as L and NL play a central role in space bounded computation. The study of counting versions of these complexity classes have lead to several interesting insights into the structure of computational problems such as computing the determinant and counting paths in directed acyclic graphs. Though parameterised complexity theory was initiated roughly three decades ago by Downey and Fellows, a satisfactory study of parameterised logarithmic space bounded computation was developed only in the last decade by Elberfeld, Stockhusen and Tantau (IPEC 2013, Algorithmica 2015). In this paper, we introduce a new framework for parameterised counting in logspace, inspired by the parameterised space bounded models developed by Elberfeld, Stockhusen and Tantau (IPEC 2013, Algorithmica 2015). They defined the operators para_W and para_β for parameterised space complexity classes by allowing bounded nondeterminism with multiple-read and read-once access, respectively. Using these operators, they characterised the parameterised complexity of natural problems on graphs. In the spirit of the operators para_W and para_β by Stockhusen and Tantau, we introduce variants based on tail-nondeterminism, para_{W[1]} and para_{βtail}. Then, we consider counting versions of all four operators applied to logspace and obtain several natural complete problems for the resulting classes: counting of paths in digraphs, counting first-order models for formulas, and counting graph homomorphisms. Furthermore, we show that the complexity of a parameterised variant of the determinant function for (0,1)-matrices is #para_{βtail} L-hard and can be written as the difference of two functions in #para_{βtail} L. These problems exhibit the richness of the introduced counting classes. Our results further indicate interesting structural characteristics of these classes. For example, we show that the closure of #para_{βtail} L under parameterised logspace parsimonious reductions coincides with #para_β L, that is, modulo parameterised reductions, tail-nondeterminism with read-once access is the same as read-once nondeterminism. Initiating the study of closure properties of these parameterised logspace counting classes, we show that all introduced classes are closed under addition and multiplication, and those without tail-nondeterminism are closed under parameterised logspace parsimonious reductions. Also, we show that the counting classes defined can naturally be characterised by parameterised variants of classes based on branching programs in analogy to the classical counting classes. Finally, we underline the significance of this topic by providing a promising outlook showing several open problems and options for further directions of research.
Cite as

Anselm Haak, Arne Meier, Om Prakash, and Raghavendra Rao B. V.. Parameterised Counting in Logspace. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{haak_et_al:LIPIcs.STACS.2021.40,
  author =	{Haak, Anselm and Meier, Arne and Prakash, Om and Rao B. V., Raghavendra},
  title =	{{Parameterised Counting in Logspace}},
  booktitle =	{38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
  pages =	{40:1--40:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-180-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{187},
  editor =	{Bl\"{a}ser, Markus and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2021.40},
  URN =		{urn:nbn:de:0030-drops-136859},
  doi =		{10.4230/LIPIcs.STACS.2021.40},
  annote =	{Keywords: Parameterized Complexity, Counting Complexity, Logspace}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.10
Team Semantics for the Specification and Verification of Hyperproperties

Authors: Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann

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

Abstract
We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.
Cite as

Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{krebs_et_al:LIPIcs.MFCS.2018.10,
  author =	{Krebs, Andreas and Meier, Arne and Virtema, Jonni and Zimmermann, Martin},
  title =	{{Team Semantics for the Specification and Verification of Hyperproperties}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{10:1--10:16},
  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.10},
  URN =		{urn:nbn:de:0030-drops-95926},
  doi =		{10.4230/LIPIcs.MFCS.2018.10},
  annote =	{Keywords: LTL, Hyperproperties, Team Semantics, Model Checking, Satisfiability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.32
Model Checking and Validity in Propositional and Modal Inclusion Logics

Authors: Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the basic reasoning problems for modal and propositional dependence, independence, and inclusion logics.
Cite as

Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema. Model Checking and Validity in Propositional and Modal Inclusion Logics. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{hella_et_al:LIPIcs.MFCS.2017.32,
  author =	{Hella, Lauri and Kuusisto, Antti and Meier, Arne and Virtema, Jonni},
  title =	{{Model Checking and Validity in Propositional and Modal Inclusion Logics}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{32:1--32:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.32},
  URN =		{urn:nbn:de:0030-drops-81007},
  doi =		{10.4230/LIPIcs.MFCS.2017.32},
  annote =	{Keywords: Inclusion Logic, Model Checking, Complexity}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2016.23
Backdoors for Linear Temporal Logic

Authors: Arne Meier, Sebastian Ordyniak, Ramanujan Sridharan, and Irena Schindler

Published in: LIPIcs, Volume 63, 11th International Symposium on Parameterized and Exact Computation (IPEC 2016)

Abstract
In the present paper, we introduce the backdoor set approach into the field of temporal logic for the global fragment of linear temporal logic. We study the parameterized complexity of the satisfiability problem parameterized by the size of the backdoor. We distinguish between backdoor detection and evaluation of backdoors into the fragments of Horn and Krom formulas. Here we classify the operator fragments of globally-operators for past/future/always, and the combination of them. Detection is shown to be fixed-parameter tractable (FPT) whereas the complexity of evaluation behaves differently. We show that for Krom formulas the problem is paraNP-complete. For Horn formulas, the complexity is shown to be either fixed parameter tractable or paraNP-complete depending on the considered operator fragment.
Cite as

Arne Meier, Sebastian Ordyniak, Ramanujan Sridharan, and Irena Schindler. Backdoors for Linear Temporal Logic. In 11th International Symposium on Parameterized and Exact Computation (IPEC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 63, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{meier_et_al:LIPIcs.IPEC.2016.23,
  author =	{Meier, Arne and Ordyniak, Sebastian and Sridharan, Ramanujan and Schindler, Irena},
  title =	{{Backdoors for Linear Temporal Logic}},
  booktitle =	{11th International Symposium on Parameterized and Exact Computation (IPEC 2016)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-023-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{63},
  editor =	{Guo, Jiong and Hermelin, Danny},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2016.23},
  URN =		{urn:nbn:de:0030-drops-69462},
  doi =		{10.4230/LIPIcs.IPEC.2016.23},
  annote =	{Keywords: Linear Temporal Logic, Parameterized Complexity, Backdoor Sets}
}
Document
DOI: 10.4230/DagSemProc.10061.5
Proof Complexity of Propositional Default Logic

Authors: Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)

Abstract
Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen's system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti's enhanced calculus for skeptical default reasoning.
Cite as

Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, and Heribert Vollmer. Proof Complexity of Propositional Default Logic. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:DagSemProc.10061.5,
  author =	{Beyersdorff, Olaf and Meier, Arne and M\"{u}ller, Sebastian and Thomas, Michael and Vollmer, Heribert},
  title =	{{Proof Complexity of Propositional Default Logic}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--14},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.5},
  URN =		{urn:nbn:de:0030-drops-25261},
  doi =		{10.4230/DagSemProc.10061.5},
  annote =	{Keywords: Proof complexity, default logic, sequent calculus}
}
Document
DOI: 10.4230/DagSemProc.10061.6
The Complexity of Reasoning for Fragments of Autoepistemic Logic

Authors: Nadia Creignou, Arne Meier, Michael Thomas, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)

Abstract
Autoepistemic logic extends propositional logic by the modal operator L. A formula that is preceded by an L is said to be "believed". The logic was introduced by Moore 1985 for modeling an ideally rational agent's behavior and reasoning about his own beliefs. In this paper we analyze all Boolean fragments of autoepistemic logic with respect to the computational complexity of the three most common decision problems expansion existence, brave reasoning and cautious reasoning. As a second contribution we classify the computational complexity of counting the number of stable expansions of a given knowledge base. To the best of our knowledge this is the first paper analyzing the counting problem for autoepistemic logic.
Cite as

Nadia Creignou, Arne Meier, Michael Thomas, and Heribert Vollmer. The Complexity of Reasoning for Fragments of Autoepistemic Logic. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{creignou_et_al:DagSemProc.10061.6,
  author =	{Creignou, Nadia and Meier, Arne and Thomas, Michael and Vollmer, Heribert},
  title =	{{The Complexity of Reasoning for Fragments of Autoepistemic Logic}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.6},
  URN =		{urn:nbn:de:0030-drops-25234},
  doi =		{10.4230/DagSemProc.10061.6},
  annote =	{Keywords: Autoepistemic logic, computational complexity, nonmonotonic reasoning, Post's lattice}
}
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