Parametric Model Checking Continuous-Time Markov Chains
CSL is a well-known temporal logic for specifying properties of real-time stochastic systems, such as continuous-time Markov chains. We introduce PCSL, an extension of CSL that allows using existentially quantified parameters in timing constraints, and investigate its expressiveness and decidability over properties of continuous-time Markov chains. Assuming Schanuel’s Conjecture, we prove the decidability of model checking the one-parameter fragment of PCSL on continuous-time Markov chains. Technically, the central problem we solve (relying on Schanuel’s Conjecture) is to decide positivity of real-valued exponential polynomial functions on bounded intervals. A second contribution is to give a reduction of the Positivity Problem for matrix exponentials to the PCSL model checking problem, suggesting that it will be difficult to give an unconditional proof of the decidability of model checking PCSL.
Probabilistic Continuous Stochastic Logic
Continuous-time Markov Chains
model checking
Schanuel’s Conjecture
positivity problem
Theory of computation~Logic and verification
Theory of computation~Verification by model checking
Theory of computation~Random walks and Markov chains
7:1-7:18
Regular Paper
Catalin-Andrei
Ilie
Catalin-Andrei Ilie
Department of Computer Science, University of Bucharest, Romania
James Ben
Worrell
James Ben Worrell
Department of Computer Science, University of Oxford, UK
Supported by EPSRC Fellowship EP/N008197/1.
10.4230/LIPIcs.TIME.2020.7
S Akshay, Timos Antonopoulos, Joël Ouaknine, and James Worrell. Reachability problems for Markov chains. Information Processing Letters, 115(2):155-158, 2015.
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. Model-checking continuous-time Markov chains. ACM Transactions on Computational Logic (TOCL), 1(1):162-170, 2000.
Paul Bell, Jean-Charles Delvenne, Raphael Jungers, and Vincent D. Blondel. The continuous Skolem-Pisot problem: On the complexity of reachability for linear ordinary differential equations. Theoretical Computer Science, 411(40–42):3625-3634, 2010.
Ventsislav Chonev, Joel Ouaknine, and James Worrell. On the Skolem problem for continuous linear dynamical systems. 43rd International Colloquium on Automata, Languages, and Programming (ICALP), pages 100:1-100:13, 2016.
Henri Cohen. A Course in Computational Algebraic Number Theory. Springer, 1993.
Paul M. Cohn. Basic Algebra: Groups, Rings and Fields. Springer, second edition, 2004.
Bettina Just. Integer relations among algebraic numbers. In International Symposium on Mathematical Foundations of Computer Science, pages 314-320. Springer, 1989.
Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. Proc. 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of LNCS, pages 585-591, Springer, 2011.
Angus Macintyre and Alex J Wilkie. On the decidability of the real exponential field. In (ed. Piergiorgio Odifreddi) Kreiseliana: About and Around Georg Kreisel., 1996.
Ivan Niven. Irrational Numbers. The Mathematical Association of America, fifth edition, 2005.
Paul S Wang. Factoring multivariate polynomials over algebraic number fields. Mathematics of Computation, 30(134):324-336, 1976.
Boris Zilber. Exponential sums equations and the Schanuel conjecture. Journal of the London Mathematical Society, 65(1):27-44, 2002.
Catalin-Andrei Ilie and James Ben Worrell
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode