@string{hp_SergeyGoncharov="http://www8.informatik.uni-erlangen.de/~sergey/"} @string{hp_LutzSchröder="http://www8.informatik.uni-erlangen.de/schroeder/"} @string{hp_StefanMilius="http://www8.informatik.uni-erlangen.de/~milius/"} @string{hp_TadeuszLitak="http://www8.informatik.uni-erlangen.de/~litak/"} @string{hp_DanielGorín="http://www8.informatik.uni-erlangen.de/~gorin/"} % % 2014 % @inproceedings{DBLP:conf/fossacs/DahlqvistP13, author = {Fredrik Dahlqvist and Dirk Pattinson}, title = {Some Sahlqvist Completeness Results for Coalgebraic Logics}, booktitle = {FoSSaCS}, pages = {193-208}, editor = {Frank Pfenning}, booktitle = {Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7794}, year = {2013}, isbn = {978-3-642-37074-8}, ee = {http://dx.doi.org/10.1007/978-3-642-37075-5}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/corr/abs-1105-2246, author = {Corina C\^{\i}rstea and Clemens Kupke and Dirk Pattinson}, title = {EXPTIME Tableaux for the Coalgebraic mu-Calculus}, journal = {Logical Methods in Computer Science}, volume = {7}, nonumber = {3}, year = {2011}, ee = {http://dx.doi.org/10.2168/LMCS-7(3:3)2011}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/tcs/KupkeP11, author = {Clemens Kupke and Dirk Pattinson}, title = {Coalgebraic semantics of modal logics: An overview}, journal = {Theor. Comput. Sci.}, volume = {412}, nonumber = {38}, year = {2011}, pages = {5070-5094}, ee = {http://dx.doi.org/10.1016/j.tcs.2011.04.023}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/calco/DahlqvistP11, author = {Fredrik Dahlqvist and Dirk Pattinson}, title = {On the Fusion of Coalgebraic Logics}, booktitle = {CALCO}, editor = {Andrea Corradini and Bartek Klin and Corina C\^{\i}rstea}, booktitle = {Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6859}, year = {2011}, isbn = {978-3-642-22943-5}, ee = {http://dx.doi.org/10.1007/978-3-642-22944-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/tbillc/LitakPS11, author = {Tadeusz Litak and Dirk Pattinson and Katsuhiko Sano}, title = {Coalgebraic Predicate Logic: Equipollence Results and Proof Theory}, booktitle = {TbiLLC}, editor = {Guram Bezhanishvili and Sebastian L{\"o}bner and Vincenzo Marra and Frank Richter}, booktitle = {Logic, Language, and Computation - 9th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2011, Revised Selected Papers}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7758}, year = {2013}, isbn = {978-3-642-36975-9}, ee = {http://dx.doi.org/10.1007/978-3-642-36976-6}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/tacas/GoreKP10, author = {Rajeev Gor{\'e} and Clemens Kupke and Dirk Pattinson}, title = {Optimal Tableau Algorithms for Coalgebraic Logics}, booktitle = {TACAS}, editor = {Javier Esparza and Rupak Majumdar}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6015}, year = {2010}, isbn = {978-3-642-12001-5}, ee = {http://dx.doi.org/10.1007/978-3-642-12002-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/mscs/KurzP05, author = {Alexander Kurz and Dirk Pattinson}, title = {Coalgebraic modal logic of finite rank}, journal = {Mathematical Structures in Computer Science}, volume = {15}, number = {3}, year = {2005}, pages = {453-473}, ee = {http://dx.doi.org/10.1017/S0960129505004755}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{KupkeEA04, author = {Clemens Kupke and Alexander Kurz and Dirk Pattinson}, title = {Algebraic Semantics for Coalgebraic Logics}, booktitle = {Coalgebraic Methods in Computer Science, CMCS 2004}, series = {Electr. Notes Theor. Comput. Sci.}, volume = {106}, year = {2004}, pages = {219-241}, ee = {http://dx.doi.org/10.1016/j.entcs.2004.02.037}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/tcs/Pattinson03, author = {Dirk Pattinson}, title = {Coalgebraic modal logic: soundness, completeness and decidability of local consequence}, journal = {Theor. Comput. Sci.}, volume = {309}, nonumber = {1-3}, year = {2003}, pages = {177-193}, ee = {http://dx.doi.org/10.1016/S0304-3975(03)00201-9}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/corr/abs-1206-4935, author = {Clemens Kupke and Alexander Kurz and Yde Venema}, title = {Completeness for the coalgebraic cover modality}, journal = {Logical Methods in Computer Science}, volume = {8}, nonumber = {3}, year = {2012}, ee = {http://dx.doi.org/10.2168/LMCS-8(3:2)2012}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/calco/BergfeldV11, author = {Jort Bergfeld and Yde Venema}, title = {Model Constructions for Moss' Coalgebraic Logic}, booktitle = {CALCO}, editor = {Andrea Corradini and Bartek Klin and Corina C\^{\i}rstea}, booktitle = {Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6859}, year = {2011}, isbn = {978-3-642-22943-5}, ee = {http://dx.doi.org/10.1007/978-3-642-22944-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/logcom/KurzPV10, author = {Alexander Kurz and Alessandra Palmigiano and Yde Venema}, title = {Coalgebra and Logic: A Brief Overview}, journal = {J. Log. Comput.}, volume = {20}, nonumber = {5}, year = {2010}, pages = {985-990}, ee = {http://dx.doi.org/10.1093/logcom/exn094}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/aiml/KurzV10, author = {Alexander Kurz and Yde Venema}, title = {Coalgebraic Lindstr{\"o}om Theorems}, booktitle = {Advances in Modal Logic}, editor = {Lev D. Beklemishev and Valentin Goranko and Valentin Shehtman}, booktitle = {Advances in Modal Logic, AiML 2010}, booktitle = {Advances in Modal Logic}, publisher = {College Publications}, year = {2010}, isbn = {978-1-84890-013-4}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/ndjfl/Pattinson04, author = {Dirk Pattinson}, title = {Expressive Logics for Coalgebras via Terminal Sequence Induction}, journal = {Notre Dame Journal of Formal Logic}, volume = {45}, nonumber = {1}, year = {2004}, pages = {19-33}, ee = {http://projecteuclid.org/euclid.ndjfl/1094155277}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/icalp/FontaineLV10, author = {Ga{\"e}lle Fontaine and Raul Andres Leal and Yde Venema}, title = {Automata for Coalgebras: An Approach Using Predicate Liftings}, booktitle = {ICALP (2)}, editor = {Samson Abramsky and Cyril Gavoille and Claude Kirchner and Friedhelm {Meyer auf der Heide} and Paul G. Spirakis}, booktitle = {Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6199}, year = {2010}, isbn = {978-3-642-14161-4}, ee = {http://dx.doi.org/10.1007/978-3-642-14162-1}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/calco/KissigV09, author = {Christian Kissig and Yde Venema}, title = {Complementation of Coalgebra Automata}, booktitle = {CALCO}, editor = {Alexander Kurz and Marina Lenisa and Andrzej Tarlecki}, title = {Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5728}, year = {2009}, isbn = {978-3-642-03740-5}, ee = {http://dx.doi.org/10.1007/978-3-642-03741-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/lmcs/KupkeV08, author = {Clemens Kupke and Yde Venema}, title = {Coalgebraic Automata Theory: Basic Results}, journal = {Logical Methods in Computer Science}, volume = {4}, nonumber = {4}, year = {2008}, ee = {http://dx.doi.org/10.2168/LMCS-4(4:10)2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/corr/abs-1207-2732, author = {Alexander Kurz and Jir\'{\i} Rosick{\'y}}, title = {Strongly Complete Logics for Coalgebras}, journal = {Logical Methods in Computer Science}, volume = {8}, nonumber = {3}, year = {2012}, ee = {http://dx.doi.org/10.2168/LMCS-8(3:14)2012}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/tcs/KurzL12, author = {Alexander Kurz and Raul Andres Leal}, title = {Modalities in the Stone age: A comparison of coalgebraic logics}, journal = {Theor. Comput. Sci.}, volume = {430}, year = {2012}, pages = {88-116}, ee = {http://dx.doi.org/10.1016/j.tcs.2012.03.027}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/aiml/KapulkinKV12, author = {Krzysztof Kapulkin and Alexander Kurz and Jiri Velebil}, title = {Expressiveness of Positive Coalgebraic Logic}, booktitle = {Advances in Modal Logic}, editor = {Thomas Bolander and Torben Bra{\"u}ner and Silvio Ghilardi and Lawrence S. Moss}, booktitle = {Advances in Modal Logic, AiML 2012}, publisher = {College Publications}, year = {2012}, isbn = {978-1-84890-068-4}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/sigact/Kurz06, author = {Alexander Kurz}, title = {Coalgebras and their logics}, journal = {SIGACT News}, volume = {37}, nonumber = {2}, year = {2006}, pages = {57-77}, ee = {http://doi.acm.org/10.1145/1140612.1140628}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:journals/entcs/Klin07, author = {Bartek Klin}, title = {Coalgebraic Modal Logic Beyond Sets}, booktitle = {623rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII), Proceedings}, series = {Electr. Notes Theor. Comput. Sci.}, volume = {173}, year = {2007}, pages = {177-201}, ee = {http://dx.doi.org/10.1016/j.entcs.2007.02.034}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/lics/Klin07, author = {Bartek Klin}, title = {Bialgebraic Operational Semantics and Modal Logic}, booktitle = {LICS}, booktitle = {22nd IEEE Symposium on Logic in Computer Science, LICS 2007, Proceedings}, publisher = {IEEE Computer Society}, year = {2007}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/logcom/JacobsS10, author = {Bart Jacobs and Ana Sokolova}, title = {Exemplaric Expressivity of Modal Logics}, journal = {J. Log. Comput.}, volume = {20}, nonumber = {5}, year = {2010}, pages = {1041-1068}, ee = {http://dx.doi.org/10.1093/logcom/exn093}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{GorinSchroder13, author = {Daniel Gor{\'i}n and Lutz Schr{\"o}der}, title = {Simulations and Bisimulations For Coalgebraic Modal Logics}, booktitle = {Proc. 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013}, editor = {Reiko Heckel and Stefan Milius}, series = {Lect. Notes Comput. Sci.}, publisher = {Springer}, volume = {8089}, doi = {10.1007/978-3-642-40206-7_19}, year = {2013}, pages = {253-266}, url = {http://arxiv.org/pdf/1303.2467}, } @InProceedings{CarreiroEA13, author = {Facundo Carreiro and Daniel Gor{\'i}n and Lutz Schr{\"o}der}, title = {Coalgebraic Announcement Logics}, booktitle = {Proc. 40th International Colloquium on Automata, Languages and Programming, ICALP 2013}, series = {Lect. Notes Comput. Sci.}, publisher = {Springer}, pages = {101-112}, editor = {Fedor V. Fomin and Rusins Freivalds and Marta Z. Kwiatkowska and David Peleg}, volume = {7966}, year = {2013}, url = {http://www8.cs.fau.de/_media/research:papers:icalp13.pdf}, doi = {10.1007/978-3-642-39212-2_12}, } @InProceedings{KulackaEA13, author = {Agnieszka Kulacka and Dirk Pattinson and Lutz Schr{\"o}der}, title = {Syntactic Labelled Tableaux for Lukasiewicz Fuzzy {ALC}}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proc. 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013}, OPTpages = {}, year = {2013}, editor = {Francesca Rossi}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {IJCAI/AAAI}, OPTannote = {}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/_media/research:papers:lukasiewicz-tableau.pdf"> [updated version]</a>}, url = {http://ijcai.org/papers13/Papers/IJCAI13-147.pdf}, } @inproceedings{GorinSchroder12, author = {Daniel Gor\'{\i}n and Lutz Schr{\"o}der}, title = {Narcissists Are Easy, Stepmothers Are Hard}, pages = {240-254}, ee = {http://dx.doi.org/10.1007/978-3-642-28729-9_16}, doi = {10.1007/978-3-642-28729-9_16}, editor = {Lars Birkedal}, booktitle = {Proc. 15th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2012}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7213}, year = {2012}, isbn = {978-3-642-28728-2}, bibsource = {DBLP, http://dblp.uni-trier.de}, url = {http://www8.cs.fau.de/_media/research:papers:fossacs12.pdf}, } @InProceedings{GorinSchroder14, author = {Daniel Gor{\'\i}n and Lutz Schr{\"o}der}, title = {Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics}, booktitle = {Proc. Advances in Modal Logic, AiML 2014}, year = {2014}, editor = {Agi Kurucz and Rajeev Gor{\'e}}, series = {LNCS}, publisher = {Springer}, note = {To appear}, } @Article{CirsteaEA09, author = {Corina Cirstea and Alexander Kurz and Dirk Pattinson and Lutz Schr{\"o}der and Yde Venema}, title = {Modal logics are coalgebraic}, year = {2011}, journal = {The Computer Journal}, volume = {54}, pages = {31-41}, number = {1}, keywords = {Modal logic coalgebra knowledge representation automata modularity pi-calculus}, doi = {"> [preprint] </a>http://comjnl.oxfordjournals.org/cgi/content/abstract/bxp004}, url = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/ModalCoalgRev.pdf}, abstract = {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. }} @InProceedings{GoreEA10, author = {Rajeev Gore and Clemens Kupke and Dirk Pattinson and Lutz Schr{\"o}der}, title = {Global Caching for Coalgebraic Description Logics}, year = {2010}, editor = {J{\"u}rgen Giesl and Reiner Haehnle}, booktitle = {International Joint Conference on Automated Reasoning, IJCAR 2010}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6173}, pages = {46-60}, keywords = {Coalgebra description logic modal logic hybrid logic tableaux global caching}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/hyGlobalCaching.pdf"> [preprint] </a>}, abstract = { Coalgebraic description logics offer a common semantic umbrella for extensions of description logics with reasoning principles outside relational semantics, e.g. quantitative uncertainty, non-monotonic conditionals, or coalitional power. Specifically, we work in coalgebraic logic with global assumptions (i.e. a general TBox), nominals, and satisfaction operators, and prove soundness and completeness of an associated tableau algorithm of optimal complexity ExpTime. The algorithm uses the (known) tableau rules for the underlying modal logics, and is based on on global caching, which raises hopes of practically feasible implementation. Instantiation of this result to concrete logics yields new algorithms in all cases including standard relational hybrid logic.}, } @InProceedings{MyersEA09, author = {Rob Myers and Dirk Pattinson and Lutz Schr{\"o}der}, title = {Coalgebraic Hybrid Logic}, year = {2009}, editor = {Luca de Alfaro}, booktitle = {Foundations of Software Science and Computation Structures (FOSSACS 2009)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5504}, pages = {137-151}, keywords = {coalgebra hybrid logic decision procedures polynomial space hilbert gentzen sequent tableaux}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/chl.pdf"> [preprint] </a>}, abstract = { We introduce a generic framework for hybrid logics, i.e. modal logics additionally featuring nominals and satisfaction operators, thus providing the necessary facilities for reasoning about individual states in a model. This framework, coalgebraic hybrid logic, works at the same level of generality as coalgebraic modal logic, and in particular subsumes, besides normal hybrid logics such as hybrid K, a wide variety of logics with non-normal modal operators such as probabilistic, graded, or coalitional modalities and non-monotonic conditionals. We prove a generic finite model property and an ensuing weak completeness result, and we give a semantic criterion for decidability in PSPACE. Moreover, we present a fully internalised PSPACE tableau calculus. These generic results are easily instantiated to particular hybrid logics and thus yield a wide range of new results, including e.g. decidability in PSPACE of probabilistic and graded hybrid logics.}, } @InProceedings{PattinsonSchroder08, author = {Dirk Pattinson and Lutz Schr{\"o}der}, title = {Beyond Rank 1: Algebraic Semantics and Finite Models for Coalgebraic Logics}, year = {2008}, editor = {Roberto Amadio}, booktitle = {Foundations of Software Science and Computation Structures (FOSSACS 2008)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4962}, pages = {66-80}, keywords = {Coalgebra modal logic frame conditions algebraic semantics quantitative uncertainty coalition logic}, url = {http://dx.doi.org/10.1007/978-3-540-78499-9_6}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/fmp-fap.pdf"> [preprint] </a>}, abstract = { Coalgebras provide a uniform framework for the semantics of a large class of (mostly non-normal) modal logics, including e.g. monotone modal logic, probabilistic and graded modal logic, and coalition logic, as well as the usual Kripke semantics of modal logic. In earlier work, the finite model property for coalgebraic logics has been established w.r.t. the class of emph{all} structures appropriate for a given logic at hand; the corresponding modal logics are characterised by being axiomatised in rank 1, i.e. without nested modalities. Here, we extend the range of coalgebraic techniques to cover logics that impose global properties on their models, formulated as frame conditions with possibly nested modalities on the logical side (in generalisation of frame conditions such as symmetry or transitivity in the context of Kripke frames). We show that the finite model property for such logics follows from the finite algebra property of the associated class of complex algebras, and then investigate sufficient conditions for the finite algebra property to hold. Example applications include extensions of coalition logic and logics of uncertainty and knowledge. }, } @Article{PattinsonSchroder10, author = {Dirk Pattinson and Lutz Schr{\"o}der}, title = {Cut Elimination in Coalgebraic Logics}, year = {2010}, journal = {Information and Computation}, volume = {208}, pages = {1447-1468}, keywords = {Coalgebra modal logic cut elimination interpolation coalition logic conditiona logic}, url = {http://dx.doi.org/10.1016/j.ic.2009.11.008}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/cut-ext.pdf"> [preprint] </a>}, abstract = {We give two generic proofs for cut elimination in propositional modal logics, interpreted over coalgebras. We first investigate semantic coherence conditions between the axiomatisation of a particular logic and its coalgebraic semantics that guarantee that the cut-rule is admissible in the ensuing sequent calculus. We then independently isolate a purely syntactic property of the set of modal rules that guarantees cut elimination. Apart from the fact that cut elimination holds, our main result is that the syntactic and semantic assumptions are equivalent in case the logic is amenable to coalgebraic semantics. As applications we present a new proof of the (already known) interpolation property for coalition logic and newly establish the interpolation property for the conditional logics CK and CK+ID.}, } @Article{Schroder06Expr-TCS, author = {Lutz Schr{\"o}der}, title = {Expressivity of Coalgebraic Modal Logic: The Limits and Beyond}, year = {2008}, journal = {Theoretical Computer Science}, volume = {390}, pages = {230-247}, keywords = {coalgebra expressivity modal logic predicate lifting natural relation}, url = {http://dx.doi.org/10.1016/j.tcs.2007.09.023}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/coalgml-ext.pdf"> [preprint] </a>}, abstract = {Modal logic has a good claim to being the logic of choice for describing the reactive behaviour of systems modeled as coalgebras. Logics with modal operators obtained from so-called predicate liftings have been shown to be invariant under behavioral equivalence. Expressivity results stating that, conversely, logically indistinguishable states are behaviorally equivalent depend on the existence of separating sets of predicate liftings for the signature functor at hand. Here, we provide a classification result for predicate liftings which leads to an easy criterion for the existence of such separating sets, and we give simple examples of functors that fail to admit expressive normal or monotone modal logics, respectively, or in fact an expressive (unary) modal logic at all. We then move on to polyadic modal logic, where modal operators may take more than one argument formula. We show that every accessible functor admits an expressive polyadic modal logic. Moreover, expressive polyadic modal logics are, unlike unary modal logics, compositional. }} @Article{Schroder07, author = {Lutz Schr{\"o}der}, title = {A finite model construction for coalgebraic modal logic}, year = {2007}, journal = {Journal of Logic and Algebraic Programming (FOSSACS 06 special issue)}, volume = {73}, pages = {97-110}, keywords = {Coalgebra Modal Logic Decision Procedures Complexity Filtrations}, url = {http://dx.doi.org/10.1016/j.jlap.2006.11.004}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/CMLfmp-ext.pdf"> [preprint] </a>}, abstract = {In recent years, a tight connection has emerged between modal logic on the one hand and coalgebras, understood as generic transition systems, on the other hand. Here, we prove that (finitary) coalgebraic modal logic has the finite model property. This fact not only reproves known completeness results for coalgebraic modal logic, which we push further by establishing that every coalgebraic modal logic admits a complete axiomatisation in rank 1; it also enables us to establish a generic decidability result and a first complexity bound. Examples covered by these general results include, besides standard Hennessy-Milner logic, graded modal logic and probabilistic modal logic. } } @InProceedings{SchroderEA09, author = {Lutz Schr{\"o}der and Dirk Pattinson and Clemens Kupke}, title = {Nominals for Everyone}, year = {2009}, editor = {Craig Boutilier}, booktitle = {International Joint Conferences on Artificial Intelligence (IJCAI 2009)}, publisher = {AAAI Press; Menlo Park, CA}, pages = {917-922}, keywords = {Description logic coalgebra hybrid logic modal logic nominals uncertainty Tudor dynasty}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/Nominals.pdf"> [preprint] </a>}, abstract = { It has been recognised that the expressivity of ontology languages benefits from the introduction of non-standard modal operators beyond the usual existential restrictions and the number restrictions already featured by many description logics. Such operators serve to support notions such as uncertainty, defaults, agency, obligation, or evidence, which are hard to capture using only the standard operators, and whose semantics often goes beyond relational structures. We work in a unified theory for logics that combine non-standard modal operators and nominals, a feature of established description logics that provides the necessary means for reasoning about individuals; in particular, the logics of this framework allow for internalisation of ABoxes. We reenforce the general framework by proving decidability in EXPTIME of concept satisfiability over general TBoxes; moreover, we discuss example instantiations in various probabilistic logics with nominals. }, } @Article{SchroderPattinson08, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {PSPACE Bounds for Rank-1 Modal Logics}, year = {2009}, journal = {ACM Transactions on Computational Logic}, volume = {10}, pages = {1-33}, number = {2:13}, keywords = {Modal logic coalgebra non-iterative majority probabilistic graded coalition PSPACE}, url = {http://arxiv.org/abs/0706.4044}, comment = { <a href = "http://tocl.acm.org/accepted/352schroeder.pdf"> [preprint] </a>}, abstract = {For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a number of logics including K, KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.}, } @Article{SchroderPattinson08b, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {Rank-1 modal logics are coalgebraic }, year = {2010}, journal = {Journal of Logic and Computation}, volume = {20}, pages = {1113-1147}, number = {5}, keywords = {Modal logic coalgebra neighbourhood frames deontic logic decision procedures}, url = {http://logcom.oxfordjournals.org/content/20/5/1113.abstract}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/rank1coalg-ext.pdf"> [preprint] </a>}, abstract = {Coalgebras provide a unifying semantic framework for a wide variety of modal logics. It has previously been shown that the class of coalgebras for an endofunctor can always be axiomatised in rank 1. Here we establish the converse, i.e. every rank 1 modal logic has a sound and strongly complete coalgebraic semantics. This is achieved by constructing for a given modal logic a canonical coalgebraic semantics, consisting of a signature functor and interpretations of modal operators, which turns out to be final among all such structures. The canonical semantics may be seen as a coalgebraic reconstruction of neighbourhood semantics, broadly construed. A finitary restriction of the canonical semantics yields a canonical weakly complete semantics which moreover enjoys the Hennessy-Milner property. As a consequence, the machinery of coalgebraic modal logic, in particular generic decision procedures and upper complexity bounds, becomes applicable to arbitrary rank 1 modal logics, without regard to their semantic status; we thus obtain purely syntactic versions of such results. As an extended example, we apply our framework to recently defined deontic logics. In particular, our methods lead to the new result that these logics are strongly complete. }} @InProceedings{SchroderPattinson08c, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {How Many Toes Do I Have? Parthood and Number Restrictions in Description Logics}, year = {2008}, editor = {Gerhard Brewka and Jer{\^o}me Lang}, booktitle = {Principles of Knowledge Representation and Reasoning (KR 2008)}, publisher = {AAAI Press; Menlo Park, CA}, pages = {307-218}, keywords = {Coalgebra modal logic description logic number restriction parthood trees}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/TreeDL.pdf"> [preprint] </a>}, abstract = {The modelling of parthood relations in description logics via transitive roles often leads to undecidability when combined with number restrictions and role hierarchies. Here, we introduce the description logic PHQ that explicitly supports reasoning about parthood in the presence of qualified number restrictions. Our main results are completeness and decidability in NEXPTIME. Conceptually, we argue that PHQ provides a better semantic fit for many applications: more often than not, parthoods occurring e.g. in biomedical ontologies are expected to be tree-like. In such cases, PHQ supports stronger inferences than standard description logics. Technically this is achieved by explicitly excluding the merging of descendants, which, at the same time, eliminates the prime source of undecidability. We work in the general setting of coalgebraic modal logic, a generic semantic framework for not-necessarily-normal modal logics. This added generality allows the re-use of many of our results for other logics of sometimes quite different flavour. }, } @InProceedings{SchroderPattinson09, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {Strong completeness of coalgebraic modal logics}, year = {2009}, editor = {Susanne Albers and Jean-Yves Marion}, booktitle = {26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009)}, publisher = {Schloss Dagstuhl - Leibniz-Center of Informatics; Dagstuhl, Germany}, series = {Leibniz International Proceedings in Informatics}, pages = {673--684}, url = {http://drops.dagstuhl.de/opus/volltexte/2009/1855}, abstract = {Canonical models are of central importance in modal logic, in particular as they witness strong completeness and hence compactness. While the canonical model construction is well understood for Kripke semantics, non-normal modal logics often present subtle difficulties - up to the point that canonical models may fail to exist, as is the case e.g. in most probabilistic logics. Here, we present a generic canonical model construction in the semantic framework of coalgebraic modal logic, which pinpoints coherence conditions between syntax and semantics of modal logics that guarantee strong completeness. We apply this method to reconstruct canonical model theorems that are either known or folklore, and moreover instantiate our method to obtain new strong completeness results. In particular, we prove strong completeness of graded modal logic with finite multiplicities, and of the modal logic of exact probabilities.}, } @InProceedings{SchroderPattinson10, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {Named Models in Coalgebraic Hybrid Logic}, year = {2010}, editor = {Jean-Yves Marion and Thomas Schwentick}, booktitle = {27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010}, publisher = {Schloss Dagstuhl - Leibniz-Center of Informatics; Dagstuhl, Germany}, series = {Leibniz International Proceedings in Informatics}, volume = {5}, pages = {645--656}, keywords = {coalgebra modal logic named models pure completeness local binding}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/namedModels.pdf"> [preprint] </a>}, abstract = { Hybrid logic extends modal logic with support for reasoning about individual states, designated by so-called nominals. We study hybrid logic in the broad context of coalgebraic semantics, where Kripke frames are replaced with coalgebras for a given functor, thus covering a wide range of reasoning principles including, e.g., probabilistic, graded, default, or coalitional operators. Specifically, we establish generic criteria for a given coalgebraic hybrid logic to admit named canonical models, with ensuing completeness proofs for pure extensions on the one hand, and for an extended hybrid language with local binding on the other. We instantiate our framework with a number of examples. Notably, we prove completeness of graded hybrid logic with local binding. }, } @InProceedings{SchroderPattinson10b, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {Coalgebraic correspondence theory}, year = {2010}, editor = {Luke Ong}, booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS 2010)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6014}, pages = {328--342}, keywords = {coalgebra modal logic correspondence theory rosen van benthem theorem first order logic}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/correspondence.pdf"> [preprint] </a>}, abstract = { We lay the foundations of a first-order correspondence theory for coalgebraic logics that makes the transition structure explicit in the first-order modelling. In particular, we prove a coalgebraic version of the van Benthem/Rosen theorem stating that both over arbitrary structures and over finite structures, coalgebraic modal logic is precisely the bisimulation invariant fragment of first-order logic. }, } @Article{SchroderPattinson10c, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {Modular Algorithms for Heterogeneous Modal Logics via Multi-Sorted Coalgebra}, year = {2011}, journal = {Math. Struct. Comput. Sci.}, volume = {21}, pages = {235-266}, number = {2}, keywords = {multisorted coalgebra modal logic complexity pspace shallow models features}, url = {http://journals.cambridge.org/action/displayAbstract?aid=8238956}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/ModAlg-Ext.pdf"> [preprint] </a>}, abstract = {State-based systems and modal logics for reasoning about them often heterogeneously combine a number of features such as non-determinism and probabilities. Here, we show that the combination of features can be reflected algorithmically and develop modular decision procedures for heterogeneous modal logics. The modularity is achieved by formalizing the underlying state-based systems as multi-sorted coalgebras and associating both a logical and an algorithmic description to a number of basic building blocks. Our main result is that logics arising as combinations of these building blocks can be decided in polynomial space provided that this is the case for the components. By instantiating the general framework to concrete cases, we obtain PSPACE decision procedures for a wide variety of structurally different logics, describing e.g. Segala systems and games with uncertain information.}, note = {Copyright Cambridge University Press}, } @InProceedings{SchroderPattinson11, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {Description Logics and Fuzzy Probability}, year = {2011}, editor = {Toby Walsh}, booktitle = {International Joint Conference on Artificial Intelligence, IJCAI 2011}, publisher = {AAAI Press; Menlo Park, CA}, keywords = {fuzzy logic coalgebra probability expectation lukasiewicz semantics complexity}, comment = { <a href = "http://informatik.uni-bremen.de/~lschrode/papers/FuzzyCDL.pdf"> [preprint] </a>}, pages = {1075-1081}, url = {http://ijcai.org/papers11/Papers/IJCAI11-184.pdf}, abstract = {Uncertainty and vagueness are pervasive phenomena in real-life knowledge. They are supported in extended description logics that adapt classical description logics to deal with numerical probabilities or fuzzy truth values. While the two concepts are distinguished for good reasons, they combine in the notion of probably, which is ultimately a fuzzy qualification of probabilities. Here, we develop existing propositional logics of fuzzy probability into a full-blown description logic, and we show decidability of several variants of this logic under Lukasiewicz semantics. We obtain these results in a novel generic framework f fuzzy coalgebraic logic; this enables us to extend our results to logics that combine crisp ingredients including standard crisp roles and crisp numerical probabilities with fuzzy roles and fuzzy probabilities.}, note = {Oral and poster presentation}, } @InProceedings{SchroderPattison08d, author = {Lutz Schr{\"o}der and Dirk Pattinson}, title = {Shallow models for non-iterative modal logics}, year = {2008}, editor = {Andreas Dengel and Karsten Berns and Thomas Breuel and Frank Bomarius and Thomas Roth-Berghofer}, booktitle = {Advances in Artificial Intelligence (KI 2008)}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, volume = {5243}, pages = {324-331}, keywords = {Modal logic coalgebra agent shallow model PSPACE decision procedures}, url = {http://dx.doi.org/10.1007/978-3-540-85845-4_40}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/nonitPSP.pdf"> [preprint] </a>}, abstract = {Modal logics see a wide variety of applications in artificial intelligence, e.g. in reasoning about knowledge, belief, uncertainty, agency, defaults, and relevance. From the perspective of applications, the attractivity of modal logics stems from a combination of expressive power and comparatively low computational complexity. Compared to the classical treatment of modal logics with relational semantics, the use of modal logics in AI has two characteristic traits: Firstly, a large and growing variety of logics is used, adapted to the concrete situation at hand, and secondly, these logics are often non-normal. Here, we present a shallow model construction that witnesses PSPACE bounds for a broad class of mostly non-normal modal logics. Our approach is uniform and generic: we present general criteria that uniformly apply to and are easily checked in large numbers of examples. Thus, we not only re-prove known complexity bounds for a wide variety of structurally different logics and obtain previously unknown PSPACE-bounds, e.g. for Elgesem's logic of agency, but also lay the foundations upon which the complexity of newly emerging logics can be determined. }, note = {<a href="http://arxiv.org/abs/0802.0116">Full version</a> available as e-print arXiv:0802.0116}, } @InProceedings{SchroderVenema10, author = {Lutz Schr{\"o}der and Yde Venema}, title = {Flat coalgebraic fixed point logics}, year = {2010}, editor = {Paul Gastin and Fran\c{c}ois Laroussinie}, booktitle = {21st International Conference on Concurrency Theory, CONCUR 2010}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6269}, pages = {524-538}, keywords = {Coalgebra modal logic fixpoints fixed points mu-calculus flat single-variable alternating time graded ATL AMC}, comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/flatfix.pdf"> [preprint] </a>}, abstract = {Fixed point logics are widely used in computer science, in particular in artificial intelligence and concurrency. The most expressive logics of this type are the mu-calculus and its relatives. However, popular fixed point logics tend to trade expressivity for simplicity and readability, and in fact often live within the single variable fragment of the mu-calculus. The family of such flat fixed point logics includes, e.g., CTL, the *-nesting-free fragment of PDL, and the logic of common knowledge. Here, we extend this notion to the generic semantic framework of coalgebraic logic, thus covering a wide range of logics beyond the standard mu-calculus including, e.g., flat fragments of the graded mu-calculus and the alternating-time mu-calculus (such as ATL), as well as probabilistic and monotone fixed point logics. Our main results are completeness of the Kozen-Park axiomatization and a timed-out tableaux method that matches ExpTime upper bounds inherited from the coalgebraic mu-calculus but avoids using automata. }, }