3 papers
cs.LO2026
Witnesses for Fixpoint Games on Lattices
Barbara König, Karla Messing
We construct witnesses that can be used to derive strategies in fixpoint games and provide proof that the least fixpoint of a function is either above or not below some given bound…
cs.LO2025
Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems (Full Version)
Barbara König, Arend Rensink, Lara Stoltenow +1
This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class…
cs.LO2024
Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions
Lara Stoltenow, Barbara König, Sven Schneider +3
We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability an…