Model Checking Quantitative Linear Time Logic

被引：23
|
作者：
Faella, Marco [1 ]
Legay, Axel [2 ]
Stoelinga, Marielle [3 ]
机构：
[1] Univ Napoli Federico II, Naples, Italy
[2] Univ Liege, Liege, Belgium
[3] Univ Twente, Enschede, Netherlands
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2008年 / 220卷 / 03期
关键词：
Linear temporal logic; Quantitative verification; Automata;
D O I：
10.1016/j.entcs.2008.11.019
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper considers QLtl, a quantitative analagon of Ltl and presents algorithms for model checking QLtl over quantitative versions of Kripke structures and Markov chains.
引用
下载
收藏
页码：61 / 77
页数：17
相关论文
共 50 条
  • [41] Model checking linear temporal logic of rewriting formulas under localized fairness
    Bae, Kyungmin
    Meseguer, Jose
    SCIENCE OF COMPUTER PROGRAMMING, 2015, 99 : 193 - 234
  • [42] Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures
    Liang C.-J.
    Li Y.-M.
    Tien Tzu Hsueh Pao/Acta Electronica Sinica, 2017, 45 (12): : 2971 - 2977
  • [43] Symbolic computation tree logic model checking of time Petri nets
    Okawa, Yasukichi
    Yoneda, Tomohiro
    Electronics and Communications in Japan, Part III: Fundamental Electronic Science (English translation of Denshi Tsushin Gakkai Ronbunshi), 1997, 80 (04): : 11 - 20
  • [44] Abstraction In Model Checking Real-Time Temporal Logic of Knowledge
    Zhou, CongHua
    Sun, Bo
    JOURNAL OF COMPUTERS, 2012, 7 (02) : 362 - 370
  • [45] Probabilistic alternating-time temporal logic and model checking algorithm
    Chen, Taolue
    Lu, Jian
    FOURTH INTERNATIONAL CONFERENCE ON FUZZY SYSTEMS AND KNOWLEDGE DISCOVERY, VOL 2, PROCEEDINGS, 2007, : 35 - +
  • [46] Model Checking of Real-Time Systems Using Rewriting Logic
    Bendiaf, Messaoud
    Bourahla, Mustapha
    Boudia, Malika
    Rehab, Seidali
    PROCEEDINGS OF 2017 INTERNATIONAL CONFERENCE ON ELECTRICAL AND INFORMATION TECHNOLOGIES (ICEIT 2017), 2017,
  • [47] Symbolic computation tree logic model checking of time Petri nets
    Okawa, Y
    Yoneda, T
    ELECTRONICS AND COMMUNICATIONS IN JAPAN PART III-FUNDAMENTAL ELECTRONIC SCIENCE, 1997, 80 (04): : 11 - 20
  • [48] Checking the linear transformation model for clustered failure time observations
    Satoshi Hattori
    Lifetime Data Analysis, 2008, 14 : 253 - 266
  • [49] Checking the linear transformation model for clustered failure time observations
    Hattori, Satoshi
    LIFETIME DATA ANALYSIS, 2008, 14 (03) : 253 - 266
  • [50] Linear-time model checking: Automata theory in practice
    Vardi, Moshe Y.
    IMPLEMENTATION AND APPLICATION OF AUTOMATA, 2007, 4783 : 5 - 10
12345