On the connections between PCTL and dynamic programming

DOI10.1145/1755952.1755988MaRDI QIDQ2985889zbMATH OpenOpenAlexFDO

Authors Debasish Chatterjee, Sean Summers, John Lygeros, Federico Ramponi

Publication date 10 May 2017

Published in Proceedings of the 13th ACM international conference on Hybrid systems: computation and control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0910.4738

zbMATH Keywords

dynamic programmingintegral equationMarkov processesPCTL

Mathematics Subject Classification ID

Temporal logic (03B44) Computational methods in Markov chains (60J22) Specification and verification (program logics, model checking, etc.) (68Q60) Dynamic programming (90C39)

Abstract: Probabilistic Computation Tree Logic (PCTL) is a well-known modal logic which has become a standard for expressing temporal properties of finite-state Markov chains in the context of automated model checking. In this paper, we give a definition of PCTL for noncountable-space Markov chains, and we show that there is a substantial affinity between certain of its operators and problems of Dynamic Programming. After proving some uniqueness properties of the solutions to the latter, we conclude the paper with two examples to show that some recovery strategies in practical applications, which are naturally stated as reach-avoid problems, can be actually viewed as particular cases of PCTL formulas.

Recommendations

• scientific article; zbMATH DE number 772627
• Generalizations and applications of a class of dynamic programming problems
• Some Problems in the Theory of Dynamic Programming
• scientific article; zbMATH DE number 4174799
• Dynamic programming and pseudo-inverses
• Dynamic programming and d-graphs
• On Bounds for Dynamic Programs
• An application of Kleene's fixed point theorem to dynamic programming
• Declarative dynamic programming as an alternative realization of Courcelle's theorem
• Conjugate duality and its implications in dynamic programming

Cites work

• Decentralized Control of Discrete-Event Systems With Bounded or Unbounded Delay Communication
• Discrete-time control for rectangular hybrid automata
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 1444339 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Marked directed graphs
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Stability Analysis of Networked Control Systems Using a Switched Linear Systems Approach
• Unfoldings: A partial-order approach to model checking.
• What's decidable about hybrid automata?

Cited in

(9)

• Automated verification and synthesis of stochastic hybrid systems: a survey
• Robustly complete finite-state abstractions for verification of stochastic systems
• Stochastic system controller synthesis for reachability specifications encoded by random sets
• More or less true DCTL for continuous-time MDPs
• Characterization and computation of infinite-horizon specifications over Markov processes
• Control synthesis for stochastic systems given automata specifications defined by stochastic sets
• Dynamic Bayesian networks for formal verification of structured stochastic processes
• Maximizing the probability of attaining a target prior to extinction
• Formal controller synthesis for Markov jump linear systems with uncertain dynamics

This page was built for publication: On the connections between PCTL and dynamic programming

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