Knowledge Based Verification of Aggregate Specifications

The paper considers the verification approach of Piece--Linear Aggregate models used for formalization and simulation of complex systems. The approach is based on constructing an aggregate specification and transforming the specification to the set of predicate logic formulas describing both aggregate specification and properties under investigation. The resolution method implemented in Prolog is applied to generate and analyze a decision tree. The presented approach is illustrated by example.