8 Search Results for "Kaiser, Lukasz"

Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2023.2
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)

Authors: Robbert Krebbers

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
In program verification, it is common to embed a high-level object logic into the meta logic of a proof assistant to hide low-level aspects of the verification. To verify imperative and concurrent programs, separation logic hides explicit reasoning about heaps and pointer disjointness. To verify programs with cyclic features such as modules or higher-order state, modal logic provides modalities to hide explicit reasoning about step-indices that are used to stratify recursion. The meta logic of proof assistants such as Coq is well suited to embed high-level object logics and prove their soundness. However, proof assistants such as Coq do not have native infrastructure to facilitate proofs in embedded logics - their proof contexts and built-in tactics for interactive and automated proofs are tailored to the connectives of the meta logic, and do not extend to those of the object logic. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic. In this talk I will describe our work in the Iris project to address this problem - first for interactive proofs, and then for semi-automated proofs. The Iris Proof Mode provides high-level tactics for interactive proofs in higher-order concurrent separation logic with modalities. Recent work on RefinedC and Diaframe have built on top of the Iris Proof Mode to obtain proof automation for low-level C programs and fine-grained concurrent programs.
Cite as

Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{krebbers:LIPIcs.ITP.2023.2,
  author =	{Krebbers, Robbert},
  title =	{{Interactive and Automated Proofs in Modal Separation Logic}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.2},
  URN =		{urn:nbn:de:0030-drops-183770},
  doi =		{10.4230/LIPIcs.ITP.2023.2},
  annote =	{Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.441
A Unified Approach to Boundedness Properties in MSO

Authors: Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
In the past years, extensions of monadic second-order logic (MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. In this work, we propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide a decidability proof for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resource-automatic structures.
Cite as

Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding. A Unified Approach to Boundedness Properties in MSO. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 441-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.CSL.2015.441,
  author =	{Kaiser, Lukasz and Lang, Martin and Le{\ss}enich, Simon and L\"{o}ding, Christof},
  title =	{{A Unified Approach to Boundedness Properties in MSO}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{441--456},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.441},
  URN =		{urn:nbn:de:0030-drops-54309},
  doi =		{10.4230/LIPIcs.CSL.2015.441},
  annote =	{Keywords: quantitative logics, monadic second order logic, boundedness, automatic structures, tree automata}
}
Document
DOI: 10.4230/LIPIcs.STACS.2015.34
Graph Searching Games and Width Measures for Directed Graphs

Authors: Saeed Akhoondian Amiri, Lukasz Kaiser, Stephan Kreutzer, Roman Rabinovich, and Sebastian Siebertz

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
In cops and robber games a number of cops tries to capture a robber in a graph. A variant of these games on undirected graphs characterises tree width by the least number of cops needed to win. We consider cops and robber games on digraphs and width measures (such as DAG-width, directed tree width or D-width) corresponding to them. All of them generalise tree width and the game characterising it. For the DAG-width game we prove that the problem to decide the minimal number of cops required to capture the robber (which is the same as deciding DAG-width), is PSPACE-complete, in contrast to most other similar games. We also show that the cop-monotonicity cost for directed tree width games cannot be bounded by any function. As a consequence, D-width is not bounded in directed tree width, refuting a conjecture by Safari. A large number of directed width measures generalising tree width has been proposed in the literature. However, only very little was known about the relation between them, in particular about whether classes of digraphs of bounded width in one measure have bounded width in another. In this paper we establish an almost complete order among the most prominent width measures with respect to mutual boundedness.
Cite as

Saeed Akhoondian Amiri, Lukasz Kaiser, Stephan Kreutzer, Roman Rabinovich, and Sebastian Siebertz. Graph Searching Games and Width Measures for Directed Graphs. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 34-47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{akhoondianamiri_et_al:LIPIcs.STACS.2015.34,
  author =	{Akhoondian Amiri, Saeed and Kaiser, Lukasz and Kreutzer, Stephan and Rabinovich, Roman and Siebertz, Sebastian},
  title =	{{Graph Searching Games and Width Measures for Directed Graphs}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{34--47},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.34},
  URN =		{urn:nbn:de:0030-drops-49020},
  doi =		{10.4230/LIPIcs.STACS.2015.34},
  annote =	{Keywords: cops and robber games, directed graphs, DAG-width}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.366
A Counting Logic for Structure Transition Systems

Authors: Lukasz Kaiser and Simon Leßenich

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Quantitative questions such as "what is the maximum number of tokens in a place of a Petri net?" or "what is the maximal reachable height of the stack of a pushdown automaton?" play a significant role in understanding models of computation. To study such problems in a systematic way, we introduce structure transition systems on which one can define logics that mix temporal expressions (e.g. reachability) with properties of a state (e.g. the height of the stack). We propose a counting logic Qmu[#MSO] which allows to express questions like the ones above, and also many boundedness problems studied so far. We show that Qmu[#MSO] has good algorithmic properties, in particular we generalize two standard methods in model checking, decomposition on trees and model checking through parity games, to this quantitative logic. These properties are used to prove decidability of Qmu[#MSO] on tree-producing pushdown systems, a generalization of both pushdown systems and regular tree grammars.
Cite as

Lukasz Kaiser and Simon Leßenich. A Counting Logic for Structure Transition Systems. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 366-380, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.CSL.2012.366,
  author =	{Kaiser, Lukasz and Le{\ss}enich, Simon},
  title =	{{A Counting Logic for Structure Transition Systems}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{366--380},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.366},
  URN =		{urn:nbn:de:0030-drops-36848},
  doi =		{10.4230/LIPIcs.CSL.2012.366},
  annote =	{Keywords: Logic in Computer Science, Quantitative Logics, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.STACS.2012.577
The Field of Reals is not omega-Automatic

Authors: Faried Abu Zaid, Erich Grädel, and Lukasz Kaiser

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Abstract
We investigate structural properties of omega-automatic presentations of infinite structures in order to sharpen our methods to determine whether a given structure is omega-automatic. We apply these methods to show that no field of characteristic 0 admits an injective omega-automatic presentation, and that uncountable fields with a definable linear order cannot be omega-automatic.
Cite as

Faried Abu Zaid, Erich Grädel, and Lukasz Kaiser. The Field of Reals is not omega-Automatic. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 577-588, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{abuzaid_et_al:LIPIcs.STACS.2012.577,
  author =	{Abu Zaid, Faried and Gr\"{a}del, Erich and Kaiser, Lukasz},
  title =	{{The Field of Reals is not omega-Automatic}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{577--588},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.577},
  URN =		{urn:nbn:de:0030-drops-34234},
  doi =		{10.4230/LIPIcs.STACS.2012.577},
  annote =	{Keywords: Logic, Algorithmic Model Theory, Automatic Structures}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.387
A Perfect-Information Construction for Coordination in Games

Authors: Dietmar Berwanger, Lukasz Kaiser, and Bernd Puchala

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
We present a general construction for eliminating imperfect information from games with several players who coordinate against nature, and to transform them into two-player games with perfect information while preserving winning strategy profiles. The construction yields an infinite game tree with epistemic models associated to nodes. To obtain a more succinct representation, we define an abstraction based on homomorphic equivalence, which we prove to be sound for games with observable winning conditions. The abstraction generates finite game graphs in several relevant cases, and leads to a new semi-decision procedure for multi-player games with imperfect information.
Cite as

Dietmar Berwanger, Lukasz Kaiser, and Bernd Puchala. A Perfect-Information Construction for Coordination in Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 387-398, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{berwanger_et_al:LIPIcs.FSTTCS.2011.387,
  author =	{Berwanger, Dietmar and Kaiser, Lukasz and Puchala, Bernd},
  title =	{{A Perfect-Information Construction for Coordination in Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{387--398},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.387},
  URN =		{urn:nbn:de:0030-drops-33354},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.387},
  annote =	{Keywords: Distributed Synthesis, Games on Graphs, Imperfect Information, Epistemic Models}
}
Document
DOI: 10.4230/LIPIcs.STACS.2008.1352
Model Checking Games for the Quantitative µ-Calculus

Authors: Diana Fischer, Erich Grädel, and Lukasz Kaiser

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract
We investigate quantitative extensions of modal logic and the modal $mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $mu$-calculus.
Cite as

Diana Fischer, Erich Grädel, and Lukasz Kaiser. Model Checking Games for the Quantitative µ-Calculus. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 301-312, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{fischer_et_al:LIPIcs.STACS.2008.1352,
  author =	{Fischer, Diana and Gr\"{a}del, Erich and Kaiser, Lukasz},
  title =	{{Model Checking Games for the Quantitative µ-Calculus}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{301--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1352},
  URN =		{urn:nbn:de:0030-drops-13525},
  doi =		{10.4230/LIPIcs.STACS.2008.1352},
  annote =	{Keywords: Games, logic, model checking, quantitative logics}
}
Document
DOI: 10.4230/LIPIcs.STACS.2008.1360
Cardinality and counting quantifiers on omega-automatic structures

Authors: Lukasz Kaiser, Sasha Rubin, and Vince Bárány

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract
We investigate structures that can be represented by omega-automata, so called omega-automatic structures, and prove that relations defined over such structures in first-order logic expanded by the first-order quantifiers `there exist at most $aleph_0$ many', 'there exist finitely many' and 'there exist $k$ modulo $m$ many' are omega-regular. The proof identifies certain algebraic properties of omega-semigroups. As a consequence an omega-regular equivalence relation of countable index has an omega-regular set of representatives. This implies Blumensath's conjecture that a countable structure with an $omega$-automatic presentation can be represented using automata on finite words. This also complements a very recent result of Hj"orth, Khoussainov, Montalban and Nies showing that there is an omega-automatic structure which has no injective presentation.
Cite as

Lukasz Kaiser, Sasha Rubin, and Vince Bárány. Cardinality and counting quantifiers on omega-automatic structures. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 385-396, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.STACS.2008.1360,
  author =	{Kaiser, Lukasz and Rubin, Sasha and B\'{a}r\'{a}ny, Vince},
  title =	{{Cardinality and counting quantifiers on omega-automatic structures}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{385--396},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1360},
  URN =		{urn:nbn:de:0030-drops-13602},
  doi =		{10.4230/LIPIcs.STACS.2008.1360},
  annote =	{Keywords: \$omega\$-automatic presentations, \$omega\$-semigroups, \$omega\$-automata}
}
  • Refine by Author
  • 7 Kaiser, Lukasz
  • 2 Grädel, Erich
  • 2 Leßenich, Simon
  • 1 Abu Zaid, Faried
  • 1 Akhoondian Amiri, Saeed
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Program verification
  • 1 Theory of computation → Separation logic

  • Refine by Keyword
  • 2 quantitative logics
  • 1 $omega$-automata
  • 1 $omega$-automatic presentations
  • 1 $omega$-semigroups
  • 1 Algorithmic Model Theory
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 2 2008
  • 2 2012
  • 2 2015
  • 1 2011
  • 1 2023

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