I will offer three ways of analyzing the expressive power of modal
an temporal languages, all three use bisimulations as an essential tool.
- invariance/preservation: characterize the fragment of classical
first- or higher-order logic to which a modal language corresponds
- safety: which (first-order) definable operations on relations
respect bisimilarity?
- definability: which properties can be expressed using a modal or
temporal language?
These three approaches will first be discussed for a simple modal language;
after that I will briefly indicate how the approaches can or cannot be
extended to other modal languages.
I will conclude with some pointers to ongoing work and open problems.