This article is cited in 1 paper

Safety, Viability, Reliability, Technical Diagnostics

Formal verification of logical descriptions with functional uncertainty based on logarithmic encoding of conditions

L. D. Cheremisinova

United Institute of Informatics Problems, Belarussian National Academy of Sciences, Minsk, Belarus

Abstract: We consider the implementability testing problem for a description with functional uncertainty represented with a system of partial Boolean functions (PBF) given by a combinatorial circuit. Implementability testing is based on a formal approach in which we construct a conjunctive normal form (CNF) based on encoding multi-output intervals from the domain of this system. We propose a method for CNF construction related to a system of PBFs which is based on logarithmic encoding of multi-output intervals from the domain of this system and lets one reduce the number of auxiliary variables introduced in the resulting CNF.

Presented by the member of Editorial Board: P. P. Parkhomenko

Received: 28.01.2011

 English version: Automation and Remote Control, 2012, 73:7, 1216–1226

Bibliographic databases:

• 
•