Fluid Model Checking of Timed Properties

DOI10.1007/978-3-319-22975-1_12zbMath1465.68171arXiv1506.05909OpenAlexW1190219380MaRDI QIDQ2945594

Luca Bortolussi, Roberta Lanciani

Publication date: 14 September 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1506.05909

zbMATH Keywords

delay differential equationsfluid approximationdeterministic timed automatafluid model checkingstochastic model checkingtime-inhomogeneous Markov renewal processes

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Stochastic functional-differential equations (34K50) Specification and verification (program logics, model checking, etc.) (68Q60) Applications of Markov renewal processes (reliability, queueing networks, etc.) (60K20) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties ⋮ Model checking Markov population models by stochastic approximations ⋮ Mean-Field Limits Beyond Ordinary Differential Equations

Cites Work

• Differential equation approximations for Markov chains
• A theory of timed automata
• Stochastic epidemic models and their statistical analysis
• Model checking single agent behaviours by fluid approximation
• On-the-fly Fast Mean-Field Model-Checking
• Fluid Model Checking
• Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Observing Continuous-Time MDPs by 1-Clock Timed Automata
• Verification of linear duration properties over continuous-time markov chains
• Implementing Radau IIA methods for stiff delay differential equations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item