Model Checking Temporal Properties of Recursive Probabilistic Programs

DOI10.46298/lmcs-19(4:24)2023arXiv2111.03501MaRDI QIDQ6137848

Unnamed Author, 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)

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 computing (68Qxx) Theory of software (68Nxx) Computer science (68-XX)

Related Items (1)

Model Checking Temporal Properties of Recursive Probabilistic Programs

Cites Work

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

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