Probabilistic verification beyond context-freeness

DOI10.1145/3531130.3533351MaRDI QIDQ6649464

Guanyan Li, Luke Ong, Andrzej S. Murawski

Publication date: 6 December 2024

zbMATH Keywords

first-order theory of the realscomputing termination probabilitydeciding almost sure terminationprobabilistic (affine additive) higher-order recursion schemesrestricted (probabilistic) tree stack automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• On multiple context-free grammars
• On the hardness of analyzing probabilistic programs
• Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
• Analyzing probabilistic pushdown automata
• MIX is a 2-MCFL and the word problem in \(\mathbb{Z}^2\) is captured by the IO and the OI hierarchies
• A lattice-theoretical fixpoint theorem and its applications
• An Automata Characterisation for Multiple Context-Free Languages
• Markov Chains
• Types and higher-order recursion schemes for verification of higher-order programs
• Collapsible Pushdown Automata and Recursion Schemes
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Probabilistic verification beyond context-freeness