@ARTICLE{arec:coin10,
author = {Areces, C. and Gor\'{\i}n, D.},
title = {Coinductive models and normal forms for modal logics (or how we learned
to stop worrying and love coinduction)},
journal = {Journal of Applied Logic},
year = {2010},
volume = {8},
pages = {305--318},
number = {4},
abstract = {We present a coinductive definition of models for modal logics and
show that it provides a homogeneous framework in which it is possible
to include different modal languages ranging from classical modalities
to operators from hybrid and memory logics. Moreover, results that
had to be proved separately for each different language --but whose
proofs were known to be mere routine-- now can be proved in a general
way. We show, for example, that we can have a unique definition of
bisimulation for all these languages, and prove a single invariance-under-bisimulation
theorem. We then use the new framework to investigate normal forms
for modal logics. The normal form we introduce may have a smaller
modal depth than the original formula, and it is inspired by global
modalities like the universal modality and the satisfiability operator
from hybrid logics. These modalities can be extracted from under
the scope of other operators. We provide a general definition of
extractable modalities and show how to compute extracted normal forms.
As it is the case with other classical normal forms --e.g., the conjunctive
normal form of propositional logic-- the extracted normal form of
a formula can be exponentially bigger than the original formula,
if we require the two formulas to be equivalent. If we only require
equi-satisfiability, then every modal formula has an extracted normal
form which is only polynomially bigger than the original formula,
and it can be computed in polynomial time.},
keywords = {Modal logics; Hybrid logics; Normal forms; Modal depth},
publisher = {Elsevier}
}