Coalgebraic Logic: Expanding the Scope

Lead Research Organisation: University of Leicester
Department Name: Computer Science


COALGEBRAIC LOGICLogic plays a fundamental role in Computer Science. At the most basiclevel, Boolean logic is used to design the circuits we use every day inour computers. At the higher end, the tasks that computers perform need toconform to specifications expressed in logics suitable for programmers,analysts or even other computational devices.Such specification logics have to be able to express many differentconcepts such as time, knowledge, space, mobility, communication,probability, conditionals etc. Bespoke logics for each of these conceptsexist and are studied under the umbrella of Modal Logic.In any substantial application of Modal Logic to the specification ofa system, the need to combine different logics will arise, each logicaccounting for, eg, one of the aspects mentioned above. The need thenarises to deal with these logics in a uniform and modular way.Not all of these logics have a standard Kripke semantics, but in allcases, the semantics can be considered to be coalgebraic. Coalgebrasgeneralise the standard Kripke semantics of modal logic to encompassnotions such as neighbourhood frames, Markov chains, topologicalspaces, etc.Moreover, Coalgebra is a concept from Category Theory. Category Theoryis an area of mathematics which describes mathematical constructionsin abstract terms that make these constructions available to manydifferent areas of mathematics, logic, and computer science. Inparticular, the category theoretic nature of Coalgebras allows us totackle the modularity problem using category theoreticconstructions. One of the benefits of category theory is that theseconstructions, because of their generality, apply to specificationlanguages and to their semantic models.To summarise, Coalgebraic Logic combines Modal Logic withCoalgebra. This generalises modal logics from Kripke frames tocoalgebras and makes category theoretic methods and constructionsavailable in Modal Logic.EXPANDING THE SCOPECoalgebraic Logic can be traced back to 1997 when the first draft ofMoss's paper with the same title was circulated. Since then, it hasbeen developed by a number of researchers. Just now, Coalgebraic Logicis about to establish itself as an own area. Whereas much of thecurrent work in Coalgebraic Logic aims at exploiting the currentachievements towards more applications, this project starts from thefollowing two observations:First, Coalgebraic logic did not yet make use of many of the importantdevelopments that have taken place in Modal Logic. Two of thesedevelopments are:1) the relationship between Modal Logic and First-Order Logic and2) the uniform treatment of classes of modal logics.Second, there exist many parallel developments in Modal Logic andDomain Theory. Some of the relationships have only recently becomeclear, through the connection of both areas with Coalgebra. Wetherefore plan to3) generalise methods from Modal Logic so that they can be applied tothe logics arising in Domain Theory (this will include the work doneunder 1 and 2 above)


10 25 50
publication icon
A Kurz And Y Venema (2010) Advances in Modal Logic 8

publication icon
Balan A (2010) On Coalgebras over Algebras in Electronic Notes in Theoretical Computer Science

publication icon
Balan A (2011) On coalgebras over algebras in Theoretical Computer Science

publication icon
BEZHANISHVILI G (2010) Bitopological duality for distributive lattices and Heyting algebras in Mathematical Structures in Computer Science

publication icon
Bilkova M (2013) Relation lifting, with an application to the many-valued cover modality in Logical Methods in Computer Science

publication icon
Chen L (2014) On a Categorical Framework for Coalgebraic Modal Logic in Electronic Notes in Theoretical Computer Science

publication icon
Ciancia V (2010) Families of Symmetries as Efficient Models of Resource Binding in Electronic Notes in Theoretical Computer Science

Description The aim of the project was to expand the scope of coalgebraic logic. The RA on the grant, Dr Litak, extended the scope by introducing nominal boolean algebras and by introducing the current formalism for coalgebraic predicate and second order logic. The PI pursued coalgebraic logic over enriched categories in general and over posets and preorders in particular. The key finding of the grant is that the strengths of the coalgebraic approach carry over to all of these new settings and extensions.
Exploitation Route This grant is in the mathematical foundations of computer science. So in the short-term our findings will be of interest only to a specialist community of researchers in theoretical computer science. But in the long-term, just because the research is foundational, it will, more indirectly and together with other areas of theoretical computer science, impact all areas using computing devices. As the form below does not seem to be crafted with foundational research in mind, I interpret "potentially of interest" in the long-term sense and tick all boxes.
Sectors Aerospace, Defence and Marine,Agriculture, Food and Drink,Chemicals,Communities and Social Services/Policy,Construction,Creative Economy,Digital/Communication/Information Technologies (including Software),Education,Electronics,Energy,Environment,Financial Services, and Management Consultancy,Healthcare,Leisure Activities, including Sports, Recreation and Tourism,Government, Democracy and Justice,Manufacturing, including Industrial Biotechology,Culture, Heritage, Museums and Collections,Pharmace

Description The grant is in the mathematical foundations of computer science and my findings have been used exclusively in academia. The work had immediate impact on the PhD thesis of Wilkinson (Southampton, 2013) who is taking some of our results further. Impact on the wider society will be indirect and may take a couple of decades.
First Year Of Impact 2012
Impact Types Cultural

Description Duality of relations 
Organisation Chapman University
Country United States 
Sector Academic/University 
PI Contribution I provided research time and expertise in coalgebra and category theory.
Collaborator Contribution Prof Moshier contributed time and expertise on the topics of Stone Duality, Domain Theory, and Relational Morphisms. Chapman University provided support for accommodation and travel.
Impact This is a long project which has produced several hundred pages of drafts, but publications are to be submitted only in 2018, due to the complexity of the research.
Start Year 2012
Description Quantitative Coalgebraic Logic 
Organisation Czech Technical University in Prague
Country Czech Republic 
Sector Academic/University 
PI Contribution Together with Jiri Velebil from the Faculty of Electrical Engineering, Czech Technical University in Prague, Prague, Czech Republic, we are exploring coalgebraic methods for quantitative logics. In particular we are recreating the mathematical foundations of coalgebra in the setting of quantale enriched category theory. Our contributions are mainly in our expertise in coalgebra.
Collaborator Contribution Jiri Velebils contributions are mainly in his expertise in enriched category theory.
Impact Alexander Kurz, Jiri Velebil: Relation lifting, a survey. J. Log. Algebr. Meth. Program. 85(4): 475-499 (2016) Adriana Balan, Alexander Kurz, Jiri Velebil: Positive fragments of coalgebraic logics. Logical Methods in Computer Science 11(3) (2015) Adriana Balan, Alexander Kurz, Jiri Velebil: Extensions of Functors From Set to V-cat. CALCO 2015: 17-34, 2013 Alexander Kurz, Jiri Velebil: Enriched Logical Connections. Applied Categorical Structures 21(4): 349-377 (2013) Marta Bílková, Alexander Kurz, Daniela Petrisan, Jiri Velebil: Relation lifting, with an application to the many-valued cover modality. Logical Methods in Computer Science 9(4) (2013) Adriana Balan, Alexander Kurz, Jiri Velebil: Positive Fragments of Coalgebraic Logics. CALCO 2013: 51-65, 2012 Krzysztof Kapulkin, Alexander Kurz, Jiri Velebil: Expressiveness of Positive Coalgebraic Logic. Advances in Modal Logic 2012: 368-385 Marta Bílková, Alexander Kurz, Daniela Petrisan, Jiri Velebil: Relation Liftings on Preorders and Posets. CoRR abs/1210.1433 (2012), 2011 Jiri Velebil, Alexander Kurz: Equational presentations of functors and monads. Mathematical Structures in Computer Science 21(2): 363-381 (2011) Marta Bílková, Alexander Kurz, Daniela Petrisan, Jiri Velebil: Relation Liftings on Preorders and Posets. CALCO 2011: 115-129
Start Year 2010