3 results
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 […]
Published on March 7, 2006
A. R. Balasubramanian ; Javier Esparza ; Mikhail Raskin.
In rendez-vous protocols an arbitrarily large number of indistinguishable finite-state agents interact in pairs. The cut-off problem asks if there exists a number $B$ such that all initial configurations of the protocol with at least $B$ agents in a given initial state can reach a final […]
Published on October 12, 2023
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 […]
Published on February 21, 2024