Model Checking Temporal Properties of Recursive Probabilistic Programs

DOI10.1007/978-3-030-99253-8_23arXiv2111.03501MaRDI QIDQ6137848FDOQ6137848

Authors: Tobias Winkler, Joost-Pieter Katoen 

Publication date: 16 January 2024

Published in: Lecture Notes in Computer Science, Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on $omega$-regular and LTL properties. In this paper, we study the model checking problem of pPDA against $omega$-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than $omega$-regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.

Full work available at URL: https://arxiv.org/abs/2111.03501

zbMATH Keywords

caretmodel checkingvisibly pushdown languagesprobabilistic pushdown automataCaRetprobabilistic recursive programs

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of software (68Nxx) Theory of computing (68Qxx) Computer science (68-XX)

Cites Work

• Visibly pushdown languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Labelled Markov processes.
• Proofs of randomized algorithms in Coq
• An introduction to randomized algorithms
• Model Checking Probabilistic Pushdown Automata
• Tools and Algorithms for the Construction and Analysis of Systems
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Analyzing probabilistic pushdown automata
• Model checking probabilistic systems against pushdown specifications
• Tools and Algorithms for the Construction and Analysis of Systems
• STACS 2005
• First-Order and Temporal Logics for Nested Words
• Title not available (Why is that?)
• Branching processes in biology
• Probabilistic relational reasoning for differential privacy
• Partial correctness for probabilistic demonic programs
• Visibly linear temporal logic
• Computing the least fixed point of positive polynomial systems
• Operator precedence temporal logic and model checking
• Model Checking Procedural Programs
• Complex probabilistic modeling with recursive relational Bayesian networks
• Reasoning about Recursive Probabilistic Programs
• Upper Bounds for Newton’s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata
• A Branching Time Variant of CaRet
• Model Checking Temporal Properties of Recursive Probabilistic Programs

Cited In (2)

• Model Checking Temporal Properties of Recursive Probabilistic Programs
• Certificates for probabilistic pushdown automata via optimistic value iteration

This page was built for publication: Model Checking Temporal Properties of Recursive Probabilistic Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137848)