Trustworthy Systems

Smaller abstraction for ACTL* without next

Authors

Kai Engelhardt and Ralf Huuck

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}
  }

Download