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