Model checking single agent behaviours by fluid approximation

DOI10.1016/j.ic.2015.03.002zbMath1317.68108OpenAlexW2162314735MaRDI QIDQ2346412

Luca Bortolussi, Jane Hillston

Publication date: 1 June 2015

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2015.03.002

zbMATH Keywords

mean field approximationfluid approximationstochastic model checkingreachability probabilitytime-inhomogeneous continuous-time Markov chains

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Continuous-time Markov processes on discrete state spaces (60J27) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (8)

Fluid Analysis of Spatio-Temporal Properties of Agents in a Population Model ⋮ Fluid Model Checking of Timed Properties ⋮ Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference ⋮ Model checking Markov population models by stochastic approximations ⋮ Fluid approximation of broadcasting systems ⋮ Mean-Field Limits Beyond Ordinary Differential Equations ⋮ Spatial Logic and Spatial Model Checking for Closure Spaces ⋮ Hybrid behaviour of Markov population models

Uses Software

• PRISM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fluid computation of passage-time distributions in large Markov models
• Derived eigenvalues of symmetric matrices, with applications to distance geometry
• A fluid analysis framework for a Markovian process algebra
• Differential equation approximations for Markov chains
• Enclosing all zeros of an analytic function - a rigorous approach
• Interval analysis: Theory and applications
• Zero tests for constants in simple scientific computation
• Systems of linear ordinary differential equations with bounded coefficients may have very oscillating solutions
• Fluid Model Checking
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Satisfiability of Systems of Equations of Real Analytic Functions Is Quasi-decidable
• A lambda calculus for real analysis
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
• Abstraction Refinement for Probabilistic Software
• Dynamical Systems and Stochastic Programming: To Ordinary Differential Equations and Back
• LTL Model Checking of Time-Inhomogeneous Markov Chains
• Recursive algorithms, urn processes and chaining number of chain recurrent sets
• Markov Chains
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation
• Game-Based Probabilistic Predicate Abstraction in PRISM
• On the Approximation of Stochastic Concurrent Constraint Programming by Master Equation
• Deterministic Approximation of Stochastic Evolution in Games
• Solutions of ordinary differential equations as limits of pure jump markov processes
• Model-checking continuous-time Markov chains

This page was built for publication: Model checking single agent behaviours by fluid approximation