Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination

DOI10.1016/j.ic.2019.104504zbMath1443.68101arXiv1709.02093OpenAlexW2995644129MaRDI QIDQ2182734

Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Christel Baier, Joachim Klein, Joost-Pieter Katoen

Publication date: 26 May 2020

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1709.02093

zbMATH Keywords

computational complexityGaussian eliminationPCTLparametric Markov chainparametric model checking

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Markov chains (discrete-time Markov processes on discrete state spaces) (60J10) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

Formal abstraction and synthesis of parametric stochastic processes, Model checking finite-horizon Markov chains with probabilistic inference, Fine-tuning the odds in Bayesian networks, Gradient-descent for randomized controllers under partial observability, The complexity of reachability in parametric Markov decision processes, Parameter synthesis in Markov models: a gentle survey, POMDP controllers with optimal budget, Unnamed Item, Are Parametric Markov Chains Monotonic?, Finding provably optimal Markov chains, Inductive synthesis for probabilistic programs reaches new horizons

Uses Software

• PRISM
• Eigen
• PARAM
• Storm
• PROPhESY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Parametric probabilistic transition systems for system design and analysis
• Probabilistic self-stabilization
• Solving systems of linear equations over polynomials
• The complexity of elementary algebra and geometry
• An algorithm for solving parametric linear systems
• A logic for reasoning about time and reliability
• Probabilistic verification of Herman's self-stabilisation algorithm
• Parameter synthesis for Markov models: faster than ever
• Reachability in augmented interval Markov chains
• Sequential Convex Programming for the Efficient Verification of Parametric MDPs
• The Exact Solution of Systems of Linear Equations with Polynomial Coefficients
• LTL Model Checking of Interval Markov Chains
• Model-Checking ω-Regular Properties of Interval Markov Chains
• Computational Solutions of Matrix Problems Over an Integral Domain
• Theoretical Aspects of Computing - ICTAC 2004
• Tools and Algorithms for the Construction and Analysis of Systems