2 papers
cs.LO2025
Interpolation for Converse PDL
Johannes Kloibhofer, Valentina Trucco Dalmas, Yde Venema
Converse PDL is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse PDL enjoys the (local) Craig Interpolation…
cs.LO2025
Interpolation for the two-way modal mu-calculus
Johannes Kloibhofer, Yde Venema
The two-way modal mu-calculus is the extension of the (standard) one-way mu-calculus with converse (backward-looking) modalities. For this logic we introduce two new sequent-style…