Behavioral Diagnosis of LTL Specifications at Operator Level
Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. Pages 1053-1058.
Abstract
Product defects and rework efforts due to flawed specifications represent major issues for a project's performance, so that there is a high motivation for providing effective means that assist designers in assessing and ensuring a specification's quality. Recent research in the context of formal specifications, e.g. on coverage and vacuity, offers important means to tackle related issues. In the currently underrepresented research direction of diagnostic reasoning on a specification, we propose a scenario-based diagnosis at a specification's operator level using weak or strong fault models. Drawing on efficient SAT encodings, we show in this paper how to achieve that effectively for specifications in LTL. Our experimental results illustrate our approach's validity and attractiveness.
@inproceedings{ijcai2013p160,
title = {Behavioral Diagnosis of LTL Specifications at Operator Level},
author = {Pill, Ingo and Quaritsch, Thomas},
booktitle = {Proceedings of the Twenty-Third International Joint Conference on
Artificial Intelligence, {IJCAI-13}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Francesca Rossi},
pages = {1053--1058},
year = {2013},
month = {8},
url = {https://ijcai.org/proceedings/2013/160},
}
TY - CPAPER TI - Behavioral Diagnosis of LTL Specifications at Operator Level AU - Pill, Ingo AU - Quaritsch, Thomas T2 - Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI-13 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2013 SP - 1053 EP - 1058 UR - https://ijcai.org/proceedings/2013/160 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
