Cover Image

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Gerlach, Lina, Winkler, Tobias, Ábrahám, Erika, Bonakdarpour, Borzoo, Junges, Sebastian
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Tractable Hyperproperties for MDPs
by: Gerlach, Lina, et al.
Published: (2026)

Efficient Discovery of Actual Causality using Abstraction-Refinement
by: Rafieioskouei, Arshia, et al.
Published: (2024)

A Hyperlogic for Strategies in Stochastic Games (Extended Version)
by: Gerlach, Lina, et al.
Published: (2025)

Tractable Hyperproperties for MDPs - Artifact
by: Gerlach, Carolina, et al.
Published: (2026)

HypRL: Reinforcement Learning of Control Policies for Hyperproperties
by: Hsu, Tzu-Han, et al.
Published: (2025)

Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed and Accuracy
by: Bonakdarpour, Borzoo, et al.
Published: (2024)

Probabilistic Model Checking Taken by Storm
by: Volk, Matthias, et al.
Published: (2026)

Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
by: Heck, Linus, et al.
Published: (2025)

Syntax-Guided Automated Program Repair for Hyperproperties
by: Beutner, Raven, et al.
Published: (2024)

Policies Grow on Trees: Model Checking Families of MDPs
by: Andriushchenko, Roman, et al.
Published: (2024)

Robust Almost-Sure Reachability in Multi-Environment MDPs
by: van der Vegt, Marck, et al.
Published: (2023)

Model Checking Temporal Properties of Recursive Probabilistic Programs
by: Winkler, Tobias, et al.
Published: (2021)

First-Order LTLf Synthesis with Lookback (Extended Version)
by: Winkler, Sarah
Published: (2025)

Model Checking as Program Verification by Abstract Interpretation (Extended Version)
by: Baldan, Paolo, et al.
Published: (2025)

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
by: Watanabe, Kazuki, et al.
Published: (2024)

Relating Apartness and Branching Bisimulation Games
by: Rot, Jurriaan, et al.
Published: (2024)

Distributional Probabilistic Model Checking
by: Elsayed-Aly, Ingy, et al.
Published: (2023)

HyperQB: A Bounded Model Checker for Hyperproperties
by: Hsu, Tzu-Han, et al.
Published: (2021)

Probabilistic Model Checking: Applications and Trends
by: Kwiatkowska, Marta, et al.
Published: (2025)

Object-Centric Conformance Alignments with Synchronization (Extended Version)
by: Gianola, Alessandro, et al.
Published: (2023)

Property Directed Reachability with Extended Resolution
by: Luka, Andrew, et al.
Published: (2025)

Reachability and Safety Games under TSO Semantics (Extended Version)
by: Spengler, Stephan
Published: (2024)

Shields to Guarantee Probabilistic Safety in MDPs
by: Heck, Linus, et al.
Published: (2026)

Probabilistic Linear Logic Programming with an Application to Bayesian Network Computations (Extended Version)
by: Acclavio, Matteo, et al.
Published: (2026)

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
by: Amat, Nicolas, et al.
Published: (2024)

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
by: Deng, Haotian, et al.
Published: (2025)

Small Test Suites for Active Automata Learning
by: Kruger, Loes, et al.
Published: (2024)

Automata-less Monitoring via Trace-Checking (Extended Version)
by: Brunello, Andrea, et al.
Published: (2025)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Monadic Intersection Types, Relationally (Extended Version)
by: Gavazzo, Francesco, et al.
Published: (2024)

Fixed Point Certificates for Reachability and Expected Rewards in MDPs
by: Chatterjee, Krishnendu, et al.
Published: (2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Learning Robust Markov Models for Safe Runtime Monitoring
by: Skurka, Antonina, et al.
Published: (2026)

Infinite State Model Checking by Learning Transitive Relations
by: Frohn, Florian, et al.
Published: (2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
by: Batz, Kevin, et al.
Published: (2025)

Partially Finite Model Reasoning in Description Logics Extended Version
by: Gogacz, Tomasz, et al.
Published: (2026)

Small Decision Trees for MDPs with Deductive Synthesis
by: Andriushchenko, Roman, et al.
Published: (2025)

A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs
by: Suilen, Marnix, et al.
Published: (2024)

A Unifying Approach to Product Constructions for Quantitative Temporal Inference
by: Watanabe, Kazuki, et al.
Published: (2024)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
by: Haselwarter, Philipp G., et al.
Published: (2026)