Model checking mobile stochastic logic

DOI10.1016/J.TCS.2007.05.008MaRDI QIDQ995465zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Rocco De Nicola, Joost-Pieter Katoen, Diego Latella, Michele Loreti, Mieke Massink

Publication date 3 September 2007

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2007.05.008

zbMATH Keywords

MobilityGlobal computingStochastic logicsStochastic model-checkingStochastic process algebra

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On distributed stochastic logics for mobile systems
• Model Checking Software
• Model checking functional and performability properties of stochastic fluid models
• Formal Methods for Components and Objects
• Stochastic model checking

Cites work

• scientific article; zbMATH DE number 1361121 (Why is no real title available?)
• scientific article; zbMATH DE number 1956481 (Why is no real title available?)
• scientific article; zbMATH DE number 2079828 (Why is no real title available?)
• scientific article; zbMATH DE number 2087391 (Why is no real title available?)
• scientific article; zbMATH DE number 846904 (Why is no real title available?)
• A logic for reasoning about time and reliability
• A modal logic for mobile agents
• A spatial logic for concurrency. I
• A theory of timed automata
• Anytime, anywhere: modal logics for mobile ambients
• Formal Methods for Components and Objects
• Model checking of probabilistic and nondeterministic systems
• Model-checking continuous-time Markov chains
• Process algebra for performance evaluation
• Programming Languages and Systems
• Temporal logics for the specification of performance and reliability
• The Klaim project: Theory and practice

Cited in

(6)

• On distributed stochastic logics for mobile systems
• Spatial logic and spatial model checking for closure spaces
• Analysis of spatio-temporal properties of stochastic systems using TSTL
• \textsf{MarCaSPiS}: a Markovian extension of a calculus for services
• Assisting the design of a groupware system - Model checking usability aspects of thinkteam
• Stabilizing mobile philosophers

Describes a project that uses

Uses Software

• PRISM
• MRMC
• SLMC
• ULM
• KLAIM
• MoMo

This page was built for publication: Model checking mobile stochastic logic

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