Smaller abstraction for ACTL* without next
Authors
UNSW
NICTA
Abstract
The successful application of model-checking to large systems relies strongly on the choice of good abstractions. In this work we present an approach for constructing abstractions when checking next-free universal ACTL* properties. It is known that functional abstractions are safe and that next-free universal ACTL* is insensitive to finite stuttering. We exploit these results by introducing a safe next-free abstraction} that is typically smaller than the usual functional one while at the same time more precise, i.e., it has less spurious counter-examples.
BibTeX Entry
@inbook{Kai_Huuck_10, author = {Engelhardt, Kai and Huuck, Ralf}, booktitle = {Concurrency, Compositionality, and Correctness: Essays in Honor of Willem-Paul de Roever}, editor = {{Dennis Dams, Ulrich Hannemann, Martin Steffen }}, isbn = {364211511X}, month = feb, pages = {250--259}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Smaller Abstraction for {ACTL}* Without Next}, volume = {5930}, year = {2010} }