Coalgebraic Announcement Logics - Gorin, Daniel; Schröder, Lutz; Carreiro, Facundo (Proc. 40th International Colloquium on Automata, Languages, and Programming, ICALP 2013, Part II, 2013)
In epistemic logic, dynamic operators describe the evolution of the knowledge of participating agents through communication, one of the most basic forms of communication being public announcement. Semantically, dynamic operators correspond to transformations of the underlying model. While metatheoretic results on dynamic epistemic logic so far are largely limited to the setting of Kripke models, there is evident interest in extending its scope to non-relational modalities capturing, e.g., uncertainty or collaboration. We develop a generic framework for non-relational dynamic logic by adding dynamic operators to coalgebraic logic. We discuss a range of examples and establish basic results including bisimulation invariance, complexity, and a small model property. © 2013 Springer-Verlag.
UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes_1.coalge_9

COOL — A Generic Reasoner for Coalgebraic Hybrid Logics (System Description) - Gorin, Daniel; Pattinson, Dirk; Schröder, Lutz; Widmann, Florian; Wißmann, Thorsten (Automated Reasoning, 2014)
We describe the Coalgebraic Ontology Logic solver Cool, a generic reasoner that decides the satisfiability of modal (and, more generally, hybrid) formulas with respect to a set of global assumptions-in Description Logic parlance, we support a general TBox and internalize a Boolean ABox. The level of generality is that of coalgebraic logic, a logical framework covering a wide range of modal logics, beyond relational semantics. The core of Cool is an efficient unlabelled tableaux search procedure using global caching. Concrete logics are added by implemening the corresponding (one-step) tableaux rules. The logics covered at the moment include standard relational examples as well as graded modal logic and Pauly's Coalition Logic (the next-step fragment of Alternating-time Temporal Logic), plus every logic that arises as a fusion of the above. We compare the performance of Cool with state-of-the-art reasoners. © 2014 Springer International Publishing Switzerland.
UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.coolag

Extending ALCQ With Bounded Self-Reference - Gorin, Daniel; Schröder, Lutz (Advances in Modal Logic, 2012)
UnivIS-Import:2015-04-16:Pub.2012.tech.IMMD.profes_1.extend

Narcissists Are Easy, Stepmothers Are Hard - Gorin, Daniel; Schröder, Lutz (Foundations of Software Science and Computational Structures Foundations of Software Science and Computational Structures, 2012)
Modal languages are well-known for their robust decidability and relatively low complexity. However, as soon as one adds a self-referencing construct, like hybrid logic's down-arrow binder, to the basic modal language, decidability is lost, even if one restricts binding to a single variable. Here, we concentrate on the latter case and investigate the logics obtained by restricting the nesting depth of modalities between binding and use. In particular, for distances strictly below 3 we obtain well-behaved logics with a relatively high descriptive power. We investigate the fragment with distance 1 in the framework of coalgebraic modal logic, for which we provide very general decidability and complexity results. For the fragment with distance 2 we focus on the case of Kripke semantics and obtain optimum complexity bounds (no harder than the base logic). We show that this fragment is expressive enough to accommodate the guarded fragment over the correspondence language. © 2012 Springer-Verlag Berlin Heidelberg.
UnivIS-Import:2015-04-16:Pub.2012.tech.IMMD.profes_1.narcis

Ontological Modelling of a Psychiatric Clinical Practice Guideline - Gorin, Daniel; Meyn, Malte; Naumann, Alexander; Polzer, Miriam; Rabenstein, Ulrich; Schröder, Lutz (KI 2017: Advances in Artificial Intelligence - 40th Annual German Conference on AI, Dortmund, Germany, September 25-29, 2017, Proceedings, 2017)

Reasoning with Bounded Self-reference Using Logical Interpreters - Gorin, Daniel; Schröder, Lutz; Wißmann, Thorsten (Proc. 26th International Workshop on Description Logics, DL 2013, 2013)
Self-referential concepts in description logic may formally be viewed as concepts that at some point mention an individual previously encountered in the evaluation; this corresponds to a restricted form of the down-arrow binder known from hybrid logic. Typical examples include being a narcissist, (someone who loves himself); a celebrity (someone who is known by everyone she meets) or a grant application reviewer (who can only review proposals of researchers with whom she did not collaborate in the past). While reasoning in ALC plus self-reference is known to be undecidable, it has recently been shown that one can often safely restrict self-reference to at most two indirections (allowing the definition of narcissists and celebrities, but not of grant reviewers). In particular, the extension of ALCQ with this construct has an expressive power roughly equivalent to ALCHIQ plus safe Boolean combinations of roles. Here, we discuss a translation-based approach to reasoning in this logic. The translation goes into ALCHIQ (without Boolean roles) and therefore can be used in combination with off-the-shelf reasoners for OWL. The translation strategy encodes the semantics of the source axiomatically in the target logic. We use an implementation of this type of translations to evaluate the feasibility of the whole approach.
UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes_1.reason

Simulations and Bisimulations For Coalgebraic Modal Logics - Gorin, Daniel; Schröder, Lutz (5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, 2013)
Simulations serve as a proof tool to compare the behaviour of reactive systems. We define a notion of Λ-simulation for coalgebraic modal logics, parametric in the choice of a set Λ of monotone predicate liftings for a functor T. That is, we obtain a generic notion of simulation that can be flexibly instantiated to a large variety of systems and logics, in particular in settings that semantically go beyond the classical relational setup, such as probabilistic, game-based, or neighbourhood-based systems. We show that this notion is adequate in several ways: i) Λ-simulations preserve truth of positive formulas, ii) for Λ a separating set of monotone predicate liftings, the associated notion of Λ-bisimulation corresponds to T-behavioural equivalence (moreover, this correspondence extends to the respective finite-lookahead counterparts), and iii) Λ-bisimulations remain sound when taken up to difunctional closure. In essence, we arrive at a modular notion of equivalence that, when used with a separating set of monotone predicate liftings, coincides with T-behavioural equivalence regardless of whether T preserves weak pullbacks. That is, for finitary set-based coalgebras, Λ-bisimulation works under strictly more general assumptions than T-bisimulation in the sense of Aczel and Mendler. © 2013 Springer-Verlag Berlin Heidelberg.
UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes_1.simula

Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics - Gorin, Daniel; Schröder, Lutz (Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic,", 2014)
While reasoning in a logic extending a complete Boolean basis is coNP-hard, re- stricting to conjunctive fragments of modal languages sometimes allows for tractable reasoning even in the presence of greatest fixpoints. One such example is the EL family of description logics; here, eficient reasoning is based on satisfaction checking in suitable small models that characterize formulas in terms of simulations. It is well- known, though, that not every conjunctive modal language has a tractable reasoning problem. Natural questions are then how common such tractable fragments are and how to identify them. In this work we provide suficient conditions for tractability in a general way by considering unlabeled tableau rules for a given modal logic. We work in the framework of coalgebraic modal logics as unifying semantic setting. Apart from recovering known results for description logics such as and 0, we obtain new ones for conjunctive fragments of relational and non-relational modal logics with greatest fixpoints. Most notably we find tractable fragments of game logic and the alternating-time μ-calculus.
UnivIS-Import:2015-03-09:Pub.2014.tech.IMMD.profes_1.subsum
Keywords: Convexity; Fixpoints; Materializers; Tractable reasoning