A Machine-Checked Proof of A State-Space Construction AlgorithmThis paper presents the correctness proof of Saturation, an algorithm for generating state spaces of concurrent systems, implemented in the SMART tool. Unlike the Breadth First Search exploration algorithm, which is easy to understand and formalise, Saturation is a complex algorithm, employing a mutually-recursive pair of procedures that compute a series of non-trivial, nested local fixed points, corresponding to a chaotic fixed point strategy. A pencil-and-paper proof of Saturation exists, but a machine checked proof had never been attempted. The key element of the proof is the characterisation theorem of saturated nodes in decision diagrams, stating that a saturated node represents a set of states encoding a local fixed-point with respect to firing all events affecting only the node s level and levels below. For our purpose, we have employed the Prototype Verification System (PVS) for formalising the Saturation algorithm, its data structures, and for conducting the proofs.
Document ID
20100018546
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Catano, Nestor (Universidade da Madeira Funchal, Portugal)
Siminiceanu, Radu I. (National Inst. of Aerospace Hampton, VA, United States)
Date Acquired
August 24, 2013
Publication Date
April 1, 2010
Publication Information
Publication: Proceedings of the Second NASA Formal Methods Symposium