scientific article; zbMATH DE number 7280017

MaRDI QIDQ5137353zbMATH OpenFDO

Authors Marta Kwiatkowska, Christel Baier

Publication date 2 December 2020

Full work available at URL https://link.springer.com/article/10.1007/s004460050046

zbMATH Keywords

fairnessprobabilistic processestemporal logicverification

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic
• Validation of Stochastic Systems
• Polytime model checking for times probabilistic computation tree logic
• Branching-time logics and fairness, revisited
• Model checking for probabilistic timed automata
• Modalities for model checking: Branching time logic strikes back
• Branching-time model-checking of probabilistic pushdown automata
• Branching-time model-checking of probabilistic pushdown automata
• Model checking for hybrid branching-time logics

Cited in

(34)

• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• Automatic verification of real-time systems with discrete probability distributions.
• Task-structured probabilistic I/O automata
• The satisfiability problem for a quantitative fragment of PCTL
• Preface to the special issue on probabilistic model checking
• Model checking for probabilistic timed automata
• Symbolic model checking for probabilistic timed automata
• Comparative branching-time semantics for Markov chains
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• On the verification of qualitative properties of probabilistic processes under fairness constraints.
• Weak probabilistic anonymity
• Exogenous probabilistic computation tree logic
• Model checking under fairness in ProB and its application to fair exchange protocols
• Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic
• High-level modelling and efficient analysis of randomized protocols.
• Model checking probabilistic systems
• Fair termination for parameterized probabilistic concurrent systems
• On-the-Fly Stuttering in the Construction of Deterministic ω-Automata
• Implementing a fair monodic temporal logic prover
• Quantitative analysis under fairness constraints
• Compositional probabilistic verification through multi-objective model checking
• Model checking linear-time properties of probabilistic systems
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• The satisfiability problem for a quantitative fragment of PCTL
• Playing Against Fair Adversaries in Stochastic Games with Total Rewards
• Correlated equilibria and fairness in concurrent stochastic games
• Logical characterization of branching bisimilarity over random processes
• Quantifying masking fault-tolerance via fair stochastic games
• The finite satisfiability problem for PCTL is undecidable
• Quantitative analysis with the probabilistic model checker PRISM
• The finite satisfiability problem for PCTL is undecidable
• Branching bisimulation congruence for probabilistic systems
• Experiments with deterministic -automata for formulas of linear temporal logic
• Reachability in recursive Markov decision processes

This page was built for publication:

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