Search

• < Previous
• 1
• Next >

---

Model Checking Probabilistic Pushdown Automata

Javier Esparza ; Antonin Kucera ; Richard Mayr.

We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model&nbsp;[&hellip;]

---

Separators in Continuous Petri Nets

Michael Blondin ; Javier Esparza.

Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking $\vec{m}_\text{src}$ cannot reach a marking $\vec{m}_\text{tgt}$, then there is a formula $\varphi$ of Presburger arithmetic such that: $\varphi(\vec{m}_\text{src})$ holds; $\varphi$ is&nbsp;[&hellip;]

---