Model Checking Linear-Time Properties of Probabilistic Systems

DOI10.1007/978-3-642-01492-5_13zbMath1484.68095OpenAlexW1679405140MaRDI QIDQ5072555

Frank Ciesinski, Marcus Größer, Christel Baier

Publication date: 28 April 2022

Published in: Monographs in Theoretical Computer Science. An EATCS Series (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-01492-5_13

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (6)

Model Checking Probabilistic Systems ⋮ Singular value automata and approximate minimization ⋮ A coalgebraic perspective on linear weighted automata ⋮ Pumping Lemmata for Recognizable Weighted Languages over Artinian Semirings ⋮ Generalization bounds for learning weighted automata ⋮ Verification and control for probabilistic hybrid automata with finite bisimulations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A stubborn attack on state explosion
• Skew and infinitary formal power series
• Weighted automata with discounting
• Bisimulation through probabilistic testing
• Symbolic model checking: \(10^{20}\) states and beyond
• A logic for reasoning about time and reliability
• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• Automatic verification of real-time systems with discrete probability distributions.
• Combinatorial optimization. Polyhedra and efficiency (3 volumes)
• Automata, logics, and infinite games. A guide to current research
• Quantitative solution of omega-regular games
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Deciding bisimilarity and similarity for probabilistic processes.
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• A survey of algorithmic methods for partially observed Markov decision processes
• Model checking of probabilistic and nondeterministic systems
• Weighted Automata and Weighted Logics with Discounting
• Quantitative Model Checking Revisited: Neither Decidable Nor Approximable
• Probabilistic CEGAR
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Partial Order Reduction for Markov Decision Processes: A Survey
• The Complexity of Markov Decision Processes
• State of the Art—A Survey of Partially Observable Markov Decision Processes: Theory, Models, and Algorithms
• The complexity of probabilistic verification
• Symbolic model checking for probabilistic processes
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• Traces, Series-Parallel Posets, and Pictures: A Weighted Study
• On Reduction Criteria for Probabilistic Reward Models
• On Decision Problems for Probabilistic Büchi Automata
• Probabilistic automata
• Automata, Languages and Programming
• Counterexamples in Probabilistic Model Checking
• Formal Modeling and Analysis of Timed Systems

This page was built for publication: Model Checking Linear-Time Properties of Probabilistic Systems