Flat modal fixpoint logics with the converse modality

DOI10.1093/LOGCOM/EXY016MaRDI QIDQ4612435zbMATH OpenOpenAlexWikidataFDO

Authors Sebastian Enqvist

Publication date 31 January 2019

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1710.04628

zbMATH Keywords

networkcompletenessmu-calculusconverse modalitymodal fixpoint logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70)

Abstract: We prove a generic completeness result for a class of modal fixpoint logics corresponding to flat fragments of the two-way mu-calculus, extending earlier work by Santocanale and Venema. We observe that Santocanale and Venema's proof that least fixpoints in the Lindenbaum-Tarski algebra of certain flat fixpoint logics are constructive, using finitary adjoints, no longer works when the converse modality is introduced. Instead, our completeness proof directly constructs a model for a consistent formula, using the induction rule in a way that is similar to the standard completeness proof for propositional dynamic logic. This approach is combined with the concept of a focus, which has previously been used in tableau based reasoning for modal fixpoint logics.

Recommendations

• Completeness for flat modal fixpoint logics
• Completeness for Flat Modal Fixpoint Logics
• Modal fixed point logics

Cited in

(3)

• Completeness for Flat Modal Fixpoint Logics
• The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games
• Completeness for flat modal fixpoint logics

This page was built for publication: Flat modal fixpoint logics with the converse modality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4612435)