Search

• < Previous
• 1
• Next >

---

Analysis of Timed and Long-Run Objectives for Markov Automata

Dennis Guck ; Hassan Hatefi ; Holger Hermanns ; Joost-Pieter Katoen ; Mark Timmer.

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&nbsp;[&hellip;]

---

High-level Counterexamples for Probabilistic Automata

Ralf Wimmer ; Nils Jansen ; Erika Ã?brahÃ?m ; Joost-Pieter Katoen.

Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of limited&nbsp;[&hellip;]

---