Model Checking Algorithms for Markov Automata
Hassan Hatefi, Holger Hermanns
Abstract
Markov automata constitute a compositional modeling formalism spanning as special cases the models of discrete and continuous time Markov chains, as well as interactive Markov chains and probabilistic automata. This paper discusses the core algorithmic ingredients of a numerical model checking procedure for Markov automata with respect to a PCTL or CSL like temporal logic. The main challenge lies in the computation of time-bounded reachability probabilities, for which we provide a stable approximation scheme.
Topics & Concepts
Markov chainComputer scienceReachabilityAutomatonFormalism (music)Probabilistic logicAlgorithmMarkov modelQuantum finite automataTheoretical computer scienceBounded functionModel checkingProbabilistic CTLMarkov processVariable-order Markov modelAutomata theoryProbabilistic analysis of algorithmsMathematicsArtificial intelligenceMachine learningVisual artsMathematical analysisArtMusicalStatisticsFormal Methods in VerificationAdvanced Software Engineering MethodologiesModel-Driven Software Engineering Techniques