Symbolic model checking of tense logics on rational Kripke models

TL;DR

This paper introduces rational Kripke models based on rational graphs and demonstrates that model checking for the tense logic Kt and its extensions is decidable and effectively computable within these models.

Contribution

It defines rational Kripke models using rational graphs and automata, and proves decidability and computability of model checking for Kt and some extensions.

Findings

Model checking of Kt is decidable in rational Kripke models.

Every Kt formula has an effectively computable regular extension.

Complexity of the model checking procedures is analyzed.

Abstract

We introduce the class of rational Kripke models and study symbolic model checking of the basic tense logic Kt and some extensions of it in models from that class. Rational Kripke models are based on (generally infinite) rational graphs, with vertices labeled by the words in some regular language and transitions recognized by asynchronous two-head finite automata, also known as rational transducers. Every atomic proposition in a rational Kripke model is evaluated in a regular set of states. We show that every formula of Kt has an effectively computable regular extension in every rational Kripke model, and therefore local model checking and global model checking of Kt in rational Kripke models are decidable. These results are lifted to a number of extensions of Kt. We study and partly determine the complexity of the model checking procedures.