Probabilistic verification beyond context-freeness

DOI10.1145/3531130.3533351MaRDI QIDQ6649464zbMATH OpenFDO

Authors Guanyan Li, Andrzej S. Murawski, Luke Ong

Publication date 6 December 2024

Full work available at URL https://doi.org/10.1145/3531130.3533351

zbMATH Keywords

computing termination probabilitydeciding almost sure terminationfirst-order theory of the realsprobabilistic (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

• A lattice-theoretical fixpoint theorem and its applications
• An Automata Characterisation for Multiple Context-Free Languages
• Analyzing probabilistic pushdown automata
• Collapsible pushdown automata and recursion schemes
• Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
• scientific article; zbMATH DE number 3597592 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3053259 (Why is no real title available?)
• Linear logic
• Markov Chains
• MIX is a 2-MCFL and the word problem in \(\mathbb{Z}^2\) is captured by the IO and the OI hierarchies
• On multiple context-free grammars
• On the expressivity of linear recursion schemes
• On the hardness of analyzing probabilistic programs
• On the termination problem for probabilistic higher-order recursive programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Types and higher-order recursion schemes for verification of higher-order programs

Cited in

(1)

• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity

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

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