The goal of testing is to discriminate between multiple hypotheses about a system – for example, different fault diagnoses of an HVAC system – by applying input patterns and verifying or falsifying the hypotheses from the observed outputs. Definitely discriminating tests (DDTs) are those input patterns that are guaranteed to discriminate between different hypotheses of non-deterministic systems. Finding DDTs is important in practice, but can be very expensive . Even more challenging is the problem of finding a DDT that minimizes the energy consumption of the testing process, i.e., an input pattern that can be enforced with minimal energy consumption and that is a DDT. This paper addresses both problems. We show how we can transform a given problem into a Boolean structure in decomposable negation normal form (DNNF), and extract from it a Boolean formula whose models correspond to DDTs. This allows us to harness recent advances in both knowledge compilation and satisfiability for efficient and scalable DDT computation in practice. Furthermore, we show how we can generate a DNNF structure compactly encoding all DDTs of the problem and use it to obtain an energy-optimal DDT in time linear in the size of the structure.
How to Cite
diagnosis, model-based testing, SAT, DNNF graphs
(Boroday et al., 2007) S. Boroday, A. Petrenko, and R. Groz. Can a model checker generate tests for non-deterministic systems? Electronic Notes in Theoretical Computer Science, 190:3–19, 2007.
(Darwiche and Marquis, 2002) A. Darwiche and P. Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research, 17:229–264, 2002.
(Darwiche, 1998) Adnan Darwiche. Model-based diagnosis using structured system descriptions. Journal of Artificial Intelligence Research, 8:165–222, 1998.
(Darwiche, 2001) A. Darwiche. Decomposable negation normal form. Journal of the ACM, 48(4):608– 647, 2001.
(Darwiche, 2005) A. Darwiche. The C2D compiler user manual. Technical report, Comp. Sci. UCLA, 2005.
(Esser and Struss, 2007) M. Esser and P. Struss. Fault-model-based test generation for embedded software. In Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI), pages 342–347, 2007.
(Heinz and Sachenbacher, 2009) S. Heinz and M. Sachenbacher. Using model counting to find optimal distinguishing tests. In Proceedings of the Sixth International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR), pages 117–131, 2009.
(Huang, 2007) J. Huang. A case for simple SAT solvers. In Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming (CP), pages 839–846, 2007.
(Lunze and Nixdorf, 2001) J. Lunze and B. Nixdorf. Representation of hybrid systems by means of stochastic automata. Mathematical and Computer Modeling of Dynamical Systems , 4:383–422, 2001.
(Luo et al., 2007) J. Luo, K. Pattipati, L. Qiao, and S. Chigusa. An integrated diagnostic development process for automotive engine control systems. IEEE Trans. on Systems, Man, and Cybernetics, 37(6):1163–1173, 2007.
(Sachenbacher and Schwoon, 2008) M. Sachen- bacher and S. Schwoon. Model-based testing using quantified CSPs. In ECAI-08 Workshop on Model-based Systems, 2008.
(Schumann et al., 2009) A. Schumann, M. Sachen- bacher, and J. Huang. Constraint-based optimal testing using DNNF graphs. In Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming (CP), pages 731–745, 2009.
(Schumann et al., 2010) A. Schumann, J. Huang, and M. Sachenbacher. Computing cost-optimal definitely discriminating tests. In Proceedings of the 24th National Conference on Artificial Intelligence (AAAI), 2010.
(Struss, 1994) P. Struss. Testing physical systems. In
Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-94), pages 251–256, 1994.
(Struss, 2007) P. Struss. Model-based optimization of testing through reduction of stimuli. In Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI), pages 593–598, 2007.
(Torta and D. Theseider Dupré, 2008) G. Torta and L. Anselma D. Theseider Dupré. Hypothesis discrimination with abstractions based on observation and action costs. In Proceedings of the 19th International Workshop on Principles of Diagnosis (DX- 08), pages 189–196, 2008.
(Tseitin, 1968) G. Tseitin. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, pages 115–125, 1968.
(Venturini and Provan, 2008) A. Venturini and G. Provan. Incremental algorithms for approximate compilation. In Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI-08), 2008.
(Walsh,2000) T.Walsh.SATvs.CSP.InProceedings of the Sixth International Conference on Principles and Practice of Constraint Programming (CP), pages 441–456, 2000.
The Prognostic and Health Management Society advocates open-access to scientific data and uses a Creative Commons license for publishing and distributing any papers. A Creative Commons license does not relinquish the author’s copyright; rather it allows them to share some of their rights with any member of the public under certain conditions whilst enjoying full legal protection. By submitting an article to the International Conference of the Prognostics and Health Management Society, the authors agree to be bound by the associated terms and conditions including the following:
As the author, you retain the copyright to your Work. By submitting your Work, you are granting anybody the right to copy, distribute and transmit your Work and to adapt your Work with proper attribution under the terms of the Creative Commons Attribution 3.0 United States license. You assign rights to the Prognostics and Health Management Society to publish and disseminate your Work through electronic and print media if it is accepted for publication. A license note citing the Creative Commons Attribution 3.0 United States License as shown below needs to be placed in the footnote on the first page of the article.
First Author et al. This is an open-access article distributed under the terms of the Creative Commons Attribution 3.0 United States License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.