Reachability Analysis of Probabilistic Systems by Successive Refinements

No abstract is available for this paper.

• Publication year

  2001

• Venue

  Process Algebra and Probabilistic Methods, Performance Modeling and Verification

• Publication date

  2001-09-12

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/3-540-44804-7_3
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems

  2003cited by this paper
• Probabilistic Extensions of Process Algebras

  2001cited by this paper
• A Markov Chain Model Checker

  2000cited by this paper
• Dynamic Partitioning in Linear Relation Analysis. Application to the Verification of Synchronous Programs

  2000cited by this paper
• Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation

  2000cited by this paper
• Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains

  1999cited by this paper
• ProbVerus: Probabilistic Symbolic Model Checking

  1999cited by this paper
• Approximate Symbolic Model Checking of Continuous-Time Markov Chains

  1999cited by this paper
• Automatic verification of real-time systems with discrete probability distributions

  1999cited by this paper
• Theories of Programming Languages: Communicating Sequential Processes

  1998cited by this paper
• Partition Refinement in Real-Time Model Checking

  1998cited by this paper
• Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation

  1997influential reference
• Algebric Decision Diagrams and Their Applications

  1997cited by this paper
• Quantitative analysis and model checking

  1997cited by this paper
• The Bounded Retransmission Protocol Must Be on Time!

  1997influential reference
• Modeling and verification of randomized distributed real-time systems

  1996cited by this paper
• Deductive Model Checking

  1996cited by this paper
• Model Checking of Probabalistic and Nondeterministic Systems

  1995cited by this paper
• It Usually Works: The Temporal Logic of Stochastic Systems

  1995cited by this paper
• Markov Decision Processes: Discrete Stochastic Dynamic Programming

  1994cited by this paper
• Proof-Checking a Data Link Protocol

  1994influential reference
• Markov Decision Processes: Discrete Stochastic Dynamic Programming

  1994cited by this paper
• Algebraic decision diagrams and their applications

  1993influential reference
• A Bounded Retransmission Protocol for Large Data Packets: A Case Study in Computer Checked Algebraic Verification

  1993cited by this paper
• Minimal State Graph Generation

  1992cited by this paper
• Minimization of Timed Transition Systems

  1992cited by this paper
• Bisimulation through Probabilistic Testing

  1991cited by this paper
• Specification and refinement of probabilistic processes

  1991cited by this paper
• Korth cm. International business : environment and management. Prentice hall, inc, englewood cliffs, 1985, 2a ed

  1985cited by this paper

• A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs

  2025cites this paper
• Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions

  2023cites this paper
• Graph-Based Reductions for Parametric and Weighted MDPs

  2023cites this paper
• Bayesian statistical model-checking of continuous stochastic logic by

  2022cites this paper
• Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

  2022cites this paper
• Continuous verification of system of systems with collaborative MAPE-K pattern and probability model slicing

  2022cites this paper
• Generating probabilistic safety guarantees for neural network controllers

  2021cites this paper
• Latticed k-Induction with an Application to Probabilistic Programs

  2021cites this paper
• Approximate Bisimulation Minimisation

  2021cites this paper
• Probabilistic Model Checking and Autonomy

  2021cites this paper
• Scenario-based verification of uncertain parametric MDPs

  2021cites this paper
• PrIC3: Property Directed Reachability for MDPs

  2020cites this paper
• Bayesian Statistical Model Checking for Continuous Stochastic Logic

  2020cites this paper
• Switss: Computing Small Witnessing Subsystems

  2020cites this paper
• Out of Control: Reducing Probabilistic Models by Control-State Elimination

  2020cites this paper
• Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints

  2019cites this paper
• Are Parametric Markov Chains Monotonic?

  2019cites this paper
• Probabilistic Models

  2019cites this paper
• The 10, 000 Facets of MDP Model Checking

  2019cites this paper
• A PSO-Based CEGAR Framework for Stochastic Model Checking

  2019cites this paper
• Accelerated Learning of Predictive Runtime Monitors for Rare Failure

  2019cites this paper
• Counterexample Guided Abstraction Refinement for Polyhedral Probabilistic Hybrid Systems

  2019cites this paper
• Statistical verification of PCTL using antithetic and stratified samples

  2019cites this paper
• Parameter synthesis for Markov models: covering the parameter space

  2019cites this paper
• Predictive Runtime Verification of Stochastic Systems

  2019cites this paper
• Formal System Verification

  2018cites this paper
• Probabilistic model checking: advances and applications

  2018cites this paper
• Abstract model repair for probabilistic systems

  2018cites this paper
• Bounded Verification of Reachability of Probabilistic Hybrid Systems

  2018cites this paper
• Reachability in Parametric Interval Markov Chains Using Constraints

  2017cites this paper
• DR AF T Probabilistic Model Checking : Advances and Applications

  2017cites this paper
• Constraint modelling and solving of some verification problems. (Modélisation et résolution par contraintes de problèmes de vérification)

  2017cites this paper
• The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes

  2017cites this paper
• Modal Stochastic Games - Abstraction-Refinement of Probabilistic Automata

  2017influential citation
• Continuous simulation abstraction refinement for Markov decision processes

  2017cites this paper
• Abstraction Based Reachability Analysis for Finite Branching Stochastic Hybrid Systems

  2017cites this paper
• SMT-based Searching for k-quasi-optimal Runs in Weighted Timed Automata

  2017cites this paper
• Spielbasierte Abstraktion von Markow-Automaten

  2016cites this paper
• An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties

  2016cites this paper
• Less is More

  2016cites this paper
• On-the-fly model checking for extended action-based probabilistic operators

  2016influential citation
• Qualitative Model Checking of Markov Decision Processes on GPUs

  2015cites this paper
• Formal Verification and Synthesis for Discrete-Time Stochastic Systems

  2015cites this paper
• Projection Matrix Optimization for Sparse Signals in Structured Noise

  2015cites this paper
• Garantías cuantitativas para espacios de estados no tratables

  2015cites this paper
• Using SPIN to Check Nondeterministic Simulink Stateflow Models

  2015cites this paper
• In the quantitative automata zoo

  2015cites this paper
• CEGAR for compositional analysis of qualitative properties in Markov decision processes

  2015cites this paper
• Counterexamples in probabilistic verification

  2015cites this paper
• Counterexample Explanation by Learning Small Strategies in Markov Decision Processes

  2015cites this paper
• Abstraction and refinement of probabilistic automata using modal stochastic games

  2015cites this paper
• Computing Conditional Probabilities in Markovian Models Efficiently

  2014cites this paper
• 25 Years of Model Checking

  2014cites this paper
• Minimal counterexamples for linear-time probabilistic verification

  2014cites this paper
• CEGAR for Qualitative Analysis of Probabilistic Systems

  2014cites this paper
• Verification of Markov Decision Processes Using Learning Algorithms

  2014cites this paper
• Selection Pressure in Alternative Reading Frames

  2014cites this paper
• GPU-aided Model Checking of Markov Decision Processes

  2014cites this paper
• Symbolic Model Checking of Probabilistic Systems using Multi-Terminal Binary Decision Diagrams

  2014cites this paper
• Quantitative Verification of the Bounded Retransmission Protocol

  2014cites this paper
• Local abstraction refinement for probabilistic timed programs

  2014influential citation
• Minimal Critical Subsystems for PCTL

  2013cites this paper
• An analysis for proving probabilistic termination of biological systems

  2013cites this paper
• Automated reliability estimation over partial systematic explorations

  2013cites this paper
• Stochastic Analysis of Synthetic Genetic Circuits

  2013cites this paper
• Incremental Bisimulation Abstraction Refinement

  2013cites this paper
• Efficient Probabilistic Parameter Synthesis for Adaptive Systems

  2013cites this paper
• LTL Model Checking of Interval Markov Chains

  2013influential citation
• Tulip: Model Checking Probabilistic Systems Using Expectation Maximisation Algorithm

  2013cites this paper
• Variable Probabilistic Abstraction Refinement

  2012cites this paper
• State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems

  2012cites this paper
• MODEST - A unified language for quantitative models

  2012cites this paper
• On Abstraction of Probabilistic Systems

  2012cites this paper
• Advances in Probabilistic Model Checking

  2012cites this paper
• Probabilistic model checking of biological systems with uncertain kinetic rates

  2012cites this paper
• Analyzing Oscillatory Behavior with Formal Methods

  2012cites this paper
• A linear process-algebraic format with data for probabilistic automata

  2012cites this paper
• Three-valued abstraction for probabilistic systems

  2012cites this paper
• Heuristics for Probabilistic Timed Automata with Abstraction Refinement

  2012cites this paper
• Transient Reward Approximation for Continuous-Time Markov Chains

  2012cites this paper
• Transient Reward Approximation for Grids, Crowds, and Viruses

  2012cites this paper
• Algorithmic probabilistic game semantics

  2012cites this paper
• Minimal Counterexamples for Refuting ω-Regular Properties of Markov Decision Processes – Extended Version –

  2012cites this paper
• Roadmap Document on Stochastic Analysis

  2012cites this paper
• Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems

  2011cites this paper
• Scaling probabilistic timing verification of hardware using abstractions in design source code

  2011cites this paper
• Process Algebra with Timed-Priority Executing Policy

  2011cites this paper
• Propagation Models for Biochemical Reaction Networks

  2011cites this paper
• Abstract Probabilistic Semantics for the Analysis of Biological Systems Models PhD Program in Computer Science and Engineering XXIII Cycle

  2011cites this paper
• Finite-state abstractions for probabilistic computation tree logic

  2011cites this paper
• Deliverable no . : D 2 . 4 Title of Deliverable : Abstraction and Refinement

  2011cites this paper
• Modular Specification and Compositional Analysis of Stochastic Systems. (Spécification Modulaire et Analyse Compositionnelle de Systèmes Stochastiques)

  2010cites this paper
• Best Probabilistic Transformers

  2010cites this paper
• PASS: Abstraction Refinement for Infinite Probabilistic Models

  2010cites this paper
• Conceptual Models for Assessment & Assurance of Dependability, Security and Privacy in the Eternal CONNECTed World

  2010cites this paper
• Advances and challenges of probabilistic model checking

  2010cites this paper
• A Linear Process-Algebraic Format for Probabilistic Systems with Data

  2010cites this paper
• Goal based bisimulation for testing therapies in traditional Chinese medicine

  2010cites this paper
• A game-based abstraction-refinement framework for Markov decision processes

  2010influential citation
• Stochastic abstraction of programs : towards performance-driven development

  2010cites this paper