On-the-fly Probabilistic Model Checking

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 f, and local approaches in which, given a state s in M, the procedure determines whether s satisfies f. When s is a term of a...

Full description

Bibliographic Details
Main Authors: Diego Latella, Michele Loreti, Mieke Massink
Format: Article
Language:English
Published: Open Publishing Association 2014-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1410.7469v1