TY - GEN
T1 - A logic approach for LTL system modification
AU - Ding, Yulin
AU - Zhang, Yan
PY - 2005
Y1 - 2005
N2 - Model checking has been successfully applied to system verification. However, there are no standard and universal tools to date being applied for system modification. This paper introduces a formal approach called the Linear Temporal Logic (LTL) model update for system modification. In contrast to previous error repairing methods, which were usually simple program debugging and specialized technical methods, our LTL model update modifies the existing LTL model of an abstracted system to correct automatically the errors occurring within this model. We introduce three single operations to represent, update, and simplify the updating problem. The minimal change rules are then defined based on such update operations. We show how our approach can eventually be applied in system modifications by illustrating an example of program corrections and characterizing some frequently used properties in the LTL Kripke model.
AB - Model checking has been successfully applied to system verification. However, there are no standard and universal tools to date being applied for system modification. This paper introduces a formal approach called the Linear Temporal Logic (LTL) model update for system modification. In contrast to previous error repairing methods, which were usually simple program debugging and specialized technical methods, our LTL model update modifies the existing LTL model of an abstracted system to correct automatically the errors occurring within this model. We introduce three single operations to represent, update, and simplify the updating problem. The minimal change rules are then defined based on such update operations. We show how our approach can eventually be applied in system modifications by illustrating an example of program corrections and characterizing some frequently used properties in the LTL Kripke model.
KW - Belief revision and update
KW - Logic for Artificial Intelligence
KW - Model checking
KW - Model update
KW - Temporal reasoning
UR - https://www.scopus.com/pages/publications/26944491108
U2 - 10.1016/j.neuint.2004.12.009
DO - 10.1016/j.neuint.2004.12.009
M3 - Conference Paper
AN - SCOPUS:26944491108
SN - 3540258787
SN - 9783540258780
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 435
EP - 444
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
T2 - 15th International Symposium on Methodologies for Intelligent Systems, ISMIS 2005
Y2 - 25 May 2005 through 28 May 2005
ER -