Analysis of Timed and Long-Run Objectives for Markov Automata

Markov automata (MAs) extend labelled transition systems with random delays and probabilistic branching. Action-labelled transitions are instantaneous and yield a distribution over states, whereas timed transitions impose a random delay governed by an exponential distribution. MAs are thus a nondete...

Full description

Bibliographic Details
Main Authors: Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2014-09-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/943/pdf