TY - GEN
T1 - Finite Quantified Linear Temporal Logic and Its Satisfiability Checking
AU - Chen, Yu
AU - Zhang, Xiaoyu
AU - Li, Jianwen
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
PY - 2022
Y1 - 2022
N2 - In this paper, we present Finite Quantified Linear Temporal Logic (FQLTL), a new formal specification language which extends Linear Temporal Logic (LTL) with quantifiers over finite domains. Explicitly, FQLTL leverages quantifiers and predicates to constrain the domains in the system and utilizes temporal operators from LTL to specify properties with time sequences. Compared to LTL, FQLTL is more suitable and accessible to describe the specification with both restricted domains and temporal properties, which can be applied to the scenarios such as railway transition systems. In addition, this paper proposes a methodology to check FQLTL satisfiability, releasing the corresponding checker for potential users to further use. Towards experiments, we show that by applying the logic to the railway transit system, most of the safety specifications can be formalized and several inconsistent specifications are reported through our implemented satisfiability checker.
AB - In this paper, we present Finite Quantified Linear Temporal Logic (FQLTL), a new formal specification language which extends Linear Temporal Logic (LTL) with quantifiers over finite domains. Explicitly, FQLTL leverages quantifiers and predicates to constrain the domains in the system and utilizes temporal operators from LTL to specify properties with time sequences. Compared to LTL, FQLTL is more suitable and accessible to describe the specification with both restricted domains and temporal properties, which can be applied to the scenarios such as railway transition systems. In addition, this paper proposes a methodology to check FQLTL satisfiability, releasing the corresponding checker for potential users to further use. Towards experiments, we show that by applying the logic to the railway transit system, most of the safety specifications can be formalized and several inconsistent specifications are reported through our implemented satisfiability checker.
UR - https://www.scopus.com/pages/publications/85145017908
U2 - 10.1007/978-981-19-7510-3_1
DO - 10.1007/978-981-19-7510-3_1
M3 - 会议稿件
AN - SCOPUS:85145017908
SN - 9789811975097
T3 - Communications in Computer and Information Science
SP - 3
EP - 18
BT - Artificial Intelligence Logic and Applications - The 2nd International Conference, AILA 2022, Proceedings
A2 - Chen, Yixiang
A2 - Zhang, Songmao
PB - Springer Science and Business Media Deutschland GmbH
T2 - 2nd International Conference on Artificial Intelligence Logic and Applications, AILA 2022
Y2 - 26 August 2022 through 28 August 2022
ER -