Modal logics on rational Kripke structures

Abstract

This dissertation is a contribution to the study of infinite graphs which can be presented in a finitary way. In particular, the class of rational graphs is studied. The vertices of a rational graph are labeled by a regular language in some finite alphabet and the set of edges of a rational graph is a rational relation on that language. While the first-order logics of these graphs are generally not decidable, the basic modal and tense logics are. A survey on the class of rational graphs is done, whereafter rational Kripke models are studied. These models have rational graphs as underlying frames and are equipped with rational valuations. A rational valuation assigns a regular language to each propositional variable. I investigate modal languages with decidable model checking on rational Kripke models. This leads me to consider regularity preserving relations to see if the class can be generalised even further. Then the concept of a graph being rationally presentable is examined - this is analogous to a graph being automatically presentable. Furthermore, some model theoretic properties of rational Kripke models are examined. In particular, bisimulation equivalences between rational Kripke models are studied. I study three subclasses of rational Kripke models. I give a summary of the results that have been obtained for these classes, look at examples (and non-examples in the case of automatic Kripke frames) and of particular interest is finding extensions of the basic tense logic with decidable model checking on these subclasses. An extension of rational Kripke models is considered next: omega-rational Kripke models. Some of their properties are examined, and again I am particularly interested in finding modal languages with decidable model checking on these classes. Finally I discuss some applications, for example bounded model checking on rational Kripke models, and mention possible directions for further research.