@article(AAOW15,
 author       = {S. Akshay and T. Antonopoulos and J. Ouaknine and J. Worrell},
 year         = {2015},
 title        = {Reachability problems for {Markov} chains},
 journal      = {Information Processing Letters},
 volume       = {115},
 number       = {2},
 pages        = {155--158},
 doi          = {10.1016/j.ipl.2014.08.013},
)
@inproceedings(AlurCD90,
 author       = {R. Alur and C. Courcoubetis and D. L. Dill},
 year         = {1990},
 title        = {Model-Checking for Real-Time Systems},
 booktitle    = {Proc. of the Symposium on Logic in Computer Science},
 pages        = {414--425},
 doi          = {10.1109/LICS.1990.113766},
)
@article(BRS06,
 author       = {D. Beauquier and A. M. Rabinovich and A. Slissenko},
 year         = {2006},
 title        = {A Logic of Probability with Decidable Model Checking},
 journal      = {J. Log. Comput.},
 volume       = {16},
 number       = {4},
 pages        = {461--487},
 doi          = {10.1093/logcom/exl004},
)
@article(Buchi60,
 author       = {J. R. Buchi},
 year         = {1960},
 title        = {Weak second order arithmetic and finite automata},
 journal      = {Zeitscrift fur mathematische Logic und Grundlagen der Mathematik},
 volume       = {6},
 pages        = {66--92},
 doi          = {10.1002/malq.19600060105},
)
@article(CHHN14,
 author       = {J. Cassaigne and V. Halava and T. Harju and F. Nicolas},
 year         = {2014},
 title        = {Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More},
 journal      = {arXiv},
 volume       = {abs/1404.0644},
)
@inproceedings(CE81,
 author       = {E. M. Clarke and E. A. Emerson},
 year         = {1981},
 title        = {The Design and Synthesis of Synchronization Skeletons Using Temporal Logic},
 booktitle    = {Proc. of the Workshop on Logics of Programs, IBM Watson Research Center, LNCS 131},
)
@article(CES86,
 author       = {E. M. Clarke and E. A. Emerson and A. P. Sistla},
 year         = {1986},
 title        = {Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications},
 journal      = {{ACM} Trans. Program. Lang. Syst.},
 volume       = {8},
 number       = {2},
 pages        = {244--263},
 doi          = {10.1145/5397.5399},
)
@inproceedings(CondonLipton89,
 author       = {A. Condon and R. J. Lipton},
 year         = {1989},
 title        = {On the complexity of space bounded interactive proofs},
 booktitle    = {Proc. of the Symp. on Foundations of Computer Science},
 publisher    = {IEEE},
 pages        = {462--467},
 doi          = {10.1109/SFCS.1989.63519},
)
@article(DEMO,
 author       = {D.J.N. Eijck},
 year         = {2004},
 title        = {{Dynamic epistemic modelling}},
 journal      = {CWI. Software Engineering [SEN]},
 number       = {E 0424},
 pages        = {1--112},
)
@inproceedings(EGM07,
 author       = {K. Engelhardt and P. Gammie and {R. van der} Meyden},
 year         = {2007},
 title        = {Model Checking Knowledge and Linear Time: {PSPACE} Cases},
 booktitle    = {Proc. of the Int. Symp. on Logical Foundations of Computer Science {LFCS}},
 pages        = {195--211},
 doi          = {10.1007/978-3-540-72734-7\_14},
)
@book(Igorbook,
 author       = {G. Everest and I. Shparlinski and {A. J. van der} Poorten and T. Ward},
 year         = {2003},
 title        = {Recurrence sequences},
 publisher    = {Amer. Math. Soc.},
 doi          = {10.1090/surv/104},
)
@article(FaginHalpern,
 author       = {R. Fagin and J. Y. Halpern},
 year         = {1994},
 title        = {Reasoning About Knowledge and Probability},
 journal      = {J. {ACM}},
 volume       = {41},
 number       = {2},
 pages        = {340--367},
 doi          = {10.1145/174652.174658},
)
@article(FaginHM90,
 author       = {R. Fagin and J. Y. Halpern and N. Megiddo},
 year         = {1990},
 title        = {A Logic for Reasoning about Probabilities},
 journal      = {Information and Computation},
 volume       = {87},
 number       = {1/2},
 pages        = {78--128},
 doi          = {10.1016/0890-5401(90)90060-U},
)
@inproceedings(mck,
 author       = {P. Gammie and {R. van der} Meyden},
 year         = {2004},
 title        = {{MCK}: Model Checking the Logic of Knowledge},
 booktitle    = {Proc. Conf. on Computer-Aided Verification, CAV},
 pages        = {479--483},
 doi          = {10.1007/978-3-540-27813-9\_41},
)
@techreport(Halava97,
 author       = {V. Halava},
 year         = {1997},
 title        = {Decidable and undecidable problems in matrix theory},
 type         = {Technical Report},
 number       = {127},
 institution  = {Turku Centre for Computer Science},
 address      = {University of Turku, Finland},
)
@techreport(Halava05,
 author       = {V. Halava and T. Harju and M. Hirvensalo and J. Karhum\"aki},
 year         = {2005},
 title        = {Skolem's problem - On the border between decidability and undecidability},
 type         = {Technical Report},
 number       = {683},
 institution  = {Turku Centre for Computer Science},
 address      = {University of Turku, Finland},
)
@book(HalpernUncertainty,
 author       = {J. Y. Halpern},
 year         = {2003},
 title        = {Reasoning about Uncertainty},
 publisher    = {MIT Press},
 address      = {Cambridge, MA, USA},
)
@inproceedings(HV91,
 author       = {J. Y. Halpern and M. Y. Vardi},
 year         = {1991},
 title        = {Model Checking vs. Theorem Proving: {A} Manifesto},
 booktitle    = {Proc. of the Int. Conf. on Principles of Knowledge Representation and Reasoning},
 pages        = {325--334},
)
@techreport(Hirvensalo06,
 author       = {M. Hirvensalo},
 year         = {2006},
 title        = {Improved Undecidability Results on the Emptiness Problem of Probabilistic and Quantum Cut-Point Languages},
 type         = {Technical Report},
 number       = {769},
 institution  = {Turku Centre for Computer Science},
 address      = {University of Turku, Finland},
)
@inproceedings(HLM11,
 author       = {X. Huang and C. Luo and {R. van der} Meyden},
 year         = {2011},
 title        = {Symbolic model checking of probabilistic knowledge},
 booktitle    = {Proc. of the Conf. on Theoretical Aspects of Rationality and Knowledge},
 pages        = {177--186},
)
@inproceedings(HM10,
 author       = {X. Huang and {R. van der} Meyden},
 year         = {2010},
 title        = {The Complexity of Epistemic Model Checking: Clock Semantics and Branching Time},
 booktitle    = {Proc. {ECAI} 2010 - European Conf. on Artificial Intelligence},
 pages        = {549--554},
 doi          = {10.3233/978-1-60750-606-5-549},
)
@inproceedings(HSZ12,
 author       = {X. Huang and K. Su and C. Zhang},
 year         = {2012},
 title        = {Probabilistic Alternating-Time Temporal Logic of Incomplete Information and Synchronous Perfect Recall},
 booktitle    = {Proc. {AAAI}},
)
@article(Verics,
 author       = {M. Kacprzak and Nabia{\l}ek, W. and A. Niewiadomski and W. Penczek and P{\'o}{\l}rola, A. and M. Szreter and B. Wo{\'z}na and A. Zbrzezny},
 year         = {2008},
 title        = {VerICS 2007 - a Model Checker for Knowledge and Real-Time},
 journal      = {Fundamenta Informaticae},
 volume       = {85},
 number       = {1},
 pages        = {313--328},
)
@phdthesis(kamp,
 author       = {H. W. Kamp},
 year         = {1968},
 title        = {Tense logic and the theory of linear order},
 school       = {University of California, Los Angeles},
)
@book(KemenySnell1,
 author       = {J. G. Kemeny and J. L. Snell and A. W. Knapp},
 year         = {1976},
 title        = {Denumerable {Markov} Chains},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-1-4684-9455-6},
)
@inproceedings(MCMAS,
 author       = {A. Lomuscio and H. Qu and F. Raimondi},
 year         = {2009},
 title        = {{MCMAS:} A Model Checker for the Verification of Multi-Agent Systems},
 booktitle    = {Proc. Conf. on Computer-Aided Verification},
 pages        = {682--688},
 doi          = {10.1007/978-3-642-02658-4\_55},
)
@inproceedings(MalerNP08,
 author       = {O. Maler and D. Nickovic and A. Pnueli},
 year         = {2008},
 title        = {Checking Temporal Properties of Discrete, Timed and Continuous Behaviors},
 booktitle    = {Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday},
 pages        = {475--505},
)
@book(Matiyasevich,
 author       = {Yuri V. Matiyasevich},
 year         = {1993},
 title        = {Hilbert's Tenth Problem},
 publisher    = {MIT Press},
)
@inproceedings(MeydenShilov,
 author       = {{R. van der} Meyden and N. V. Shilov},
 year         = {1999},
 title        = {Model Checking Knowledge and Time in Systems with Perfect Recall},
 booktitle    = {Proc. FST-TCS},
 pages        = {432--445},
 doi          = {10.1007/3-540-46691-6\_35},
)
@article(MeydenWong03,
 author       = {{R. van der} {Meyden} and K-S. Wong},
 year         = {2003},
 title        = {Complete Axiomatizations for Reasoning about Knowledge and Branching Time},
 journal      = {Studia Logica},
 volume       = {75},
 number       = {1},
 pages        = {93--123},
 doi          = {10.1023/A:1026181001368},
)
@inproceedings(OW14,
 author       = {J. Ouaknine and J. Worrell},
 year         = {2014},
 title        = {Positivity Problems for Low-Order Linear Recurrence Sequences},
 booktitle    = {Proc. {ACM-SIAM} Symposium on Discrete Algorithms},
 pages        = {366--379},
 doi          = {10.1137/1.9781611973402.27},
)
@book(Paz71,
 author       = {A. Paz},
 year         = {1971},
 title        = {Introduction to probabilistic automata},
 publisher    = {Academic Press},
)
@book(prismbook,
 author       = {J. Rutten and M. Kwiatkowska and G. Norman and D. Parker},
 year         = {2004},
 title        = {Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, {\rm P. Panangaden and {F. van} Breugel (eds.)}},
 series       = {CRM Monograph Series},
 volume       = {23},
 publisher    = {American Mathematical Society},
)
@article(shannon49,
 author       = {C. Shannon},
 year         = {1949},
 title        = {Communication Theory of Secrecy Systems},
 journal      = {Bell System Technical Journal},
 volume       = {28},
 number       = {4},
 pages        = {656--715},
 doi          = {10.1002/j.1538-7305.1949.tb00928.x},
)
@inproceedings(Skolem34,
 author       = {T. Skolem},
 year         = {1934},
 title        = {Ein {V}erfahren zur {B}ehandlung gewisser exponentialer {G}leichungen und diophatischer {G}leighungen},
 booktitle    = {8de Skand. mat. Kongr. Forth, Stockholm},
)
@book(Tar1,
 author       = {A. Tarski},
 year         = {1951},
 title        = {A Decision method for elementary algebra and geometry},
 edition      = {2nd},
 publisher    = {Univ. of {C}alifornia {P}ress},
)
@article(TMS84,
 author       = {R. Tijdeman and M. Mignotte and T.N. Shorey},
 year         = {1984},
 title        = {The distance between terms of an algebraic recurrence sequence},
 journal      = {Journal f\"{u}r die reine und angewandte Mathematik},
 volume       = {349},
 pages        = {63--76},
)