Satisfaction degree for a class of temporal logic formulae based on transition systems
WANG Guo-jun1, WANG Qing-ping2, SHI Hui-xian1, LUO Qing-jun1,3, WANG Wei4
( 1 College of Mathematics and Information Science, Shaanxi Normal University, Xi′an 710062, Shaanxi, China；2 School of Statistics, Jiangxi University of Finance and Economics, Nanchang 330013, Jiangxi, China；3 School of Statistics, Xi′an University of Finance and Economics, 4 Center of Information and Education Technology, Xi′an University of Finance and Economics, Xi′an 710061, Shaanxi, China)
Abstract:
The concept of a character for lineal temporal logic (LTL, for short) formulae is introduced, and the existence of characters for a class of LTL formulae as well as the computation method are obtained. Based on this concept, two types of temporal normal form for LTL formulae are proposed, and it is proved that a class of LTL formulae can be equivalently expressed in temporal normal form, which greatly simplifies the complexity of computing of characters. Meanwhile, the satisfaction degree of LTL formulae with respect to transition systems are proposed, which can be seen as a quantitative extension of the notion “TS satisfies φ”. Finally, a computation method of the satisfaction degree for a LTL formula is provided, and the computation complexity is estimated.
KeyWords:
specification; character; eventually free; dynamic model sequence; temporal normal form; satisfaction degree
