5 Search Results for "Fermüller, Christian G."

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.12
The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives

Authors: Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
This paper studies the rational synthesis problem for multi-player games played on graphs when rational players are following subgame perfect equilibria. In these games, one player, the system, declares his strategy upfront, and the other players, composing the environment, then rationally respond by playing strategies forming a subgame perfect equilibrium. We study the complexity of the rational synthesis problem when the players have ω-regular objectives encoded as parity objectives. Our algorithm is based on an encoding into a three-player game with imperfect information, showing that the problem is in 2ExpTime. When the number of environment players is fixed, the problem is in ExpTime and is NP- and coNP-hard. Moreover, for a fixed number of players and reachability objectives, we get a polynomial algorithm.
Cite as

Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard. The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2025.12,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Reynouard, Alexis and Van Den Bogaard, Marie},
  title =	{{The Non-Cooperative Rational Synthesis Problem for SPEs and \omega-Regular Objectives}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.12},
  URN =		{urn:nbn:de:0030-drops-239622},
  doi =		{10.4230/LIPIcs.CONCUR.2025.12},
  annote =	{Keywords: non-zero-sum games, subgame perfect equilibria, rational synthesis}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.9
Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Authors: Helle Hvid Hansen and Wolfgang Poiger

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra 𝐀 of truth-degrees. More precisely, we work with coalgebraic modal logic via 𝐀-valued predicate liftings where 𝐀 is an FLew-algebra, and interpret actions (abstracting programs and games) as 𝖥-coalgebras where the functor 𝖥 represents some type of 𝐀-weighted system. We also allow combinations of crisp propositions with 𝐀-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for 𝟐-valued iteration-free PDL with 𝐀-valued accessibility relations when 𝐀 is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.
Cite as

Helle Hvid Hansen and Wolfgang Poiger. Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hansen_et_al:LIPIcs.CALCO.2025.9,
  author =	{Hansen, Helle Hvid and Poiger, Wolfgang},
  title =	{{Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{9:1--9:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.9},
  URN =		{urn:nbn:de:0030-drops-235681},
  doi =		{10.4230/LIPIcs.CALCO.2025.9},
  annote =	{Keywords: dynamic logic, many-valued coalgebraic logic, safety, strong completeness}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2025.4
Playing with Modalities (Invited Talk)

Authors: Elaine Pimentel, Carlos Olarte, Timo Lang, Robert Freiman, and Christian G. Fermüller

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

Abstract
In this work, we will explore modalities through dialogical game lenses. Games provide a powerful tool for bridging the gap between intended and formal semantics, often offering a more conceptually natural approach to logic than traditional model-theoretic semantics. We begin by exploring substructural calculi from a game semantic perspective, driven by intuitions about resource-consciousness and, more specifically, cost-sensitive reasoning. The game comes into full swing as we introduce cost labels to assumptions and a corresponding budget. Different proofs of the same end-sequent are interpreted as strategies for a player to defend a claim, which vary in cost. This leads to a labelled calculus, which can be viewed as a fragment of subexponential linear logic. We conclude this first part with a discussion of cut-admissibility for the proposed system. In the second part, we show that our games offer an interesting insight also into modal logics. More precisely, we will focus on the modal logic PNL, characterised by Kripke frames with two types of disjoint and symmetric reachability relations. This framework is motivated by the study of group polarisation, where the opinions or beliefs of individuals within a group become more extreme or polarised after interaction. Our approach to reasoning about group polarisation is based on PNL and highlights a different aspect of formal reasoning about the corresponding models - using games and proof systems. We conclude by outlining potential directions for future research.
Cite as

Elaine Pimentel, Carlos Olarte, Timo Lang, Robert Freiman, and Christian G. Fermüller. Playing with Modalities (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pimentel_et_al:LIPIcs.CSL.2025.4,
  author =	{Pimentel, Elaine and Olarte, Carlos and Lang, Timo and Freiman, Robert and Ferm\"{u}ller, Christian G.},
  title =	{{Playing with Modalities}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{4:1--4:20},
  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.4},
  URN =		{urn:nbn:de:0030-drops-227614},
  doi =		{10.4230/LIPIcs.CSL.2025.4},
  annote =	{Keywords: Linear logic, modal logic, proof theory, game semantics}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2021.6
Unit Propagation with Stable Watches (Short Paper)

Authors: Ashlin Iser and Tomáš Balyo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Unit propagation is the hottest path in CDCL SAT solvers, therefore the related data-structures, algorithms and implementation details are well studied and highly optimized. State-of-the-art implementations are based on reduced occurrence tracking with two watched literals per clause and one blocking literal per watcher in order to further reduce the number of clause accesses. In this paper, we show that using runtime statistics for watched literal selection can improve the performance of state-of-the-art SAT solvers. We present a method for efficiently keeping track of spans during which literals are satisfied and using this statistic to improve watcher selection. An implementation of our method in the SAT solver CaDiCaL can solve more instances of the SAT Competition 2019 and 2020 benchmark sets and is specifically strong on satisfiable cryptographic instances.
Cite as

Ashlin Iser and Tomáš Balyo. Unit Propagation with Stable Watches (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{iser_et_al:LIPIcs.CP.2021.6,
  author =	{Iser, Ashlin and Balyo, Tom\'{a}\v{s}},
  title =	{{Unit Propagation with Stable Watches}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{6:1--6:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.6},
  URN =		{urn:nbn:de:0030-drops-152973},
  doi =		{10.4230/LIPIcs.CP.2021.6},
  annote =	{Keywords: Unit Propagation, Two-Watched Literals, Literal Stability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.94
Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic

Authors: Matthias Baaz and Christian G. Fermüller

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

Abstract
The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.
Cite as

Matthias Baaz and Christian G. Fermüller. Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 94-109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baaz_et_al:LIPIcs.CSL.2015.94,
  author =	{Baaz, Matthias and Ferm\"{u}ller, Christian G.},
  title =	{{Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{94--109},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.94},
  URN =		{urn:nbn:de:0030-drops-54097},
  doi =		{10.4230/LIPIcs.CSL.2015.94},
  annote =	{Keywords: Cut-elimination, sequent calculus, intuitionistic logic}
}
  • Refine by Type
  • 5 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2021
  • 1 2015

  • Refine by Author
  • 2 Fermüller, Christian G.
  • 1 Baaz, Matthias
  • 1 Balyo, Tomáš
  • 1 Bruyère, Véronique
  • 1 Freiman, Robert
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Modal and temporal logics
  • 1 Theory of computation
  • 1 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Linear logic
  • 1 Theory of computation → Program reasoning
  • Show More...

  • Refine by Keyword
  • 1 Cut-elimination
  • 1 Linear logic
  • 1 Literal Stability
  • 1 Two-Watched Literals
  • 1 Unit Propagation
  • 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