Geração de contraexemplos e testemunhas para um verificador de modelos descritos em redes de autômatos estocásticos - Correa, Claiton Marques (2013)
The counterexamples and witnesses generation is one of the main attractive features of Model Checking. Counterexamples are a great data source to debug the system, because they are generated when a specification is violeted by a model of the system. On other hand, witnesses show that a model of the system holds for an specification, through an execution trace of the system. This dissertation is part of a project aimed to the construction of a Model Checker for Stochastic Automata Networks and focuses in the generation of counterexamples and witnesses for the tool