Model Checking Temporal Properties of Recursive Probabilistic Programs

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 checki...

Full description

Bibliographic Details
Main Authors: Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2023-12-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/10029/pdf