On the termination problem for probabilistic higher-order recursive programs

MaRDI QIDQ5129945zbMATH OpenFDO

Authors Naoki Kobayashi, Ugo Dal Lago, Charles Grellois

Publication date 3 November 2020

Full work available at URL https://arxiv.org/abs/1811.02133, https://lmcs.episciences.org/6817

zbMATH Keywords

higher-order programsmodel checkingprobabilistic programstermination probabilities

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Automata, Probability, and Recursion
• Model-checking higher-order programs with recursive types
• On the hardness of almost-sure termination
• Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs

Cites work

• A type-directed abstraction refinement approach to higher-order model checking
• Analyzing probabilistic pushdown automata
• Branching-time model-checking of probabilistic pushdown automata
• Collapsible pushdown automata and recursion schemes
• Complexity of model checking recursion schemes for fragments of the modal mu-calculus
• Compositional higher-order model checking via -regular games over Böhm trees
• COMPUTING LEAST FIXED POINTS OF PROBABILISTIC SYSTEMS OF POLYNOMIALS
• CONCUR 2005 – Concurrency Theory
• Design and analysis of randomized algorithms. Introduction to design paradigms.
• Environmental bisimulations for probabilistic higher-order languages
• Finitary semantics of linear logic and higher-order model-checking
• Handbook of model checking
• scientific article; zbMATH DE number 1722657 (Why is no real title available?)
• scientific article; zbMATH DE number 4179422 (Why is no real title available?)
• scientific article; zbMATH DE number 5485454 (Why is no real title available?)
• scientific article; zbMATH DE number 3615887 (Why is no real title available?)
• scientific article; zbMATH DE number 1231645 (Why is no real title available?)
• scientific article; zbMATH DE number 545277 (Why is no real title available?)
• scientific article; zbMATH DE number 2087432 (Why is no real title available?)
• scientific article; zbMATH DE number 1911266 (Why is no real title available?)
• scientific article; zbMATH DE number 819814 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable
• Krivine machines and higher-order schemes
• Model checking higher-order programs
• Model checking of recursive probabilistic systems
• On coinductive equivalences for higher-order probabilistic functional programs
• On probabilistic applicative bisimulation and call-by-value \(\lambda \)-calculi
• On probabilistic term rewriting
• On the \(\lambda Y\) calculus
• On the hardness of almost-sure termination
• On the termination problem for probabilistic higher-order recursive programs
• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Probabilistic automata on finite words: decidable and undecidable problems
• Probabilistic coherence spaces are fully abstract for probabilistic PCF
• Probabilistic encryption
• Probabilistic game semantics
• Probabilistic operational semantics for the lambda calculus
• Probabilistic termination by monadic affine sized typing
• Probabilistic termination: soundness, completeness, and compositionality
• Probabilistic Turing Machines and Computability
• Recursion schemes and the WMSO+U logic
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Recursive Markov decision processes and recursive stochastic games
• Relational semantics of linear logic and higher-order model checking
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
• Stochastic invariants for probabilistic termination
• Term Rewriting and Applications
• The IO and OI hierarchies revisited
• Types and higher-order recursion schemes for verification of higher-order programs

Cited in

(16)

• Probabilistic termination: soundness, completeness, and compositionality
• On higher-order probabilistic subrecursion
• A higher-order characterization of probabilistic polynomial time
• scientific article; zbMATH DE number 1832220 (Why is no real title available?)
• A probabilistic higher-order fixpoint logic
• On higher-order probabilistic subrecursion
• On the termination problem for probabilistic higher-order recursive programs
• New approaches for almost-sure termination of probabilistic programs
• On higher-order reachability games vs may reachability
• On Lexicographic Proof Rules for Probabilistic Termination
• Certificates for probabilistic pushdown automata via optimistic value iteration
• On lexicographic proof rules for probabilistic termination
• Probabilistic verification beyond context-freeness
• Curry and Howard meet Borel
• On the termination problem for probabilistic higher-order recursive programs
• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity

Describes a project that uses

Uses Software

• MoCHi

This page was built for publication: On the termination problem for probabilistic higher-order recursive programs

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