Istituto di Scienza e Tecnologie dell'Informazione     
Bortolussi L., Hillston J. Fluid model checking. In: CONCUR 2012 - Concurrency Theory. 23rd International Conference (Newcastle upon Tyne, UK, 3-8 September 2012). Proceedings, pp. 333 - 347. Maciej Koutny, Irek Ulidowski (eds.). (Lecture Notes in Computer Science, vol. 7454). Springer, 2012.
In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will approximate the behaviour of a single agent with a time-inhomogeneous CTMC which depends on the environment and on the other agents only through the solution of the fluid differential equation. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae and of reachability probabilities. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.
URL: http://link.springer.com/chapter/10.1007/978-3-642-32940-1_24
DOI: 10.1007/978-3-642-32940-1_24
Subject Stochastic model checking
Fluid approximation
Mean field approximation
Reachability probability
D.2.4 Software/Program Verification
68N30 Mathematical aspects of software engineering

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional