Temporal logic query checking

被引：39
|
作者：
Bruns, G [1 ]
Godefroid, P [1 ]
机构：
[1] Lucent Technol, Bell Labs, Naperville, IL 60566 USA
来源：
16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS | 2001年
关键词：
D O I：
10.1109/LICS.2001.932516
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
A temporal logic query checker takes as input a Kripke structure and a temporal logic formula with a hole, and returns the set of propositional formulas that, when put in the hole, are satisfied by the Kripke structure. By allowing the temporal properties of a System to be discovered, query checking is useful in the study and reverse engineering of systems. Temporal logic query checking was first proposed in [2]. In this paper, we generalize and simplify Chan's work by showing how a new class of alternating automata can be used for query checking with a wide range of temporal logics.
引用
收藏
页码：409 / 417
页数：9
相关论文
共 50 条
  • [1] Query Checking for Linear Temporal Logic
    Huang, Samuel
    Cleaveland, Rance
    [J]. CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION (FMICS-AVOCS 2017), 2017, 10471 : 34 - 48
  • [2] Temporal logic query checking: A tool for model exploration
    Gurfinkel, A
    Chechik, M
    Devereux, B
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (10) : 898 - 914
  • [3] Temporal logic to query semantic graphs using the model checking method
    Gueffaz, Mahdi
    Rampacek, Sylvain
    Nicolle, Christophe
    [J]. Journal of Software, 2012, 7 (07) : 1462 - 1472
  • [4] Temporal-Logic Query Checking over Finite Data Streams
    Huang, Samuel
    Cleaveland, Rance
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2020, 2020, 12327 : 252 - 271
  • [5] Temporal-logic query checking over finite data streams
    Huang, Samuel
    Cleaveland, Rance
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2022, 24 (03) : 473 - 492
  • [6] Temporal-logic query checking over finite data streams
    Samuel Huang
    Rance Cleaveland
    [J]. International Journal on Software Tools for Technology Transfer, 2022, 24 : 473 - 492
  • [7] Log-Based Understanding of Business Processes through Temporal Logic Query Checking
    Raeim, Margus
    Di Ciccio, Claudio
    Maggi, Fabrizio Maria
    Mecella, Massimo
    Mendling, Jan
    [J]. ON THE MOVE TO MEANINGFUL INTERNET SYSTEMS: OTM 2014 CONFERENCES, 2014, 8841 : 75 - 92
  • [8] Temporal logic model checking
    Clarke, EM
    [J]. LOGIC PROGRAMMING - PROCEEDINGS OF THE 1997 INTERNATIONAL SYMPOSIUM, 1997, : 3 - 3
  • [9] Temporal logic and model checking
    McMillan, KL
    [J]. VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 36 - 54
  • [10] UTP and Temporal Logic Model Checking
    Anderson, Hugh
    Ciobanu, Gabriel
    Freitas, Leo
    [J]. UNIFYING THEORIES OF PROGRAMMING, 2010, 5713 : 22 - +
12345