Search

• < Previous
• 1
• Next >

---

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

Taolue Chen ; Tingting Han ; Joost-Pieter Katoen ; Alexandru Mereacre.

We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C&nbsp;[&hellip;]

---

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;]

---

Model Checking Temporal Properties of Recursive Probabilistic Programs

Tobias Winkler ; Christina Gehnen ; Joost-Pieter Katoen.

Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties are useful for specifying the chronological order of events during program execution. Existing approaches for model&nbsp;[&hellip;]

---