Symbolic Verification of GOLOG Programs with First-Order BDDs

被引：0
|
作者：
Classen, Jens [1 ]
机构：
[1] Rhein Westfal TH Aachen, Knowledge Based Syst Grp, Aachen, Germany
来源：
SIXTEENTH INTERNATIONAL CONFERENCE ON PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING | 2018年
关键词：
LANGUAGE;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
GOLOG is an agent language that allows defining behaviours in terms of programs over actions defined in a Situation Calculus action theory. Often it is vital to verify such a program against a temporal specification before deployment. So far work on the verification of GOLOG has been mostly of theoretical nature. Here we report on our efforts on implementing a verification algorithm for GOLOG based on fixpoint computations, a graph representation of program executions, and a symbolic representation of the state space. We describe the techniques used in our implementation, in particular a first-order variant of OBDDs for compactly representing formulas. We evaluate the approach by experimental analysis.
引用
收藏
页码：524 / 528
页数：5
相关论文
共 50 条
  • [1] First-Order Timed Runtime Verification Using BDDs
    Havelund, Klaus
    Peled, Doron
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2020), 2020, 12302 : 3 - 24
  • [2] HARDWARE-VERIFICATION USING FIRST-ORDER BDDS
    SCHNEIDER, K
    KUMAR, R
    KROPF, T
    [J]. COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS, 1993, 32 : 45 - 62
  • [3] Reinforcement learning for Golog programs with first-order state-abstraction
    Beck, Daniel
    Lakemeyer, Gerhard
    [J]. LOGIC JOURNAL OF THE IGPL, 2012, 20 (05) : 909 - 942
  • [4] First-order temporal logic monitoring with BDDs
    Klaus Havelund
    Doron Peled
    Dogan Ulus
    [J]. Formal Methods in System Design, 2020, 56 : 1 - 21
  • [5] First-order temporal logic monitoring with BDDs
    Havelund, Klaus
    Peled, Doron
    Ulus, Dogan
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2020, 56 (1-3) : 1 - 21
  • [6] Temporal Verification of Programs via First-Order Fixpoint Logic
    Kobayashi, Naoki
    Nishikawa, Takeshi
    Igarashi, Atsushi
    Unno, Hiroshi
    [J]. STATIC ANALYSIS (SAS 2019), 2019, 11822 : 413 - 436
  • [7] Symbolic protocol verification with queue BDDs
    Godefroid, P
    Long, DE
    [J]. 11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, : 198 - 206
  • [8] Symbolic Protocol Verification with Queue BDDs
    Patrice Godefroid
    David E. Long
    [J]. Formal Methods in System Design, 1999, 14 : 257 - 271
  • [9] Symbolic protocol verification with queue BDDs
    Godefroid, P
    Long, DE
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 1999, 14 (03) : 257 - 271
  • [10] SYMBOLIC FUNCTIONS AND FIRST-ORDER OPERATORS
    STAFFORD, M
    NIGHTINGALE, JM
    [J]. ELECTRONICS LETTERS, 1969, 5 (08) : 167 - +
12345