Analyzing the propagation of faults is part of the preliminary safety assessment for complex safety-critical systems. A recent work proposes an SMT-based approach to deal with propagation of faults in presence of circular dependencies. The set of all the fault configurations that cause the violation of a property, also referred to as the set of minimal cut sets, is computed by means of repeated calls to the SMT solver, hence enumerating all minimal models of an SMT formula. Circularity is dealt with by imposing a strict temporal order, using the theory of difference logic. In this paper, we explore the use of Answer-Set Programming to tackle the same problem. We propose two encodings, leveraging the notion of stable model. The first approach deals with cycles in the encoding, while the second relies on ASP Modulo Acyclicity (ASPMA). We experimentally evaluate the three approaches on a comprehensive set of benchmarks. The first ASP-based encoding significantly outperforms the SMT-based approach; the ASPMA-based encoding, on the other hand, does not yield the expected performance gains.
Analysis of Cyclic Fault Propagation via ASP
Marco Bozzano;Alessandro Cimatti;Alberto Griggio;Martin Jonas;
2022-01-01
Abstract
Analyzing the propagation of faults is part of the preliminary safety assessment for complex safety-critical systems. A recent work proposes an SMT-based approach to deal with propagation of faults in presence of circular dependencies. The set of all the fault configurations that cause the violation of a property, also referred to as the set of minimal cut sets, is computed by means of repeated calls to the SMT solver, hence enumerating all minimal models of an SMT formula. Circularity is dealt with by imposing a strict temporal order, using the theory of difference logic. In this paper, we explore the use of Answer-Set Programming to tackle the same problem. We propose two encodings, leveraging the notion of stable model. The first approach deals with cycles in the encoding, while the second relies on ASP Modulo Acyclicity (ASPMA). We experimentally evaluate the three approaches on a comprehensive set of benchmarks. The first ASP-based encoding significantly outperforms the SMT-based approach; the ASPMA-based encoding, on the other hand, does not yield the expected performance gains.File | Dimensione | Formato | |
---|---|---|---|
main.pdf
solo utenti autorizzati
Descrizione: Preprint
Tipologia:
Documento in Pre-print
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
671.41 kB
Formato
Adobe PDF
|
671.41 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.