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
关键词
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 条
  • [1] Model checking linear logic specifications
    Bozzano, M
    DelZanno, G
    Martelli, M
    [J]. THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2004, 4 : 573 - 619
  • [2] BRANCHING TIME REGULAR TEMPORAL LOGIC FOR MODEL CHECKING WITH LINEAR-TIME COMPLEXITY
    HAMAGUCHI, K
    HIRAISHI, H
    YAJIMA, S
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 253 - 262
  • [3] Linear Temporal Logic Symbolic Model Checking
    Rozier, Kristin Y.
    [J]. COMPUTER SCIENCE REVIEW, 2011, 5 (02) : 163 - 203
  • [4] Model Checking General Linear Temporal Logic
    French, Tim
    McCabe-Dansted, John
    Reynolds, Mark
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2013), 2013, 8123 : 119 - 133
  • [5] Exploiting symmetry in linear time temporal logic model checking:: One step beyond
    Ajami, K
    Haddad, S
    Ilié, JM
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 : 52 - 67
  • [6] Quantitative model checking of linear-time properties based on generalized possibility measures
    Li, Yongming
    [J]. FUZZY SETS AND SYSTEMS, 2017, 320 : 17 - 39
  • [7] Model Checking the Quantitative μ-Calculus on Linear Hybrid Systems
    Fischer, Diana
    Kaiser, Lukasz
    [J]. AUTOMATA, LANGUAGES AND PROGRAMMING, ICALP, PT II, 2011, 6756 : 404 - 415
  • [8] MODEL CHECKING THE QUANTITATIVE μ-CALCULUS ON LINEAR HYBRID SYSTEMS
    Fischer, Diana
    Kaiser, Lukasz
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (03)
  • [9] Model checking for a probabilistic branching time logic with fairness
    Baier, C
    Kwiatkowska, M
    [J]. DISTRIBUTED COMPUTING, 1998, 11 (03) : 125 - 155
  • [10] Indexed linear logic and higher-order model checking
    Grellois, Charles
    Mellies, Paul-Andre
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (177): : 43 - 52