TY - GEN
T1 - Symbolic model checking of tense logics on rational Kripke models
AU - Bekker, Wilmari
AU - Goranko, Valentin
PY - 2009
Y1 - 2009
N2 - We introduce the class of rational Kripke models and study symbolic model checking of the basic tense logic K t and some extensions of it on 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 rational set of states. We show that every formula of K t has an effectively computable rational extension in every rational Kripke model, and therefore local model checking and global model checking of K t in rational Kripke models are decidable. These results are lifted to a number of extensions of K t. We study and partly determine the complexity of the model checking procedures.
AB - We introduce the class of rational Kripke models and study symbolic model checking of the basic tense logic K t and some extensions of it on 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 rational set of states. We show that every formula of K t has an effectively computable rational extension in every rational Kripke model, and therefore local model checking and global model checking of K t in rational Kripke models are decidable. These results are lifted to a number of extensions of K t. We study and partly determine the complexity of the model checking procedures.
UR - https://www.scopus.com/pages/publications/71549122876
U2 - 10.1007/978-3-642-03092-5_2
DO - 10.1007/978-3-642-03092-5_2
M3 - Conference contribution
AN - SCOPUS:71549122876
SN - 3642030912
SN - 9783642030918
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 2
EP - 20
BT - Infinity in Logic and Computation - International Conference, ILC 2007, Revised Selected Papers
T2 - International Conference on Infinity in Logic and Computation, ILC 2007
Y2 - 3 November 2007 through 5 November 2007
ER -