A probabilistic logic for verifying continuous-time Markov chains

DOI10.1007/978-3-030-99527-0_1MaRDI QIDQ6535602zbMATH OpenFDO

Authors Ji Guan, Nengkun Yu

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-99527-0_1

Mathematics Subject Classification ID

Temporal logic (03B44) Probability and inductive logic (03B48) Continuous-time Markov processes on general state spaces (60J25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model-checking continuous-time Markov chains
• scientific article; zbMATH DE number 1670788
• Model checking conditional CSL for continuous-time Markov chains
• Theoretical Aspects of Computing – ICTAC 2005
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

Cites work

• A logic for reasoning about time and reliability
• A theory of timed automata
• Approximate verification of the symbolic dynamics of Markov chains
• Automata-based CSL model checking
• Deciding polynomial-exponential problems
• Decision problems for linear recurrence sequences
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• How to recognize zero?
• scientific article; zbMATH DE number 1670788 (Why is no real title available?)
• scientific article; zbMATH DE number 47603 (Why is no real title available?)
• scientific article; zbMATH DE number 1169378 (Why is no real title available?)
• scientific article; zbMATH DE number 2087806 (Why is no real title available?)
• scientific article; zbMATH DE number 906955 (Why is no real title available?)
• scientific article; zbMATH DE number 3232021 (Why is no real title available?)
• scientific article; zbMATH DE number 3334376 (Why is no real title available?)
• scientific article; zbMATH DE number 7730615 (Why is no real title available?)
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Model-checking continuous-time Markov chains
• Monitoring CTMCs by multi-clock timed automata
• Observing continuous-time MDPs by 1-clock timed automata
• On the Skolem problem for continuous linear dynamical systems
• On the zeros of exponential polynomials
• On the zeros of exponential polynomials.
• Parametric real-time reasoning
• Positive root isolation for poly-powers
• Reachability Analysis for Solvable Dynamical Systems
• Reachability problems for Markov chains
• Real root isolation for exp-log functions
• Real root isolation for tame elementary functions
• Some Consequences of Schanuel's Conjecture in Exponential Rings
• The probabilistic model checking landscape
• Time-bounded termination analysis for probabilistic programs with delays
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Über die analytischen Methoden in der Wahrscheinlichkeitsrechnung

Cited in

(3)

• On the metric temporal logic for continuous stochastic processes
• Checking continuous stochastic logic against quantum continuous-time Markov chains
• A sample-driven solving procedure for the repeated reachability of quantum continuous-time Markov chains

This page was built for publication: A probabilistic logic for verifying continuous-time Markov chains

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