scientific article

zbMath0974.68017MaRDI QIDQ2754096

Holger Hermanns, Boudewijn R. Haverkort, Joost-Pieter Katoen, Christel Baier

Publication date: 11 November 2001

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Reliability, testing and fault tolerance of networks and computer systems (68M15)

Related Items

Scenario-Based Verification of Uncertain MDPs ⋮ Model Checking of Biological Systems ⋮ Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Precisely deciding CSL formulas through approximate model checking for CTMCs ⋮ Fault trees on a diet: automated reduction by graph rewriting ⋮ On the relations between Markov chain lumpability and reversibility ⋮ Precise parameter synthesis for stochastic biochemical systems ⋮ Learning deterministic probabilistic automata from a model checking perspective ⋮ Petri-net-based 2D design of DNA walker circuits ⋮ Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference ⋮ Model-checking large structured Markov chains. ⋮ Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Lumpability abstractions of rule-based systems ⋮ Optimal deterministic controller synthesis from steady-state distributions ⋮ Distributed disk-based algorithms for model checking very large Markov chains ⋮ Parameter and Controller Synthesis for Markov Chains with Actions and State Labels. ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ Sampling-Based Verification of CTMCs with Uncertain Rates ⋮ Probabilistic model checking of complex biological pathways ⋮ Guarded autonomous transitions increase conciseness and expressiveness of timed automata ⋮ Performability assessment by model checking of Markov reward models ⋮ IDD-based model validation of biochemical networks ⋮ Model checking expected time and expected reward formulae with random time bounds ⋮ Model checking Markov population models by stochastic approximations ⋮ Statistical probabilistic model checking with a focus on time-bounded properties ⋮ Delayed Nondeterminism in Continuous-Time Markov Decision Processes ⋮ Computation tree measurement language (CTML) ⋮ Fluid computation of passage-time distributions in large Markov models ⋮ Logical characterization of fluid equivalences ⋮ Model checking discounted temporal properties ⋮ Weak Probabilistic Anonymity ⋮ Model checking single agent behaviours by fluid approximation