Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Loreti M., Massink M. On-the-fly probabilistic model checking. In: ICE 2014 - 7th Interaction and Concurrency Experience (Berlin, Germany, 6 June 2014). Proceedings, pp. 45 - 59. Ivan Lanese, Alberto Lluch Lafuente, Ana Sokolova, Hugo Torres Vieira (eds.). (Electronic Proceedings in Theoretical Computer Science -, vol. 166). EPTCS, 2014.
Model checking approaches can be divided into two broad categories: global approaches that determine the set of all states in a model M that satisfy a temporal logic formula Φ, and local approaches in which, given a state s in M , the procedure determines whether s satisfies Φ. When s is a term of a process language, the model-checking procedure can be executed "on-the-fly", driven by the syntactical structure of s. For certain classes of systems, e.g. those composed of many parallel components, the local approach is preferable because, depending on the specific property, it may be sufficient to generate and inspect only a relatively small part of the state space. We propose an efficient, on-the- fly, PCTL model checking procedure that is parametric with respect to the semantic interpretation of the language. The procedure comprises both bounded and unbounded until modalities. The correct- ness of the procedure is shown and its efficiency is compared with a global PCTL model checker on representative applications.
URL: http://eptcs.web.cse.unsw.edu.au/paper.cgi?ICE2014.6
DOI: 10.4204/EPTCS.166.6
Subject On the Fly model-checking
Probabilistic model-checking
B.8.2 Performance Analysis and Design Aids
D.2.4 Software/Program Verification
F.1.1 Models of Computation
60Jxx Markov processes

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