A probabilistic PDL

DOI10.1016/0022-0000(85)90012-1zbMath0575.03013OpenAlexW2000108089MaRDI QIDQ1063584

Publication date: 1985

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(85)90012-1

zbMATH Keywords

probabilistic programs small model property analysis of probabilistic algorithms deductive calculus probabilistic analog of propositional dynamic logic

Mathematics Subject Classification ID

Sums of independent random variables; random walks (60G50) Modal logic (including the logic of norms) (03B45) Probability and inductive logic (03B48) General theory of stochastic processes (60G07) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Model theory of finite structures (03C13) Algorithms in computer science (68W99)

Related Items

Formal semantics of a classical-quantum language ⋮ Approximating Labelled Markov Processes Again! ⋮ Extending propositional dynamic logic for Petri nets ⋮ A metrized duality theorem for Markov processes ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ Quantitative logics for equivalence of effectful programs ⋮ A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ Hennessy-Milner results for probabilistic PDL ⋮ Reasoning about probabilistic sequential programs ⋮ An exercise on the generation of many-valued dynamic logics ⋮ A Demonic Approach to Information in Probabilistic Systems ⋮ Unnamed Item ⋮ A pseudometric in supervisory control of probabilistic discrete event systems ⋮ Metrics for labelled Markov processes ⋮ Symbolic model checking for probabilistic processes ⋮ Semantics of Probabilistic Programs: A Weak Limit Approach ⋮ Discussion on: ``Safety verification for probabilistic hybrid systems ⋮ Approximating labelled Markov processes ⋮ A specification logic for programs in the probabilistic guarded command language ⋮ Program algebra for quantitative information flow ⋮ Aleatoric propositions: reasoning about coins ⋮ Approximating Markov processes through filtration ⋮ Conditioning in probabilistic programming ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ A propositional dynamic logic with qualitative probabilities ⋮ Real-reward testing for probabilistic processes ⋮ On the hardness of analyzing probabilistic programs ⋮ Automated termination analysis of polynomial probabilistic programs ⋮ A stochastic interpretation of game logic ⋮ VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC ⋮ Probabilistic Logic over Paths ⋮ A logical duality for underspecified probabilistic systems ⋮ Probabilization of logics: completeness and decidability ⋮ Hidden-Markov program algebra with iteration ⋮ A behavioural pseudometric for probabilistic transition systems ⋮ A Type Theory for Probabilistic and Bayesian Reasoning ⋮ Unnamed Item ⋮ Temporalization of Probabilistic Propositional Logic ⋮ Bisimulation for labelled Markov processes ⋮ Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs ⋮ Probabilistic NetKAT ⋮ Categories of Timed Stochastic Relations ⋮ Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular ⋮ Approximating Markov Processes by Averaging ⋮ A logic for reasoning about probabilities ⋮ Reverse Hoare Logic ⋮ Moment-based analysis of Bayesian network properties ⋮ Quantitative static analysis of communication protocols using abstract Markov chains ⋮ A probabilistic dynamic logic ⋮ Measure and probability for concurrency theorists ⋮ Probabilistic guarded commands mechanized in HOL ⋮ A semantics and a logic for \textit{Fuzzy Arden Syntax} ⋮ Decidability of finite probabilistic propositional dynamic logics ⋮ Probabilistic Temporal Logics

Cites Work