A Finite Model Construction for Coalgebraic Modal Logic (bibtex)

by Lutz Schröder

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 axiomatization of 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.

View PDF

Reference:

Lutz Schröder: A Finite Model Construction for Coalgebraic Modal Logic, In Luca Aceto, Anna Ingólfsdóttir, eds.: Foundations Of Software Science And Computation Structures, Lecture Notes in Computer Science, vol. 3921, pp. 157–171, Springer; Berlin; http://www.springer.de, 2006. EATCS Best Paper Award at ETAPS 2006 [preprint]

Bibtex Entry:

@InProceedings{Schroder06,
  author = {Lutz Schr{\"o}der},
  title = {A Finite Model Construction for Coalgebraic Modal Logic},
  year = {2006},
  editor = {Luca Aceto and Anna Ing{\'o}lfsd{\'o}ttir},
  booktitle = {Foundations Of Software Science And Computation Structures},
  publisher = {Springer; Berlin; http://www.springer.de},
  series = {Lecture Notes in Computer Science},
  volume = {3921},
  pages = {157-171},
  keywords = {Coalgebra modal logic finite model decision procedure probabilistic modal logic},
  url = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11690634_11},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/CMLfmp.pdf"> [preprint] </a>},
  psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/CMLfmp.ps},
  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
axiomatization of 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.
},
  note = {EATCS Best Paper Award at ETAPS 2006},
}