The two-way modal μ-calculus is the extension of the (standard) one-way μ-calculus with converse (backward-looking) modalities. For this logic we introduce two new sequent-style proof calculi: a non-wellfounded system admitting infinite branches and a finitary, cyclic version of this that employs annotations.As is common in sequent systems for two-way modal logics, our calculi feature an analytic cut rule. What distinguishes our approach is the use of so-called trace atoms, which serve to apply Vardi’s two-way automata in a proof-theoretic setting.We prove soundness and completeness for both systems and subsequently use the cyclic calculus to show that the two-way μ-calculus has the (local) Craig interpolation property, with respect to both propositions and modalities. Our proof uses a version of Maehara’s method adapted to cyclic proof systems. As a corollary we prove that the two-way μ-calculus also enjoys Beth’s definability property.

Abstract Converse $$\textsf{PDL}$$ PDL is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse $$\textsf{PDL}$$ PDL enjoys the (local) Craig Interpolation Property, with respect to both atomic programs and propositional variables. As a corollary we establish the Beth Definability Property for the logic. Our interpolation proof is based on an adaptation of Maehara’s proof-theoretic method. For this purpose we introduce a sound and complete cyclic sequent system for this logic. This calculus features an analytic cut rule and uses a focus mechanism for recognising successful cycles.

Abstract We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations.

Abstract Automata operating on infinite objects feature prominently in the theory of the modal $$\mu $$ -calculus. One such application concerns the tableau games introduced by Niwiński & Walukiewicz, of which the winning condition for infinite plays can be naturally checked by a nondeterministic parity stream automaton. Inspired by work of Jungteerapanich and Stirling we show how determinization constructions of this automaton may be used to directly obtain proof systems for the $$\mu $$ -calculus. More concretely, we introduce a binary tree construction for determinizing nondeterministic parity stream automata. Using this construction we define the annotated cyclic proof system $$\textsf{BT}$$ , where formulas are annotated by tuples of binary strings. Soundness and Completeness of this system follow almost immediately from the correctness of the determinization method.

Many algorithmic results on the modal mu-calculus use representations of formulas such as alternating tree automata or hierarchical equation systems. At closer inspection, these results are not always optimal, since the exact relation between the formula and its representation is not clearly understood. In particular, there has been confusion about the definition of the fundamental notion of the size of a mu-calculus formula. We propose the notion of a parity formula as a natural way of representing a mu-calculus formula, and as a yardstick for measuring its complexity. We discuss the close connection of this concept with alternating tree automata, hierarchical equation systems and parity games. We show that well-known size measures for mu-calculus formulas correspond to a parity formula representation of the formula using its syntax tree, subformula graph or closure graph, respectively. Building on work by Bruse, Friedmann & Lange we argue that for optimal complexity results one needs to work with the closure graph, and thus define the size of a formula in terms of its Fischer-Ladner closure. As a new observation, we show that the common assumption of a formula being clean, that is, with every variable bound in at most one subformula, incurs an exponential blow-up of the size of the closure. To realise the optimal upper complexity bound of model checking for all formulas, our main result is to provide a construction of a parity formula that (a) is based on the closure graph of a given formula, (b) preserves the alternation-depth but (c) does not assume the input formula to be clean.

Algorithms for solving computational problems related to the modal μ-calculus generally do not take the formulas themselves as input, but operate on some kind of representation of formulas. This representation is usually based on a graph structure that one may associate with a μ-calculus formula. Recent work by Kupke, Marti & Venema showed that the operation of renaming bound variables may incur an exponential blow-up of the size of such a graph representation. Their example revealed the undesirable situation that standard constructions, on which algorithms for model checking and satisfiability depend, are sensitive to the specific choice of bound variables used in a formula.

A landmark result in the study of logics for formal verification is Janin and Walukiewicz’s theorem, stating that the modal μ-calculus (μML) is equivalent modulo bisimilarity to standard monadic second-order logic (here abbreviated as SMSO) over the class of labelled transition systems (LTSs for short). Our work proves two results of the same kind, one for the alternation-free or noetherian fragment μ N ML of μML on the modal side and one for WMSO, weak monadic second-order logic, on the second-order side. In the setting of binary trees, with explicit functions accessing the left and right successor of a node, it was known that WMSO is equivalent to the appropriate version of alternation-free μ-calculus. Our analysis shows that the picture changes radically once we consider, as Janin and Walukiewicz did, the standard modal μ-calculus, interpreted over arbitrary LTSs. The first theorem that we prove is that, over LTSs, μ N ML is equivalent modulo bisimilarity to noetherian MSO (NMSO), a newly introduced variant of SMSO where second-order quantification ranges over “conversely well-founded” subsets only. Our second theorem starts from WMSO and proves it equivalent modulo bisimilarity to a fragment of μ N ML defined by a notion of continuity. Analogously to Janin and Walukiewicz’s result, our proofs are automata-theoretic in nature: As another contribution, we introduce classes of parity automata characterising the expressiveness of WMSO and NMSO (on tree models) and of μ C ML and μ N ML (for all transition systems).

Using the theory of coalgebra, we introduce a uniform framework for adding modalities to the language of propositional geometric logic. Models for this logic are based on coalgebras for an endofunctor T on some full subcategory of the category Top of topological spaces and continuous functions. We compare the notions of modal equivalence, behavioural equivalence and bisimulation on the resulting class of models, and we provide a final object for the corresponding category. Furthermore, we specify a method of lifting an endofunctor on Set, accompanied by a collection of predicate liftings, to an endofunctor on the category of topological spaces.

In this work, we provide a simple coalgebraic characterisation of regular omega-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Omega-automata. In earlier work we introduced Omega-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Omega-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Omega-automata are expressively complete for the regular omega-languages. We show that, due to their coalgebraic nature, Omega-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Omega-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular omega-languages.

Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone μ -calculus, the variant of the polymodal μ -calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone μ -calculus.

This paper contributes to the theory of the modal $\mu$-calculus by proving some model-theoretic results. More in particular, we discuss a number of semantic properties pertaining to formulas of the modal $\mu$-calculus. For each of these properties we provide a corresponding syntactic fragment, in the sense that a $\mu$-formula $\xi$ has the given property iff it is equivalent to a formula $\xi'$ in the corresponding fragment. Since this formula $\xi'$ will always be effectively obtainable from $\xi$, as a corollary, for each of the properties under discussion, we prove that it is decidable in elementary time whether a given $\mu$-calculus formula has the property or not. The properties that we study all concern the way in which the meaning of a formula $\xi$ in a model depends on the meaning of a single, fixed proposition letter $p$. For example, consider a formula $\xi$ which is monotone in $p$; such a formula a formula $\xi$ is called continuous (respectively, fully additive), if in addition it satisfies the property that, if $\xi$ is true at a state $s$ then there is a finite set (respectively, a singleton set) $U$ such that $\xi$ remains true at $s$ if we restrict the interpretation of $p$ to the set $U$. Each of the properties that we consider is, in a similar way, associated with one of the following special kinds of subset of a tree model: singletons, finite sets, finitely branching subtrees, noetherian subtrees (i.e., without infinite paths), and branches. Our proofs for these characterization results will be automata-theoretic in nature; we will see that the effectively defined maps on formulas are in fact induced by rather simple transformations on modal automata. Thus our results can also be seen as a contribution to the model theory of modal automata.

Modal fixpoint logics traditionally play a central role in computer science, in particular in artificial intelligence and concurrency. The μ-calculus and its relatives are among the most expressive logics of this type. However, popular fixpoint logics tend to trade expressivity for simplicity and readability and in fact often live within the single variable fragment of the μ-calculus. The family of such flat fixpoint logics includes, e.g., Linear Temporal Logic (LTL), Computation Tree Logic (CTL), and the logic of common knowledge. Extending this notion to the generic semantic framework of coalgebraic logic enables covering a wide range of logics beyond the standard μ-calculus including, e.g., flat fragments of the graded μ-calculus and the alternating-time μ-calculus (such as alternating-time temporal logic), as well as probabilistic and monotone fixpoint logics. We give a generic proof of completeness of the Kozen-Park axiomatization for such flat coalgebraic fixpoint logics.

We present the concept of a disjunctive basis as a generic framework for normal forms in modal logic based on coalgebra. Disjunctive bases were defined in previous work on completeness for modal fixpoint logics, where they played a central role in the proof of a generic completeness theorem for coalgebraic mu-calculi. Believing the concept has a much wider significance, here we investigate it more thoroughly in its own right. We show that the presence of a disjunctive basis at the "one-step" level entails a number of good properties for a coalgebraic mu-calculus, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. Based on this, we prove a Lyndon theorem for the full fixpoint logic, its fixpoint-free fragment and its one-step fragment, and a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free fragment. We also raise the questions, when a disjunctive basis exists, and how disjunctive bases are related to Moss' coalgebraic "nabla" modalities. Nabla formulas provide disjunctive bases for many coalgebraic modal logics, but there are cases where disjunctive bases give useful normal forms even when nabla formulas fail to do so, our prime example being graded modal logic. Finally, we consider the problem of giving a category-theoretic formulation of disjunctive bases, and provide a partial solution.

Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor. We then consider invariance under behavioral equivalence of MSO-formulas. More specifically, we investigate whether the coalgebraic mu-calculus is the bisimulation-invariant fragment of the monadic second-order language for a given functor. Using automatatheoretic techniques and building on recent results by the third author, we show that in order to provide such a characterization result it suffices to find what we call an adequate uniform construction for the coalgebraic type functor. As direct applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem for the modal mu-calculus, avoiding the use of syntactic normal forms, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors (including the "game functor"). As a more involved application, involving additional non-trivial ideas, we also derive a characterization theorem for the monotone modal mu-calculus, with respect to a natural monadic second-order language for monotone neighborhood models.

We introduce an axiomatization for the coalgebraic fixed point logic which was introduced by Venema as a generalization, based on Moss' coalgebraic modality, of the well-known modal mu-calculus. Our axiomatization can be seen as a generalization of Kozen's proof system for the modal mu-calculus to the coalgebraic level of generality. It consists of a complete axiomatization for Moss'modality, extended with Kozen's axiom and rule for the fixpoint operators. Our main result is a completeness theorem stating that, for functors that preserve weak pullbacks and restrict to finite sets, our axiomatization is sound and complete for the standard interpretation of the language in coalgebraic models. Our proof is based on automata-theoretic ideas: in particular, we introduce the notion of consequence game for modal automata, which plays a crucial role in the proof of our main result. The result generalizes the celebrated Kozen-Walukiewicz completeness theorem for the modal mu-calculus, and our automata-theoretic methods simplify parts of Walukiewicz' proof.

We use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoys uniform interpolation. To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e., functors with quasifunctorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.

Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic MSO(T) interpreted over co algebras for an arbitrary set functor T. Similar to well-known results for monadic second-order logic over trees, we provide a translation of this logic into a class of automata, relative to the class of T-co algebras that admit a tree-like supporting Kripke frame. We then consider invariance under behavioral equivalence of MSO(T)-formulas, more in particular, we investigate whether the co algebraic mu-calculus is the bisimulation-invariant fragment of MSO(T). Building on recent results by the third author we show that in order to provide such a co algebraic generalization of the Janin-Walukiewicz Theorem, it suffices to find what we call an adequate uniform construction for the functor T. As applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors. Finally, we consider in some detail the monotone neighborhood functor M, which provides co algebraic semantics for monotone modal logic. It turns out that there is no adequate uniform construction for M, whence the automata-theoretic approach towards bisimulation invariance does not apply directly. This problem can be overcome if we consider global bisimulations between neighborhood models: one of our main results provides a characterization of the monotone modal mu-calculus extended with the global modalities, as the fragment of monadic second order logic for the monotone neighborhood functor that is invariant for global bisimulations.

We provide a characterization theorem, in the style of van Benthem and Janin-Walukiewicz, for the alternation-free fragment of the modal μ-calculus. For this purpose we introduce a variant of standard monadic second-order logic (MSO), which we call well-founded monadic second-order logic (WFMSO). When interpreted in a tree model, the second-order quantifiers of WFMSO range over subsets of conversely well-founded subtrees. The first main result of the paper states that the expressive power of WFMSO over trees exactly corresponds to that of weak MSO-automata. Using this automata-theoretic characterization, we then show that, over the class of all transition structures, the bisimulation-invariant fragment of WFMSO is the alternation-free fragment of the modal μ-calculus. As a corollary, we find that the logics WFMSO and WMSO (weak monadic second-order logic, where second-order quantification concerns finite subsets), are incomparable in expressive power.

This paper introduces an endofunctor VT on the category of frames that is parametrised by an endofunctor T on the category Set that satisfies certain constraints. This generalises Johnstone's construction of the Vietoris powerlocale in the sense that his construction is obtained by taking for T the finite covariant power set functor. Our construction of the T-powerlocale VT out of a frame is based on ideas from coalgebraic logic and makes explicit the connection between the Vietoris construction and Moss's coalgebraic cover modality. We show how to extend certain natural transformations between set functors to natural transformations between T-powerlocale functors. Finally, we prove that the operation VT preserves some properties of frames, such as regularity, zero-dimensionality and the combination of zero-dimensionality and compactness.

Applications of modal logics are abundant in computer science, and a large number of structurally different modal logics have been successfully employed in a diverse spectrum of application contexts. Coalgebraic semantics, on the other hand, provides a uniform and encompassing view on the large variety of specific logics used in particular domains. The coalgebraic approach is generic and compositional: tools and techniques simultaneously apply to a large class of application areas and can, moreover, be combined in a modular way. In particular, this facilitates a pick-and-choose approach to domain-specific formalisms, applicable across the entire scope of application areas, leading to generic software tools that are easier to design, to implement and to maintain. This paper substantiates the authors’ firm belief that the systematic exploitation of the coalgebraic nature of modal logic will not only have impact on the field of modal logic itself but also lead to significant progress in a number of areas within computer science, such as knowledge representation and concurrency/mobility.

We fix a logical connection (Stone ˧ Pred : Setop → BA given by 2 as a schizophrenic object) and study coalgebraic modal logic that is induced by a functor T: Set → Set that is finitary and standard and preserves weak pullbacks and finite sets. We prove that for any such T, the cover modality nabla is a left (and its dual delta is a right) adjoint relative to ω. We then consider monotone unary modalities arising from the logical connection and show that they all are left (or right) adjoints relative to ω.

Building on the fact that descriptive frames are coalgebras for the Vietoris functor on the category of Stone spaces, we introduce and study the concept of a Vietoris bisimulation between two descriptive modal models, together with the associated notion of bisimilarity. We prove that our notion of bisimilarity, which is defined in terms of relation lifting, coincides with Kripke bisimilarity (with respect to the underlying Kripke models), with behavioural equivalence, and with modal equivalence, but not with Aczel-Mendler bisimilarity. As a corollary, we obtain that the Vietoris functor does not preserve weak pullbacks. Comparing Vietoris bisimulations between descriptive models to Kripke bisimulations on the underlying Kripke models, we prove that the closure of such a Kripke bisimulation is a Vietoris bisimulation. As a corollary, we show that the collection of Vietoris bisimulations between two descriptive models forms a complete lattice. Finally, we provide a game-theoretic characterization of Vietoris bisimilarity.

Several researchers have collaborated to publish an overview of coalgebra and logic in the special issue of the Journal of Logic and Computation. They have informed that the idea of coalgebra is general enough to encompass structures that are not usually perceived as relational structures or transition systems. A coalgebra ξ resembles a topological space for TX=(PX)(2x) and helps in obtaining Chellas's conditional frames. Two states are defined in such a coalgebra to be behaviorally equivalent when they can be identified by some coalgebra morphism. This means in the case of deterministic automata that the two states induce the same accepted language. It is also observed that satisfiability of coalgebraic logic can be established in PSPACE and that complete coalgebraic logics have the finite model property.

Journal Article Algebraic and Coalgebraic Logic Corner Get access Yde Venema Yde Venema Institute for Logic, Language and Computation, University of Amsterdam Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 19, Issue 2, April 2009, Page 303, https://doi.org/10.1093/logcom/exn098 Published: 12 December 2008

We generalize some of the central results in automata theory to the abstraction level of coalgebras and thus lay out the foundations of a universal theory of automata operating on infinite objects. Let F be any set functor that preserves weak pullbacks. We show that the class of recognizable languages of F-coalgebras is closed under taking unions, intersections, and projections. We also prove that if a nondeterministic F-automaton accepts some coalgebra it accepts a finite one of the size of the automaton. Our main technical result concerns an explicit construction which transforms a given alternating F-automaton into an equivalent nondeterministic one, whose size is exponentially bound by the size of the original automaton.

We generalize some of the central results in automata theory to the abstraction level of coalgebras. In particular, we show that for any standard, weak pullback preserving functor F, the class of recognizable languages of F -coalgebras is closed under taking unions, intersections and projections. Our main technical result concerns a construction which transforms a given alternating F -automaton into an equivalent non-deterministic one.

Abstract We define an interpretation of modal languages with polyadic operators in modal languages that use monadic operators (diamonds) only. We also define a simulation operator which associates a logic Λsim in the diamond language with each logic Λ in the language with polyadic modal connectives. We prove that this simulation operator transfers several useful properties of modal logics, such as finite/recursive axiomatizability, frame completeness and the finite model property, canonicity and first-order definability.

Abstract We define a nontrivial variety of boolean algebras with operators such that every member of the variety is atomless. This shows that not every variety of boolean algebras with operators is generated by its atomic members, and thus establishes a strong incompleteness result in (multi-)modal logic.

Abstract With each projective geometry we can associate a Lyndon algebra. Such an algebra always satisfies Tarski's axioms for relation algebras and Lyndon algebras thus form an interesting connection between the fields of projective geometry and algebraic logic. In this paper we prove that if G is a class of projective geometries which contains an infinite projective geometry of dimension at least three, then the class L(G) of Lyndon algebras associated with projective geometries in G has an undecidable equational theory. In our proof we develop and use a connection between projective geometries and diagonal-free cylindric algebras.

A number of formal specification languages for knowledge-based systems has been developed. Characteristics for knowledge-based systems are a complex knowledge base and an inference engine which uses this knowledge to solve a given problem. Specification languages for knowledge-based systems have to cover both aspects. They have to provide the means to specify a complex and large amount of knowledge and they have to provide the means to specify the dynamic reasoning behavior of a knowledge-based system. We focus on the second aspect. For this purpose, we survey existing approaches for specifying dynamic behavior in related areas of research. In fact, we have taken approaches for the specification of information systems (Language for Conceptual Modeling and TROLL), approaches for the specification of database updates and logic programming (Transaction Logic and Dynamic Database Logic) and the generic specification framework of abstract state machines.

We introduce a modal language for talking about projective planes. This language is two-sorted, containing formulas to be evaluated at points and at lines, respectively. The language has two diamonds whose intended accessibility relations are the two directions of the incidence relation between points and lines. We provide a sound and complete axiomatization for the formulas that are valid in the class of projective planes. We also show that it is decidable whether a given formula is satisfiable in a projective plane, and we characterize the computational complexity of this satisfaction problem.

Abstract We prove that every rectangularly dense diagonal-free cylindric algebra is representable. As a corollary, we give finite, sound and complete axiomatizations for the finite-variable fragments of first order logic without equality and for multi-dimensional modal S5-logic.

Abstract Treating the existential quantification ∃νi as a diamond ♢i and the identity νi = νj as a constant δij, we study restricted versions of first order logic as if they were modal formalisms. This approach is closely related to algebraic logic, as the Kripke frames of our system have the type of the atom structures of cylindric algebras; the full cylindric set algebras are the complex algebras of the intended multidimensional frames called cubes. The main contribution of the paper is a characterization of these cube frames for the finite-dimensional case and, as a consequence of the special form of this characterization, a completeness theorem for this class. These results lead to finite, though unorthodox, derivation systems for several related formalisms, e.g. for the valid n-variable first order formulas, for type-free valid formulas and for the equational theory of representable cylindric algebras. The result for type-free valid formulas indicates a positive solution to Problem 4.16 of Henkin, Monk and Tarski [16].

Abstract We discuss a ‘negative’ way of defining frame classes in (multi)modal logic, and address the question of whether these classes can be axiomatized byderivation rules, the ‘non-ξ rules’, styled after Gabbay's Irreflexivity Rule. The main result of this paper is a metatheorem on completeness, of the following kind: If⋀is a derivation system having a set of axioms that are special Sahlqvist formulas and⋀+is the extension of⋀with a set of non-ξ rules, then⋀+is strongly sound and complete with respect to the class of frames determined by the axioms and the rules.

A Modal Logic for Chopping Intervals YDE VENEMA YDE VENEMA Faculteit Wiskunde en Informatica, Universiteit van AmsterdamPlantage Muidergracht 24, 1018 TV Amsterdam Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 1, Issue 4, September 1991, Pages 453–476, https://doi.org/10.1093/logcom/1.4.453 Published: 01 September 1991 Article history Received: 04 April 1990 Published: 01 September 1991